ValuationSubring_faithfullyFlat_and_isIntegral_of_henselianLocalRing_comap.lean

theorem isIntegral_of_mem_valuationSubring
    {A₀ : Type*} [CommRing A₀] [IsDomain A₀] [IsNoetherianRing A₀] [Ring.KrullDimLE 1 A₀]
    [HenselianLocalRing A₀]
    {K₀ : Type*} [Field K₀] [Algebra A₀ K₀] [IsFractionRing A₀ K₀]
    {K₁ : Type*} [Field K₁] [Algebra A₀ K₁] [Algebra K₀ K₁] [IsScalarTower A₀ K₀ K₁]
      [FiniteDimensional K₀ K₁]
    (O : ValuationSubring K₁) (hA₀ : ∀ a : A₀, algebraMap A₀ K₁ a ∈ O) (hO : O ≠ ⊤)
    (x : K₁) (hx : x ∈ O) :
    IsIntegral A₀ x

theorem isIntegral_of_mem {K : Type u} {L : Type v} [Field K] [Field L] [Algebra K L]
  [Algebra.IsAlgebraic K L]
    (A : ValuationSubring L)
    [HenselianLocalRing ↥(A.comap (algebraMap K L))] [IsDiscreteValuationRing ↥(A.comap (algebraMap
      K L))]
    (y : L) (hy : y ∈ A) :
    letI : Algebra ↥(A.comap (algebraMap K L)) L :=
      ((algebraMap K L).comp (A.comap (algebraMap K L)).subtype).toAlgebra
    IsIntegral ↥(A.comap (algebraMap K L)) y := by
  let algL : Algebra ↥(A.comap (algebraMap K L)) L :=
    ((algebraMap K L).comp (A.comap (algebraMap K L)).subtype).toAlgebra
  have hKL : IsScalarTower ↥(A.comap (algebraMap K L)) K L := IsScalarTower.of_algebraMap_eq (fun _
    => rfl)
  have hKyL : IsScalarTower ↥(A.comap (algebraMap K L)) ↥(IntermediateField.adjoin K {y}) L :=
    IsScalarTower.of_algebraMap_eq (fun _ => rfl)
  have : Ring.KrullDimLE 1 ↥(A.comap (algebraMap K L)) :=
    Ring.KrullDimLE.mk₁' (fun I hI hp => hp.isMaximal hI)
  have hyint : IsIntegral K y := (Algebra.IsAlgebraic.isAlgebraic (R := K) y).isIntegral
  have : FiniteDimensional K ↥(IntermediateField.adjoin K {y}) :=
    IntermediateField.adjoin.finiteDimensional hyint
  set O : ValuationSubring ↥(IntermediateField.adjoin K {y}) :=
    A.comap (algebraMap ↥(IntermediateField.adjoin K {y}) L) with hO_def
  have hA₀ : ∀ a : ↥(A.comap (algebraMap K L)),
      algebraMap ↥(A.comap (algebraMap K L)) ↥(IntermediateField.adjoin K {y}) a ∈ O := by
    intro a
    rw [hO_def, ValuationSubring.mem_comap, ← IsScalarTower.algebraMap_apply]
    exact (ValuationSubring.mem_comap).mp a.2
  have hO : O ≠ ⊤ := by
    intro htop
    apply IsDiscreteValuationRing.not_a_field ↥(A.comap (algebraMap K L))
    have hall : ∀ k : K, algebraMap K L k ∈ A := fun k => by
      have h1 : algebraMap K ↥(IntermediateField.adjoin K {y}) k ∈ O := by
        rw [htop]; exact ValuationSubring.mem_top _
      rw [hO_def, ValuationSubring.mem_comap, ← IsScalarTower.algebraMap_apply] at h1
      exact h1
    rw [eq_bot_iff]
    intro a ha
    rw [Ideal.mem_bot]
    by_contra h0
    have ha0 : (a : K) ≠ 0 := fun h => h0 (Subtype.ext h)
    apply (IsLocalRing.mem_maximalIdeal _).mp ha
    refine isUnit_iff_exists_inv.mpr ⟨⟨(a : K)⁻¹, ?_⟩, Subtype.ext (mul_inv_cancel₀ ha0)⟩
    rw [ValuationSubring.mem_comap, map_inv₀]
    rw [← map_inv₀]
    exact hall _
  have hyO : (⟨y, IntermediateField.mem_adjoin_simple_self K y⟩ : ↥(IntermediateField.adjoin K
    {y})) ∈ O := by
    rw [hO_def, ValuationSubring.mem_comap]
    exact hy
  have hint := isIntegral_of_mem_valuationSubring (A₀ := ↥(A.comap (algebraMap K L))) (K₀ := K)
    (K₁ := ↥(IntermediateField.adjoin K {y})) O hA₀ hO _ hyO
  exact hint.map (IsScalarTower.toAlgHom ↥(A.comap (algebraMap K L)) ↥(IntermediateField.adjoin K
    {y}) L)

theorem _root_.ValuationSubring.faithfullyFlat_and_isIntegral_of_henselianLocalRing_comap
    {K : Type u} {L : Type v} [Field K] [Field L] [Algebra K L] [Algebra.IsAlgebraic K L]
    (A : ValuationSubring L)
    [HenselianLocalRing ↥(A.comap (algebraMap K L))] [IsDiscreteValuationRing ↥(A.comap (algebraMap
      K L))]
    [Algebra ↥(A.comap (algebraMap K L)) ↥A]
    (halg : ∀ x : ↥(A.comap (algebraMap K L)),
      ((algebraMap ↥(A.comap (algebraMap K L)) ↥A x : ↥A) : L) = algebraMap K L (x : K)) :
    Module.FaithfullyFlat ↥(A.comap (algebraMap K L)) ↥A ∧
      Algebra.IsIntegral ↥(A.comap (algebraMap K L)) ↥A