ValuationSubring_exists_intermediateField_finiteDimensional_henselianLocalRing_comap_of_henselianLocalRing.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 eq_top_of_comap_eq_top {L : Type*} [Field L] (A : ValuationSubring L) (K₀ : Subfield L)
    [Algebra.IsAlgebraic K₀ L] (K₁ : IntermediateField K₀ L)
    (htop : A.comap (algebraMap K₁ L) = ⊤) : A = ⊤

theorem isNoetherianRing_and_henselianLocalRing_comap_of_eq_top {L : Type*} [Field L] (A :
  ValuationSubring L)
    {K₁ : Type*} [Field K₁] (f : K₁ →+* L) (hA : A = ⊤) :
    IsNoetherianRing ↥(A.comap f) ∧ HenselianLocalRing ↥(A.comap f)

theorem isFractionRing_of_range {L : Type*} [Field L] (A : ValuationSubring L) (K₀ : Subfield L)
    {A₀ : Type*} [CommRing A₀] (ι₀ : A₀ →+* K₀) (hinj : Function.Injective ι₀)
    (hrange : ∀ z : K₀, (z : L) ∈ A → ∃ a, ι₀ a = z) :
    letI : Algebra A₀ K₀ := ι₀.toAlgebra
    IsFractionRing A₀ K₀ := by
  let : Algebra A₀ K₀ := ι₀.toAlgebra
  have : FaithfulSMul A₀ K₀ := (faithfulSMul_iff_algebraMap_injective A₀ K₀).mpr hinj
  refine IsFractionRing.of_field A₀ K₀ (fun z => ?_)
  by_cases hz : (z : L) ∈ A
  · obtain ⟨a, ha⟩ := hrange z hz
    exact ⟨a, 1, by rw [map_one, div_one]; exact ha.symm⟩
  · have hz0 : (z : L) ≠ 0 := fun h => hz (h ▸ A.zero_mem)
    have hzi : ((z⁻¹ : K₀) : L) ∈ A := by
      rw [Subfield.coe_inv]
      exact (A.mem_or_inv_mem (z : L)).resolve_left hz
    obtain ⟨b, hb⟩ := hrange (z⁻¹) hzi
    refine ⟨1, b, ?_⟩
    rw [map_one]
    change z = 1 / ι₀ b
    rw [hb, one_div, inv_inv]

