Valuation subrings are exactly the maximal local subrings #

See LocalSubring.isMax_iff. Note that the order on local subrings is not merely inclusion but domination.

Cast a valuation subring to a local subring.

Equations

A.toLocalSubring = { toSubring := A.toSubring, isLocalRing := ⋯ }

Instances For

source

theorem ValuationSubring.toLocalSubring_injective {K : Type u_3} [Field K] :

Function.Injective toLocalSubring

source

theorem LocalSubring.map_maximalIdeal_eq_top_of_isMax {K : Type u_3} [Field K] {R : LocalSubring K} (hR : IsMax R) {S : Subring K} (hS : R.toSubring < S) :

Ideal.map (Subring.inclusion ⋯) (IsLocalRing.maximalIdeal ↥R.toSubring) = ⊤

source

theorem LocalSubring.mem_of_isMax_of_isIntegral {K : Type u_3} [Field K] {R : LocalSubring K} (hR : IsMax R) {x : K} (hx : IsIntegral (↥R.toSubring) x) :

x ∈ R.toSubring

Stacks Tag 00IC

source

theorem ValuationSubring.isMax_toLocalSubring {K : Type u_3} [Field K] (R : ValuationSubring K) :

IsMax R.toLocalSubring

Stacks Tag 052K

source

theorem LocalSubring.exists_valuationRing_of_isMax {K : Type u_3} [Field K] {R : LocalSubring K} (hR : IsMax R) :

∃ (R' : ValuationSubring K), R'.toLocalSubring = R

Stacks Tag 00IB

source

theorem LocalSubring.isMax_iff {K : Type u_3} [Field K] {A : LocalSubring K} :

IsMax A ↔ ∃ (B : ValuationSubring K), B.toLocalSubring = A

A local subring is maximal with respect to the domination order if and only if it is a valuation ring.

source

theorem LocalSubring.exists_le_valuationSubring {K : Type u_3} [Field K] (A : LocalSubring K) :

∃ (B : ValuationSubring K), A ≤ B.toLocalSubring

Stacks Tag 00IA

source

theorem Ideal.image_subset_nonunits_valuationSubring {K : Type u_3} [Field K] {A : Subring K} (I : Ideal ↥A) (hI : I ≠ ⊤) :

∃ (B : ValuationSubring K), A ≤ B.toSubring ∧ ⇑A.subtype '' ↑I ⊆ ↑B.nonunits

source

theorem Subring.exists_le_valuationSubring_of_isIntegrallyClosedIn {K : Type u_3} [Field K] {x : K} {R : Subring K} (hxR : x ∉ R) [IsIntegrallyClosedIn (↥R) K] :

∃ (V : ValuationSubring K), R ≤ V.toSubring ∧ x ∉ V

Stacks Tag 090P (part (1))

source

theorem LocalSubring.exists_le_valuationSubring_of_isIntegrallyClosedIn {K : Type u_3} [Field K] {x : K} {R : LocalSubring K} (hxR : x ∉ R.toSubring) [IsIntegrallyClosedIn (↥R.toSubring) K] :

∃ (V : ValuationSubring K), R ≤ V.toLocalSubring ∧ x ∉ V

Stacks Tag 090P (part (2))

source

theorem Subring.eq_iInf_of_isIntegrallyClosedIn {K : Type u_3} [Field K] {R : Subring K} [IsIntegrallyClosedIn (↥R) K] :

R = ⨅ (V : { V : ValuationSubring K // R ≤ V.toSubring }), (↑V).toSubring

A subring integrally closed in a field is the intersection of valuation subrings containing it.

source

theorem LocalSubring.eq_iInf_of_isIntegrallyClosedIn {K : Type u_3} [Field K] {R : LocalSubring K} [IsIntegrallyClosedIn (↥R.toSubring) K] :

R.toSubring = ⨅ (V : { V : ValuationSubring K // R ≤ V.toLocalSubring }), (↑V).toSubring

A local subring integrally closed in a field is the intersection of valuation subrings dominating it.

source

theorem iInf_valuationSubring_superset {K : Type u_3} [Field K] {s : Set K} :

⨅ (V : { V : ValuationSubring K // s ⊆ ↑V.toSubring }), (↑V).toSubring = (integralClosure (↥(Subring.closure s)) K).toSubring

The integral closure of a subset in a field is the intersection of all valuation subrings containing it.

source

theorem bijective_rangeRestrict_comp_of_valuationRing {R : Type u_1} {S : Type u_2} {K : Type u_3} [CommRing R] [CommRing S] [Field K] [IsDomain R] [ValuationRing R] [IsLocalRing S] [Algebra R K] [IsFractionRing R K] (f : R →+* S) (g : S →+* K) (h : g.comp f = algebraMap R K) [IsLocalHom f] :

Function.Bijective ⇑(g.rangeRestrict.comp f)

source

theorem IsLocalRing.exists_factor_valuationRing {R : Type u_1} {K : Type u_3} [CommRing R] [Field K] [IsLocalRing R] (f : R →+* K) :

∃ (A : ValuationSubring K) (h : ∀ (x : R), f x ∈ A.toSubring), IsLocalHom (f.codRestrict A.toSubring h)

Documentation

Mathlib.RingTheory.Valuation.LocalSubring

Valuation subrings are exactly the maximal local subrings #