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 ≤ Valuation.supp v) : 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

• Valuation.onQuotVal v 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 ≤ Valuation.supp v) : Valuation (R ⧸ J) Γ₀

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

Equations

• Valuation.onQuot v hJ = { toMonoidWithZeroHom := { toZeroHom := { toFun := Valuation.onQuotVal v 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 ≤ Valuation.supp v) : Valuation.comap (Ideal.Quotient.mk J) (Valuation.onQuot v 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.supp (Valuation.comap (Ideal.Quotient.mk J) v)

@[simp]

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

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

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

def AddValuation.onQuotVal {R : Type u_1} {Γ₀ : Type u_2} [CommRing R] [LinearOrderedAddCommMonoidWithTop Γ₀] (v : AddValuation R Γ₀) {J : Ideal R} (hJ : J ≤ AddValuation.supp v) : 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

• AddValuation.onQuotVal v 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 ≤ AddValuation.supp v) : AddValuation (R ⧸ J) Γ₀

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

Equations

• AddValuation.onQuot v 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 ≤ AddValuation.supp v) : AddValuation.comap (Ideal.Quotient.mk J) (AddValuation.onQuot v 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.supp (AddValuation.comap f v) = Ideal.comap f (AddValuation.supp v)

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.supp (AddValuation.comap (Ideal.Quotient.mk J) v)

@[simp]

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

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

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