theorem exists_intermediateField_finiteDimensional_henselianLocalRing_comap_of_henselianLocalRing
    {L : Type u} [Field L] [IsAlgClosed L] (A : ValuationSubring L)
    (A₀ : Type u) [CommRing A₀] [IsNoetherianRing A₀] [HenselianLocalRing A₀] [IsDomain A₀]
    (hdim : Ring.KrullDimLE 1 A₀)
    (ι : A₀ →+* A) [IsLocalHom ι] (hι : Function.Injective ι)
    (K₀ : Subfield L)
    (hrange : Set.range (fun a : A₀ => ((ι a : A) : L)) = (A : Set L) ∩ (K₀ : Set L))
    [Algebra.IsAlgebraic K₀ L]
    (hres : Function.Surjective ((IsLocalRing.residue A).comp ι))
    (Λ : Finset L) :
    ∃ (K₁ : IntermediateField K₀ L) (_ : FiniteDimensional K₀ K₁),
      (↑Λ : Set L) ⊆ (K₁ : Set L) ∧
      ∃ (_ : IsNoetherianRing ↥(A.comap (algebraMap K₁ L)))
        (_ : HenselianLocalRing ↥(A.comap (algebraMap K₁ L)))
        (j : A₀ →+* ↥(A.comap (algebraMap K₁ L))) (ι₁ : ↥(A.comap (algebraMap K₁ L)) →+* A)
        (_ : IsLocalHom j) (_ : IsLocalHom ι₁),
        Function.Injective ι₁ ∧ ι₁.comp j = ι ∧
        Function.Surjective ((IsLocalRing.residue A).comp ι₁) ∧
        (∀ x : ↥(A.comap (algebraMap K₁ L)), ((ι₁ x : A) : L) = algebraMap K₁ L (x : K₁)) ∧
        (A ≠ ⊤ → IsDiscreteValuationRing ↥(A.comap (algebraMap K₁ L))) := by
  classical
  let K₁ : IntermediateField K₀ L := IntermediateField.adjoin K₀ (↑Λ : Set L)
  have hfin : FiniteDimensional K₀ K₁ := by
    apply IntermediateField.finiteDimensional_adjoin
    intro x _
    exact Algebra.IsIntegral.isIntegral x
  have hΛ : (↑Λ : Set L) ⊆ (K₁ : Set L) := IntermediateField.subset_adjoin K₀ _
  refine ⟨K₁, hfin, hΛ, ?_⟩
  set A₁ : ValuationSubring K₁ := A.comap (algebraMap K₁ L) with hA₁_def
  have hιK₀ : ∀ a : A₀, ((ι a : A) : L) ∈ K₀ := fun a =>
    ((hrange.le : Set.range (fun a : A₀ => ((ι a : A) : L)) ⊆ _) ⟨a, rfl⟩).2
  let ι₀ : A₀ →+* K₀ :=
    { toFun := fun a => ⟨((ι a : A) : L), hιK₀ a⟩
      map_one' := by ext; simp
      map_mul' := fun a b => by ext; simp
      map_zero' := by ext; simp
      map_add' := fun a b => by ext; simp }
  have hι₀ : ∀ a : A₀, ((ι₀ a : K₀) : L) = ((ι a : A) : L) := fun a => rfl
  have hι₀_inj : Function.Injective ι₀ := by
    intro a b h
    apply hι
    ext
    simpa [hι₀] using congrArg (fun z : K₀ => (z : L)) h
  have hjmem : ∀ a : A₀, (algebraMap K₀ K₁ (ι₀ a)) ∈ A₁ := by
    intro a
    rw [hA₁_def, ValuationSubring.mem_comap]
    change algebraMap K₁ L (algebraMap K₀ K₁ (ι₀ a)) ∈ A
    rw [← IsScalarTower.algebraMap_apply]
    exact (ι a).2
  let j : A₀ →+* ↥A₁ := ((algebraMap K₀ K₁).comp ι₀).codRestrict A₁ hjmem
  have hι₁mem : ∀ x : ↥A₁, (algebraMap K₁ L).comp A₁.subtype x ∈ A := fun x =>
    (ValuationSubring.mem_comap).mp x.2
  let ι₁ : ↥A₁ →+* ↥A := ((algebraMap K₁ L).comp A₁.subtype).codRestrict A hι₁mem
  have hι₁ : ∀ x : ↥A₁, ((ι₁ x : A) : L) = algebraMap K₁ L (x : K₁) := fun x => rfl
  have hcomp : ι₁.comp j = ι := by
    ext a
    change algebraMap K₁ L (algebraMap K₀ K₁ (ι₀ a)) = ((ι a : A) : L)
    rw [← IsScalarTower.algebraMap_apply]
    rfl
  have hι₁_inj : Function.Injective ι₁ := by
    intro x y h
    have h' := congrArg (fun z : ↥A => (z : L)) h
    simp only [hι₁] at h'
    exact Subtype.ext ((algebraMap K₁ L).injective h')
  have hres₁ : Function.Surjective ((IsLocalRing.residue ↥A).comp ι₁) := by
    intro r
    obtain ⟨a, ha⟩ := hres r
    refine ⟨j a, ?_⟩
    rw [← ha]
    change IsLocalRing.residue ↥A (ι₁ (j a)) = IsLocalRing.residue ↥A (ι a)
    rw [← hcomp]
    rfl
  have hloc₁ : IsLocalHom ι₁ := by
    refine ⟨fun x hx => ?_⟩
    have hx0 : (x : K₁) ≠ 0 := by
      intro h0
      apply hx.ne_zero
      apply Subtype.ext
      change algebraMap K₁ L (x : K₁) = 0
      rw [h0, map_zero]
    obtain ⟨y, hy⟩ := isUnit_iff_exists_inv.mp hx
    have hyL : (y : L) = (algebraMap K₁ L (x : K₁))⁻¹ := by
      have h1 : algebraMap K₁ L (x : K₁) * (y : L) = 1 := by
        have := congrArg (fun z : ↥A => (z : L)) hy
        simpa [hι₁] using this
      exact (eq_inv_of_mul_eq_one_right h1)
    have hinv : (x : K₁)⁻¹ ∈ A₁ := by
      change (x : K₁)⁻¹ ∈ A.comap (algebraMap K₁ L)
      rw [ValuationSubring.mem_comap, map_inv₀, ← hyL]
      exact y.2
    exact isUnit_iff_exists_inv.mpr ⟨⟨(x : K₁)⁻¹, hinv⟩, Subtype.ext (mul_inv_cancel₀ hx0)⟩
  have hlocj : IsLocalHom j := by
    refine ⟨fun a ha => ?_⟩
    have h1 : IsUnit (ι₁ (j a)) := ha.map ι₁
    have h2 : IsUnit (ι a) := by rwa [← hcomp]
    exact IsLocalHom.map_nonunit a h2
  let algK₀ : Algebra A₀ K₀ := ι₀.toAlgebra
  let algK₁ : Algebra A₀ K₁ := ((algebraMap K₀ K₁).comp ι₀).toAlgebra
  have : IsScalarTower A₀ K₀ K₁ := IsScalarTower.of_algebraMap_eq (fun a => rfl)
  have : IsFractionRing A₀ K₀ := HensLevelAux.isFractionRing_of_range A K₀ ι₀ hι₀_inj (fun z hz =>
    by
    obtain ⟨a, ha⟩ := (hrange.symm.le ⟨hz, z.2⟩ : (z : L) ∈ Set.range (fun a : A₀ => ((ι a : A) :
      L)))
    exact ⟨a, Subtype.ext ha⟩)
  have : Ring.KrullDimLE 1 A₀ := hdim
  have hA₁A₀ : ∀ a : A₀, algebraMap A₀ K₁ a ∈ A₁ := hjmem
  by_cases hA : A = ⊤
  · obtain ⟨hnoeth, hhens⟩ :=
      HensLevelAux.isNoetherianRing_and_henselianLocalRing_comap_of_eq_top A (algebraMap K₁ L) hA
    exact ⟨hnoeth, hhens, j, ι₁, hlocj, hloc₁, hι₁_inj, hcomp, hres₁, hι₁, fun h => absurd hA h⟩
  · have hA₁ne : A₁ ≠ ⊤ := fun htop => hA (HensLevelAux.eq_top_of_comap_eq_top A K₀ K₁ htop)
    have hdvr' : IsDiscreteValuationRing ↥A₁ :=
      ValuationSubring.isDiscreteValuationRing_of_algebraMap_mem_of_finite (A := A₀) (K := K₀) (L
        := K₁)
        A₁ hA₁A₀ hA₁ne
    have hnoeth : IsNoetherianRing ↥A₁ :=
      @PrincipalIdealRing.isNoetherianRing _ _ hdvr'.toIsPrincipalIdealRing
    have hhens : HenselianLocalRing ↥A₁ := by
      let : Algebra A₀ ↥A₁ := j.toAlgebra
      have : IsScalarTower A₀ ↥A₁ K₁ := IsScalarTower.of_algebraMap_eq (fun a => rfl)
      have : Algebra.IsIntegral A₀ ↥A₁ := ⟨fun y =>
        IsIntegral.tower_bot (A := ↥A₁) (B := K₁) Subtype.val_injective
          (HensLevelAux.isIntegral_of_mem_valuationSubring (K₀ := ↥K₀) A₁ hA₁A₀ hA₁ne (y : K₁) y.2)⟩
      exact HenselianLocalRing.of_isIntegral_of_isLocalRing (R := A₀)
    exact ⟨hnoeth, hhens, j, ι₁, hlocj, hloc₁, hι₁_inj, hcomp, hres₁, hι₁, fun _ => hdvr'⟩