Documentation

Mathlib.RingTheory.Valuation.LocalSubring

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.

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

Cast a valuation subring to a local subring.

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