ValuationSubring_toSubring_eq_integralClosure_and_finite_and_isDiscreteValuationRing_of_henselian.lean

theorem isArtinianRing_quotient_map_maximalIdeal
    {R : Type u} [CommRing R] [IsLocalRing R]
    {S : Type v} [CommRing S] [Algebra R S] [Module.Finite R S] :
    IsArtinianRing (S ⧸ (IsLocalRing.maximalIdeal R).map (algebraMap R S))

theorem isLocalRing_of_isDomain_of_moduleFinite
    {R : Type u} [CommRing R] [HenselianLocalRing R]
    {S : Type v} [CommRing S] [IsDomain S] [Algebra R S] [Module.Finite R S] : IsLocalRing S

theorem mem_of_isIntegral {K F : Type} [Field K] [Field F] [Algebra K F]
    (O : ValuationSubring K) [Algebra O F] [IsScalarTower O K F]
    (O' : ValuationSubring F) (hO' : ∀ x : K, algebraMap K F x ∈ O' ↔ x ∈ O)
    {y : F} (hy : IsIntegral O y) : y ∈ O'

theorem valuationSubring_eq_integralClosure_of_henselian
    {K F : Type} [Field K] [Field F] [Algebra K F] [FiniteDimensional K F] [Algebra.IsSeparable K F]
    (O : ValuationSubring K) [IsDiscreteValuationRing O] [HenselianLocalRing O]
    [Algebra O F] [IsScalarTower O K F]
    (O' : ValuationSubring F) (hO' : ∀ x : K, algebraMap K F x ∈ O' ↔ x ∈ O) :
    O'.toSubring = (integralClosure O F).toSubring ∧ Module.Finite O (integralClosure O F) ∧
      IsDiscreteValuationRing (integralClosure O F)

theorem toSubring_eq_integralClosure_and_finite_and_isDiscreteValuationRing_of_henselian
    {K F : Type} [Field K] [Field F] [Algebra K F] [FiniteDimensional K F] [Algebra.IsSeparable K F]
    (O : ValuationSubring K) [IsDiscreteValuationRing O] [HenselianLocalRing O]
    [Algebra O F] [IsScalarTower O K F]
    (O' : ValuationSubring F) (hO' : ∀ x : K, algebraMap K F x ∈ O' ↔ x ∈ O) :
    O'.toSubring = (integralClosure O F).toSubring ∧ Module.Finite O (integralClosure O F) ∧
      IsDiscreteValuationRing (integralClosure O F)