The valuation on a quotient ring

The support of a valuation v : Valuation R Γ₀ is supp v. If J is an ideal of R with h : J ⊆ supp v then the induced valuation on R / J = Ideal.Quotient J is onQuot v h.

def Valuation.onQuotVal {R : Type u_1} {Γ₀ : Type u_2} [CommRing R] [LinearOrderedCommMonoidWithZero Γ₀] (v : Valuation R Γ₀) {J : Ideal R} (hJ : J ≤ v.supp) : R ⧸ J → Γ₀

If hJ : J ⊆ supp v then onQuotVal hJ is the induced function on R / J as a function. Note: it's just the function; the valuation is onQuot hJ.

def Valuation.onQuot {R : Type u_1} {Γ₀ : Type u_2} [CommRing R] [LinearOrderedCommMonoidWithZero Γ₀] (v : Valuation R Γ₀) {J : Ideal R} (hJ : J ≤ v.supp) : Valuation (R ⧸ J) Γ₀

The extension of valuation v on R to valuation on R / J if J ⊆ supp v.

@[simp]

theorem Valuation.onQuot_comap_eq {R : Type u_1} {Γ₀ : Type u_2} [CommRing R] [LinearOrderedCommMonoidWithZero Γ₀] (v : Valuation R Γ₀) {J : Ideal R} (hJ : J ≤ v.supp) : comap (Ideal.Quotient.mk J) (v.onQuot hJ) = v

theorem Valuation.self_le_supp_comap {R : Type u_1} {Γ₀ : Type u_2} [CommRing R] [LinearOrderedCommMonoidWithZero Γ₀] (J : Ideal R) (v : Valuation (R ⧸ J) Γ₀) : J ≤ (comap (Ideal.Quotient.mk J) v).supp

@[simp]

theorem Valuation.comap_onQuot_eq {R : Type u_1} {Γ₀ : Type u_2} [CommRing R] [LinearOrderedCommMonoidWithZero Γ₀] (J : Ideal R) (v : Valuation (R ⧸ J) Γ₀) : (comap (Ideal.Quotient.mk J) v).onQuot ⋯ = v

theorem Valuation.supp_quot {R : Type u_1} {Γ₀ : Type u_2} [CommRing R] [LinearOrderedCommMonoidWithZero Γ₀] (v : Valuation R Γ₀) {J : Ideal R} (hJ : J ≤ v.supp) : (v.onQuot hJ).supp = Ideal.map (Ideal.Quotient.mk J) v.supp

The quotient valuation on R / J has support (supp v) / J if J ⊆ supp v.

theorem Valuation.supp_quot_supp {R : Type u_1} {Γ₀ : Type u_2} [CommRing R] [LinearOrderedCommMonoidWithZero Γ₀] (v : Valuation R Γ₀) : (v.onQuot ⋯).supp = 0

def AddValuation.onQuotVal {R : Type u_1} {Γ₀ : Type u_2} [CommRing R] [LinearOrderedAddCommMonoidWithTop Γ₀] (v : AddValuation R Γ₀) {J : Ideal R} (hJ : J ≤ v.supp) : R ⧸ J → Γ₀

If hJ : J ⊆ supp v then onQuotVal hJ is the induced function on R / J as a function. Note: it's just the function; the valuation is onQuot hJ.

def AddValuation.onQuot {R : Type u_1} {Γ₀ : Type u_2} [CommRing R] [LinearOrderedAddCommMonoidWithTop Γ₀] (v : AddValuation R Γ₀) {J : Ideal R} (hJ : J ≤ v.supp) : AddValuation (R ⧸ J) Γ₀

The extension of valuation v on R to valuation on R / J if J ⊆ supp v.

@[simp]

theorem AddValuation.onQuot_comap_eq {R : Type u_1} {Γ₀ : Type u_2} [CommRing R] [LinearOrderedAddCommMonoidWithTop Γ₀] (v : AddValuation R Γ₀) {J : Ideal R} (hJ : J ≤ v.supp) : comap (Ideal.Quotient.mk J) (v.onQuot hJ) = v

theorem AddValuation.comap_supp {R : Type u_1} {Γ₀ : Type u_2} [CommRing R] [LinearOrderedAddCommMonoidWithTop Γ₀] (v : AddValuation R Γ₀) {S : Type u_3} [CommRing S] (f : S →+* R) : (comap f v).supp = Ideal.comap f v.supp

theorem AddValuation.self_le_supp_comap {R : Type u_1} {Γ₀ : Type u_2} [CommRing R] [LinearOrderedAddCommMonoidWithTop Γ₀] (J : Ideal R) (v : AddValuation (R ⧸ J) Γ₀) : J ≤ (comap (Ideal.Quotient.mk J) v).supp

@[simp]

theorem AddValuation.comap_onQuot_eq {R : Type u_1} {Γ₀ : Type u_2} [CommRing R] [LinearOrderedAddCommMonoidWithTop Γ₀] (J : Ideal R) (v : AddValuation (R ⧸ J) Γ₀) : (comap (Ideal.Quotient.mk J) v).onQuot ⋯ = v

theorem AddValuation.supp_quot {R : Type u_1} {Γ₀ : Type u_2} [CommRing R] [LinearOrderedAddCommMonoidWithTop Γ₀] (v : AddValuation R Γ₀) {J : Ideal R} (hJ : J ≤ v.supp) : (v.onQuot hJ).supp = Ideal.map (Ideal.Quotient.mk J) v.supp

The quotient valuation on R / J has support (supp v) / J if J ⊆ supp v.

theorem AddValuation.supp_quot_supp {R : Type u_1} {Γ₀ : Type u_2} [CommRing R] [LinearOrderedAddCommMonoidWithTop Γ₀] (v : AddValuation R Γ₀) : supp (Valuation.onQuot v ⋯) = 0