# Documentation

Mathlib.RingTheory.Valuation.Quotient

# 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 : ) :
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.

Instances For
def Valuation.onQuot {R : Type u_1} {Γ₀ : Type u_2} [] (v : Valuation R Γ₀) {J : } (hJ : ) :
Valuation (R J) Γ₀

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

Instances For
@[simp]
theorem Valuation.onQuot_comap_eq {R : Type u_1} {Γ₀ : Type u_2} [] (v : Valuation R Γ₀) {J : } (hJ : ) :
theorem Valuation.self_le_supp_comap {R : Type u_1} {Γ₀ : Type u_2} [] (J : ) (v : Valuation (R J) Γ₀) :
@[simp]
theorem Valuation.comap_onQuot_eq {R : Type u_1} {Γ₀ : Type u_2} [] (J : ) (v : Valuation (R J) Γ₀) :
Valuation.onQuot () (_ : ) = v
theorem Valuation.supp_quot {R : Type u_1} {Γ₀ : Type u_2} [] (v : Valuation R Γ₀) {J : } (hJ : ) :
=

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

Instances For
def AddValuation.onQuot {R : Type u_1} {Γ₀ : Type u_2} [] (v : AddValuation R Γ₀) {J : } (hJ : ) :

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

Instances For
@[simp]
theorem AddValuation.onQuot_comap_eq {R : Type u_1} {Γ₀ : Type u_2} [] (v : AddValuation R Γ₀) {J : } (hJ : ) :
= v
theorem AddValuation.comap_supp {R : Type u_1} {Γ₀ : Type u_2} [] (v : AddValuation R Γ₀) {S : Type u_3} [] (f : S →+* R) :
theorem AddValuation.self_le_supp_comap {R : Type u_1} {Γ₀ : Type u_2} [] (J : ) (v : AddValuation (R J) Γ₀) :
@[simp]
theorem AddValuation.comap_onQuot_eq {R : Type u_1} {Γ₀ : Type u_2} [] (J : ) (v : AddValuation (R J) Γ₀) :
theorem AddValuation.supp_quot {R : Type u_1} {Γ₀ : Type u_2} [] (v : AddValuation R Γ₀) {J : } (hJ : ) :

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} [] (v : AddValuation R Γ₀) :