AddValuation.supp_quot
theorem AddValuation.supp_quot :
∀ {R : Type u_1} {Γ₀ : Type u_2} [inst : CommRing R] [inst_1 : LinearOrderedAddCommMonoidWithTop Γ₀]
(v : AddValuation R Γ₀) {J : Ideal R} (hJ : J ≤ v.supp),
(v.onQuot hJ).supp = Ideal.map (Ideal.Quotient.mk J) v.supp
The theorem `AddValuation.supp_quot` states that for any commutative ring `R`, any `Γ₀` which is a linearly ordered additive commutative monoid with a greatest element, any additive valuation `v` on `R` with values in `Γ₀`, and any ideal `J` in `R` such that `J` is a subset of the support of `v`, the support of the quotient valuation on `R / J` is equal to the image of the support of `v` under the quotient map `R → R / J`. In other words, if an ideal `J` is a subset of the support of an additive valuation `v`, then when we compute the valuation on the quotient ring, the support of this valuation is exactly what we get by taking the support of `v` and 'modding out' by `J`.
More concisely: The support of an additive valuation on a commutative ring modulo an ideal is equal to the image of the support under the quotient map if the ideal is contained in the support of the valuation.
|
Valuation.supp_quot
theorem Valuation.supp_quot :
∀ {R : Type u_1} {Γ₀ : Type u_2} [inst : CommRing R] [inst_1 : LinearOrderedCommMonoidWithZero Γ₀]
(v : Valuation R Γ₀) {J : Ideal R} (hJ : J ≤ v.supp),
(v.onQuot hJ).supp = Ideal.map (Ideal.Quotient.mk J) v.supp
This theorem, named `Valuation.supp_quot`, states that for any commutative ring `R` and any linearly ordered commutative monoid with zero `Γ₀`, given a valuation `v` of `R` into `Γ₀` and an ideal `J` of `R` such that `J` is a subset of the support of `v`, the support of the quotient valuation on `R / J` is equal to the image of the support of `v` under the ring homomorphism from `R` to the quotient ring `R / J`. In other words, `(v.onQuot hJ).supp = Ideal.map (Ideal.Quotient.mk J) v.supp`.
More concisely: Given a commutative ring `R`, a linearly ordered commutative monoid with zero `Γ₀`, a valuation `v` of `R` into `Γ₀`, and an ideal `J` of `R` contained in the support of `v`, the support of the quotient valuation `v.onQuot hJ` on `R / J` equals the image of `v.supp` under the ring homomorphism from `R` to `R / J`.
|