mathlib3 documentation

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

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] [linear_ordered_add_comm_monoid_with_top Γ₀] (v : add_valuation R Γ₀) {J : ideal R} (hJ : J v.supp) :
theorem add_valuation.comap_supp {R : Type u_1} {Γ₀ : Type u_2} [comm_ring R] [linear_ordered_add_comm_monoid_with_top Γ₀] (v : add_valuation R Γ₀) {S : Type u_3} [comm_ring S] (f : S →+* R) :
@[simp]
theorem add_valuation.supp_quot {R : Type u_1} {Γ₀ : Type u_2} [comm_ring R] [linear_ordered_add_comm_monoid_with_top Γ₀] (v : add_valuation R Γ₀) {J : ideal R} (hJ : J v.supp) :

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