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.

source

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

v.on_quot_val hJ = λ (q : R ⧸ J), quotient.lift_on' q ⇑v _

source

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

v.on_quot hJ = {to_monoid_with_zero_hom := {to_fun := v.on_quot_val hJ, map_zero' := _, map_one' := _, map_mul' := _}, map_add_le_max' := _}

source

@[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) :

valuation.comap (ideal.quotient.mk J) (v.on_quot hJ) = v

source

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) Γ₀) :

J ≤ (valuation.comap (ideal.quotient.mk J) v).supp

source

@[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) Γ₀) :

(valuation.comap (ideal.quotient.mk J) v).on_quot _ = v

source

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

(v.on_quot hJ).supp = ideal.map (ideal.quotient.mk J) v.supp

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

source

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

(v.on_quot le_rfl).supp = 0

source

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

v.on_quot_val hJ = valuation.on_quot_val v hJ

source

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

v.on_quot hJ = valuation.on_quot v hJ

source

@[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) :

add_valuation.comap (ideal.quotient.mk J) (v.on_quot hJ) = v

source

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

(add_valuation.comap f v).supp = ideal.comap f v.supp

source

theorem add_valuation.self_le_supp_comap {R : Type u_1} {Γ₀ : Type u_2} [comm_ring R] [linear_ordered_add_comm_monoid_with_top Γ₀] (J : ideal R) (v : add_valuation (R ⧸ J) Γ₀) :

J ≤ (add_valuation.comap (ideal.quotient.mk J) v).supp

source

@[simp]

theorem add_valuation.comap_on_quot_eq {R : Type u_1} {Γ₀ : Type u_2} [comm_ring R] [linear_ordered_add_comm_monoid_with_top Γ₀] (J : ideal R) (v : add_valuation (R ⧸ J) Γ₀) :

(add_valuation.comap (ideal.quotient.mk J) v).on_quot _ = v

source

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

(v.on_quot hJ).supp = ideal.map (ideal.quotient.mk J) v.supp

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

source

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

(v.on_quot le_rfl).supp = 0