# 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} [] (v : Valuation R Γ₀) {J : } (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
Instances For
def Valuation.onQuot {R : Type u_1} {Γ₀ : Type u_2} [] (v : Valuation R Γ₀) {J : } (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' := }
Instances For
@[simp]
theorem Valuation.onQuot_comap_eq {R : Type u_1} {Γ₀ : Type u_2} [] (v : Valuation R Γ₀) {J : } (hJ : J v.supp) :
Valuation.comap (v.onQuot hJ) = v
theorem Valuation.self_le_supp_comap {R : Type u_1} {Γ₀ : Type u_2} [] (J : ) (v : Valuation (R J) Γ₀) :
J ().supp
@[simp]
theorem Valuation.comap_onQuot_eq {R : Type u_1} {Γ₀ : Type u_2} [] (J : ) (v : Valuation (R J) Γ₀) :
().onQuot = v
theorem Valuation.supp_quot {R : Type u_1} {Γ₀ : Type u_2} [] (v : Valuation R Γ₀) {J : } (hJ : J v.supp) :
(v.onQuot hJ).supp = Ideal.map 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} [] (v : Valuation R Γ₀) :
(v.onQuot ).supp = 0
def AddValuation.onQuotVal {R : Type u_1} {Γ₀ : Type u_2} [] (v : AddValuation R Γ₀) {J : } (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 =
Instances For
def AddValuation.onQuot {R : Type u_1} {Γ₀ : Type u_2} [] (v : AddValuation R Γ₀) {J : } (hJ : J v.supp) :

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

Equations
• v.onQuot hJ =
Instances For
@[simp]
theorem AddValuation.onQuot_comap_eq {R : Type u_1} {Γ₀ : Type u_2} [] (v : AddValuation R Γ₀) {J : } (hJ : J v.supp) :
The quotient valuation on R / J has support (supp v) / J if J ⊆ supp v.