# mathlib3documentation

ring_theory.valuation.quotient

# The valuation on a quotient ring #

THIS FILE IS SYNCHRONIZED WITH MATHLIB4. Any changes to this file require a corresponding PR to mathlib4.

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 on_quot v h.

def valuation.on_quot_val {R : Type u_1} {Γ₀ : Type u_2} [comm_ring R] (v : Γ₀) {J : ideal R} (hJ : J v.supp) :
R J Γ₀

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

Equations
def valuation.on_quot {R : Type u_1} {Γ₀ : Type u_2} [comm_ring R] (v : Γ₀) {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
@[simp]
theorem valuation.on_quot_comap_eq {R : Type u_1} {Γ₀ : Type u_2} [comm_ring R] (v : Γ₀) {J : ideal R} (hJ : J v.supp) :
(v.on_quot hJ) = v
theorem valuation.self_le_supp_comap {R : Type u_1} {Γ₀ : Type u_2} [comm_ring R] (J : ideal R) (v : valuation (R J) Γ₀) :
J v).supp
@[simp]
theorem valuation.comap_on_quot_eq {R : Type u_1} {Γ₀ : Type u_2} [comm_ring R] (J : ideal R) (v : valuation (R J) Γ₀) :
v).on_quot _ = v
theorem valuation.supp_quot {R : Type u_1} {Γ₀ : Type u_2} [comm_ring R] (v : Γ₀) {J : ideal R} (hJ : J v.supp) :
(v.on_quot hJ).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} [comm_ring R] (v : Γ₀) :
def add_valuation.on_quot_val {R : Type u_1} {Γ₀ : Type u_2} [comm_ring R] (v : Γ₀) {J : ideal R} (hJ : J v.supp) :
R J Γ₀

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

Equations
def add_valuation.on_quot {R : Type u_1} {Γ₀ : Type u_2} [comm_ring R] (v : Γ₀) {J : ideal R} (hJ : J v.supp) :

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

Equations
@[simp]
theorem add_valuation.on_quot_comap_eq {R : Type u_1} {Γ₀ : Type u_2} [comm_ring R] (v : Γ₀) {J : ideal R} (hJ : J v.supp) :
(v.on_quot hJ) = v
theorem add_valuation.comap_supp {R : Type u_1} {Γ₀ : Type u_2} [comm_ring R] (v : Γ₀) {S : Type u_3} [comm_ring S] (f : S →+* R) :
v).supp = v.supp
theorem add_valuation.self_le_supp_comap {R : Type u_1} {Γ₀ : Type u_2} [comm_ring R] (J : ideal R) (v : add_valuation (R J) Γ₀) :
@[simp]
theorem add_valuation.comap_on_quot_eq {R : Type u_1} {Γ₀ : Type u_2} [comm_ring R] (J : ideal R) (v : add_valuation (R J) Γ₀) :
_ = v
theorem add_valuation.supp_quot {R : Type u_1} {Γ₀ : Type u_2} [comm_ring R] (v : Γ₀) {J : ideal R} (hJ : J v.supp) :
(v.on_quot hJ).supp =

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

theorem add_valuation.supp_quot_supp {R : Type u_1} {Γ₀ : Type u_2} [comm_ring R] (v : Γ₀) :