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.

Equations

• v.onQuotVal hJ q = Quotient.liftOn' q ⇑v ⋯

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.

Equations

• v.onQuot hJ = { toFun := v.onQuotVal hJ, map_zero' := ⋯, map_one' := ⋯, map_mul' := ⋯, map_add_le_max' := ⋯ }

@[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) : Valuation.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 ≤ (Valuation.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) Γ₀) : (Valuation.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.

Equations

• v.onQuotVal hJ = Valuation.onQuotVal v 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.

Equations

• v.onQuot hJ = Valuation.onQuot v hJ

@[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) : AddValuation.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) : (AddValuation.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 ≤ (AddValuation.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) Γ₀) : (AddValuation.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 Γ₀) : AddValuation.supp (Valuation.onQuot v ⋯) = 0