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.

instance instIsIntegrallyClosedSubtypeMemSubring {K : Type u_3} [Field K] (V : ValuationSubring K) : IsIntegrallyClosed ↥V.toSubring

instance instIsIntegrallyClosedSubtypeMemValuationSubring {K : Type u_3} [Field K] (V : ValuationSubring K) : IsIntegrallyClosed ↥V

def ValuationSubring.toLocalSubring {K : Type u_3} [Field K] (A : ValuationSubring K) : LocalSubring K

Cast a valuation subring to a local subring.

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

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) = ⊤

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

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

Stacks Tag 052K

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

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.

theorem LocalSubring.exists_le_valuationSubring {K : Type u_3} [Field K] (A : LocalSubring K) : ∃ (B : ValuationSubring K), A ≤ B.toLocalSubring

Stacks Tag 00IA

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

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

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

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.

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.

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.

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)

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)