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.

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

Cast a valuation subring to a local subring.

Equations

• A.toLocalSubring = LocalSubring.mk A.toSubring

theorem ValuationSubring.toLocalSubring_injective {K : Type u_3} [Field K] : Function.Injective ValuationSubring.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 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)