ValuationSubring_exists_layer_isDiscreteValuationRing_of_finite_of_isAlgebraic_of_irreducible.lean

theorem mem_of_isIntegral {L : Type} [Field L] (A : ValuationSubring L) {x : L} (hx : IsIntegral ↥A
  x) : x ∈ A

theorem mem_maximalIdeal_iff_inv_not_mem {L : Type} [Field L] (A : ValuationSubring L) (x : L) (hx
  : x ∈ A) (hx0 : x ≠ 0) :
    (⟨x, hx⟩ : ↥A) ∈ maximalIdeal ↥A ↔ x⁻¹ ∉ A

theorem residue_eq_zero_iff_inv_not_mem {L : Type} [Field L] (A : ValuationSubring L) (x : L) (hx :
  x ∈ A) (hx0 : x ≠ 0) :
    IsLocalRing.residue ↥A ⟨x, hx⟩ = 0 ↔ x⁻¹ ∉ A

theorem isUnit_of_inv_mem {L : Type} [Field L] (B : Subring L) (x : L) (hx : x ∈ B) (hxi : x⁻¹ ∈ B)
  (hx0 : x ≠ 0) :
    IsUnit (⟨x, hx⟩ : ↥B)

theorem inv_mem_of_isUnit {L : Type} [Field L] (B : Subring L) (x : ↥B) (hx : IsUnit x) : ((x :
  L))⁻¹ ∈ B

theorem exists_frac_unit_of_mem_valuationSubring
    {B : Type} [CommRing B] [IsDedekindDomain B]
    {E : Type} [Field E] [Algebra B E] [IsFractionRing B E]
    (V : ValuationSubring E) (hBV : ∀ b : B, algebraMap B E b ∈ V) (hV : V ≠ ⊤)
    (c : E) (hc : c ∈ V) :
    ∃ b s : B, s ≠ 0 ∧ algebraMap B E s ∉ V.nonunits ∧ c * algebraMap B E s = algebraMap B E b

theorem exists_layer_isDiscreteValuationRing_of_finite_of_isAlgebraic_of_irreducible
    {L : Type} [Field L] [CharZero L] (A : ValuationSubring L)
    (C' : Subring L) (hC'A : ∀ c : L, c ∈ C' → c ∈ A) [IsDiscreteValuationRing ↥C'] (ϖ' : ↥C')
      (hϖ'irr : Irreducible ϖ')
    (hϖ' : ∀ d : ↥C', IsLocalRing.residue ↥A ⟨(d : L), hC'A d d.2⟩ = 0 ↔ ∃ d' : ↥C', d = ϖ' * d')
    (halg : ∀ a : L, a ∈ A → IsAlgebraic ↥C' a)
    (S : Finset L) (hS : ∀ s ∈ S, s ∈ A) :
    ∃ (C'' : Subring L) (_ : IsDomain ↥C'') (_ : IsDiscreteValuationRing ↥C'') (ϖ'' : ↥C'') (e : ℕ)
      (R : Subring L)
      (_ : C' ≤ C'') (hC'R : C' ≤ R) (hC''A : ∀ c : L, c ∈ C'' → c ∈ A),
      (∀ s ∈ S, s ∈ C'') ∧
      (∀ c : L, c ∈ C'' ↔ c ∈ A ∧ c ∈ Subfield.closure ((C' : Set L) ∪ ↑S)) ∧
      Irreducible ϖ'' ∧
      (∀ d : ↥C'', IsLocalRing.residue ↥A ⟨(d : L), hC''A d d.2⟩ = 0 ↔ ∃ d' : ↥C'', d = ϖ'' * d') ∧
      1 ≤ e ∧ (∃ v : L, v ∈ C'' ∧ v⁻¹ ∈ C'' ∧ ((ϖ' : ↥C') : L) = v * ((ϖ'' : ↥C'') : L) ^ e) ∧
      R ≤ C'' ∧ (letI : Algebra ↥C' ↥R := (Subring.inclusion hC'R).toAlgebra; Module.Finite ↥C' ↥R)
        ∧
      (∀ c : L, c ∈ C'' → ∃ r s : L, r ∈ R ∧ s ∈ R ∧ s ≠ 0 ∧ s⁻¹ ∈ C'' ∧ c * s = r) := by
  classical
  have hϖ'0 : ϖ' ≠ 0 := hϖ'irr.ne_zero
  have hϖ'L0 : ((ϖ' : ↥C') : L) ≠ 0 := fun h => hϖ'0 (Subtype.ext h)
  have hϖ'inv : ((ϖ' : ↥C') : L)⁻¹ ∉ A :=
    (residue_eq_zero_iff_inv_not_mem A _ (hC'A _ ϖ'.2) hϖ'L0).mp ((hϖ' ϖ').mpr ⟨1, (mul_one
      _).symm⟩)
  have hmaxC' : maximalIdeal ↥C' = Ideal.span {ϖ'} :=
    (IsDiscreteValuationRing.irreducible_iff_uniformizer ϖ').mp hϖ'irr
  set K₁ : Subfield L := Subfield.closure (C' : Set L) with hK₁
  have hC'K₁ : ∀ c : L, c ∈ C' → c ∈ K₁ := fun c hc => Subfield.subset_closure hc
  have hK₁frac : ∀ x : L, x ∈ K₁ → ∃ a b : L, a ∈ C' ∧ b ∈ C' ∧ b ≠ 0 ∧ x = a / b := by
    intro x hx
    rw [hK₁, Subfield.mem_closure_iff] at hx
    obtain ⟨y, hy, z, hz, rfl⟩ := hx
    rw [Subring.closure_eq] at hy hz
    by_cases hz0 : z = 0
    · exact ⟨0, 1, C'.zero_mem, C'.one_mem, one_ne_zero, by rw [hz0, div_zero, zero_div]⟩
    · exact ⟨y, z, hy, hz, hz0, rfl⟩
  have hnu : ∀ c : ↥C', ¬ IsUnit c → (c : L) ≠ 0 → ((c : ↥C') : L)⁻¹ ∉ A := by
    intro c hc hc0
    have hcm : c ∈ maximalIdeal ↥C' := hc
    rw [hmaxC', Ideal.mem_span_singleton'] at hcm
    obtain ⟨d, hd⟩ := hcm
    exact (residue_eq_zero_iff_inv_not_mem A _ (hC'A _ c.2) hc0).mp ((hϖ' c).mpr ⟨d,
      by rw [← hd, mul_comm]⟩)
  have hAK₁ : ∀ x : L, x ∈ K₁ → x ∈ A → x ∈ C' := by
    intro x hxK hxA
    obtain ⟨a, b, ha, hb, hb0, rfl⟩ := hK₁frac x hxK
    obtain ⟨c, hc | hc⟩ := ValuationRing.cond (⟨a, ha⟩ : ↥C') ⟨b, hb⟩
    · have hcL : a * (c : L) = b := congrArg Subtype.val hc
      by_cases ha0 : a = 0
      · rw [ha0, zero_div]; exact C'.zero_mem
      have hc0 : ((c : ↥C') : L) ≠ 0 := by
        intro h; apply hb0; rw [← hcL, h, mul_zero]
      have hab : a / b = ((c : ↥C') : L)⁻¹ := by
        rw [← hcL, div_mul_eq_div_div, div_self ha0, one_div]
      rw [hab] at hxA ⊢
      by_contra hcon
      exact hnu c (fun hu => hcon (inv_mem_of_isUnit C' c hu)) hc0 hxA
    · have hcL : b * (c : L) = a := congrArg Subtype.val hc
      rw [← hcL, mul_comm, mul_div_assoc, div_self hb0, mul_one]
      exact c.2
  let iCK : ↥C' →+* ↥K₁ :=
    { toFun := fun c => ⟨(c : L), hC'K₁ c c.2⟩
      map_one' := rfl
      map_mul' := fun _ _ => rfl
      map_zero' := rfl
      map_add' := fun _ _ => rfl }
  have hiCK : Function.Injective iCK := by
    intro x y h
    have h' := congrArg (fun z : ↥K₁ => (z : L)) h
    exact Subtype.ext h'
  let algCK : Algebra ↥C' ↥K₁ := iCK.toAlgebra
  have : IsScalarTower ↥C' ↥K₁ L := IsScalarTower.of_algebraMap_eq (fun _ => rfl)
  let E : IntermediateField ↥K₁ L := IntermediateField.adjoin ↥K₁ (↑S : Set L)
  have hEclos : ∀ c : L, c ∈ E ↔ c ∈ Subfield.closure ((C' : Set L) ∪ ↑S) := by
    intro c
    have hr : Set.range (algebraMap (↥K₁) L) = (K₁ : Set L) := by
      ext x; constructor
      · rintro ⟨y, rfl⟩; exact y.2
      · intro hx; exact ⟨⟨x, hx⟩, rfl⟩
    have h2 : Subfield.closure ((K₁ : Set L) ∪ ↑S) = Subfield.closure ((C' : Set L) ∪ ↑S) := by
      apply le_antisymm
      · rw [Subfield.closure_le]
        rintro x (hx | hx)
        · exact Subfield.closure_mono Set.subset_union_left (by rw [hK₁] at hx; exact hx)
        · exact Subfield.subset_closure (Or.inr hx)
      · exact Subfield.closure_mono (Set.union_subset_union_left _ (fun x hx => hC'K₁ x hx))
    rw [← IntermediateField.mem_toSubfield, IntermediateField.adjoin_toSubfield, hr, h2]
  have hint : ∀ s ∈ (↑S : Set L), IsIntegral ↥K₁ s := by
    intro s hs
    exact ((halg s (hS s hs)).extendScalars hiCK).isIntegral
  have hEfin : FiniteDimensional ↥K₁ ↥E := IntermediateField.finiteDimensional_adjoin hint
  have : Algebra.IsSeparable ↥K₁ ↥E := inferInstance
  let algCE : Algebra ↥C' ↥E := ((algebraMap ↥K₁ ↥E).comp iCK).toAlgebra
  have : IsScalarTower ↥C' ↥K₁ ↥E := IsScalarTower.of_algebraMap_eq (fun _ => rfl)
  have : IsScalarTower ↥C' ↥E L := IsScalarTower.of_algebraMap_eq (fun _ => rfl)
  have hfracCK : IsFractionRing ↥C' ↥K₁ := by
    rw [IsFractionRing, isLocalization_iff]
    refine ⟨?_, ?_, ?_⟩
    · rintro ⟨y, hy⟩
      have hy0 : ((y : ↥C') : L) ≠ 0 := fun h => nonZeroDivisors.ne_zero hy (Subtype.ext h)
      exact IsUnit.mk0 _ (fun h => hy0 (congrArg (fun z : ↥K₁ => (z : L)) h))
    · intro z
      obtain ⟨a, b, ha, hb, hb0, hz⟩ := hK₁frac (z : L) z.2
      refine ⟨(⟨a, ha⟩, ⟨⟨b, hb⟩, mem_nonZeroDivisors_of_ne_zero (fun h => hb0 (congrArg
        Subtype.val h))⟩), ?_⟩
      apply Subtype.ext
      change (z : L) * b = a
      rw [hz, div_mul_eq_mul_div, mul_div_assoc, div_self hb0, mul_one]
    · intro x y h
      exact ⟨1, by rw [hiCK h]⟩
  let O' : ValuationSubring ↥E := A.comap (algebraMap ↥E L)
  have hmemO' : ∀ x : ↥E, x ∈ O' ↔ (x : L) ∈ A := fun x => Iff.rfl
  have hO'ne : O' ≠ ⊤ := by
    intro h
    apply hϖ'inv
    have : (algebraMap ↥C' ↥E ϖ')⁻¹ ∈ O' := by rw [h]; exact ValuationSubring.mem_top _
    exact this
  have : Ring.KrullDimLE 1 ↥C' := inferInstance
  have hO'dvr : IsDiscreteValuationRing ↥O' :=
    ValuationSubring.isDiscreteValuationRing_of_algebraMap_mem_of_finite (A := ↥C') (K := ↥K₁) (L
      := ↥E) O'
      (fun c => (hmemO' _).mpr (hC'A c c.2)) hO'ne
  have hEinj : Function.Injective (algebraMap ↥E L) := Subtype.coe_injective
  let C'' : Subring L := O'.toSubring.map (algebraMap ↥E L)
  have hmemC'' : ∀ c : L, c ∈ C'' ↔ c ∈ A ∧ c ∈ E := by
    intro c
    constructor
    · rintro ⟨x, hx, rfl⟩; exact ⟨hx, x.2⟩
    · rintro ⟨hcA, hcE⟩; exact ⟨⟨c, hcE⟩, hcA, rfl⟩
  let eC : ↥O'.toSubring ≃+* ↥C'' := O'.toSubring.equivMapOfInjective (algebraMap ↥E L) hEinj
  have hC''dvr : IsDiscreteValuationRing ↥C'' :=
    IsDiscreteValuationRing.RingEquivClass.isDiscreteValuationRing (A := ↥O') eC
  have hC''A : ∀ c : L, c ∈ C'' → c ∈ A := fun c hc => ((hmemC'' c).mp hc).1
  have hC''E : ∀ c : L, c ∈ C'' → c ∈ E := fun c hc => ((hmemC'' c).mp hc).2
  have hC'C'' : C' ≤ C'' := fun c hc =>
    (hmemC'' c).mpr ⟨hC'A c hc, (hEclos c).mpr (Subfield.subset_closure (Or.inl hc))⟩
  have hSC'' : ∀ s ∈ S, s ∈ C'' := fun s hs =>
    (hmemC'' s).mpr ⟨hS s hs, (hEclos s).mpr (Subfield.subset_closure (Or.inr hs))⟩
  have hunitC'' : ∀ d : ↥C'', (d : L) ≠ 0 → (IsUnit d ↔ ((d : L))⁻¹ ∈ A) := by
    intro d hd0
    constructor
    · intro hu; exact hC''A _ (inv_mem_of_isUnit C'' d hu)
    · intro hi
      have : ((d : L))⁻¹ ∈ C'' := (hmemC'' _).mpr ⟨hi, inv_mem (hC''E _ d.2)⟩
      have := isUnit_of_inv_mem C'' (d : L) d.2 this hd0
      exact this
  have hresC'' : ∀ d : ↥C'', IsLocalRing.residue ↥A ⟨(d : L), hC''A d d.2⟩ = 0 ↔ d ∈ maximalIdeal
    ↥C'' := by
    intro d
    by_cases hd0 : (d : L) = 0
    · have hd : d = 0 := Subtype.ext hd0
      have : (⟨(d : L), hC''A d d.2⟩ : ↥A) = 0 := Subtype.ext hd0
      rw [this, map_zero, hd]
      exact ⟨fun _ => Ideal.zero_mem _, fun _ => rfl⟩
    · rw [residue_eq_zero_iff_inv_not_mem A _ _ hd0, IsLocalRing.mem_maximalIdeal,
        _root_.mem_nonunits_iff, hunitC'' d hd0]
  obtain ⟨ϖ'', hϖ''⟩ := IsDiscreteValuationRing.exists_irreducible ↥C''
  have hmaxC'' : maximalIdeal ↥C'' = Ideal.span {ϖ''} :=
    (IsDiscreteValuationRing.irreducible_iff_uniformizer ϖ'').mp hϖ''
  have hdiv : ∀ d : ↥C'', IsLocalRing.residue ↥A ⟨(d : L), hC''A d d.2⟩ = 0 ↔ ∃ d' : ↥C'', d = ϖ''
    * d' := by
    intro d
    rw [hresC'', hmaxC'', Ideal.mem_span_singleton']
    constructor
    · rintro ⟨a, ha⟩; exact ⟨a, by rw [← ha, mul_comm]⟩
    · rintro ⟨a, ha⟩; exact ⟨a, by rw [ha, mul_comm]⟩
  let p' : ↥C'' := ⟨((ϖ' : ↥C') : L), hC'C'' (ϖ'.2)⟩
  have hp'0 : p' ≠ 0 := fun h => hϖ'L0 (congrArg Subtype.val h)
  have hp'm : p' ∈ maximalIdeal ↥C'' := by
    rw [← hresC'']
    exact (residue_eq_zero_iff_inv_not_mem A _ _ hϖ'L0).mpr hϖ'inv
  obtain ⟨e, u, hue⟩ := IsDiscreteValuationRing.eq_unit_mul_pow_irreducible hp'0 hϖ''
  have he1 : 1 ≤ e := by
    rcases Nat.eq_zero_or_pos e with h | h
    · exfalso
      rw [h, pow_zero, mul_one] at hue
      have : IsUnit p' := hue ▸ u.isUnit
      exact (IsLocalRing.mem_maximalIdeal _).mp hp'm this
    · exact h
  have hv : ∃ v : L, v ∈ C'' ∧ v⁻¹ ∈ C'' ∧ ((ϖ' : ↥C') : L) = v * ((ϖ'' : ↥C'') : L) ^ e := by
    refine ⟨((u : ↥C'') : L), (u : ↥C'').2, inv_mem_of_isUnit C'' _ u.isUnit, ?_⟩
    have := congrArg Subtype.val hue
    simpa only [Subring.coe_mul, Subring.coe_pow] using this
  have : IsIntegrallyClosed ↥C' := inferInstance
  let B : Subalgebra ↥C' ↥E := integralClosure ↥C' ↥E
  have hBfin : Module.Finite ↥C' ↥B := IsIntegralClosure.finite ↥C' ↥K₁ ↥E ↥B
  have hBfrac : IsFractionRing ↥B ↥E := IsIntegralClosure.isFractionRing_of_finite_extension ↥C'
    ↥K₁ ↥E ↥B
  have hBded : IsDedekindDomain ↥B := IsIntegralClosure.isDedekindDomain ↥C' ↥K₁ ↥E ↥B
  let R : Subring L := B.toSubring.map (algebraMap ↥E L)
  have hC'R : C' ≤ R := fun c hc =>
    ⟨algebraMap ↥C' ↥E ⟨c, hc⟩, (mem_integralClosure_iff _ _).mpr isIntegral_algebraMap, rfl⟩
  let iCA : ↥C' →+* ↥A :=
    { toFun := fun c => ⟨(c : L), hC'A c c.2⟩
      map_one' := rfl
      map_mul' := fun _ _ => rfl
      map_zero' := rfl
      map_add' := fun _ _ => rfl }
  let algCA : Algebra ↥C' ↥A := iCA.toAlgebra
  have : IsScalarTower ↥C' ↥A L := IsScalarTower.of_algebraMap_eq (fun _ => rfl)
  have hBA : ∀ x : ↥E, x ∈ B → (x : L) ∈ A := by
    intro x hx
    have h1 : IsIntegral ↥C' (algebraMap ↥E L x) := ((mem_integralClosure_iff _ _).mp hx).algebraMap
    exact mem_of_isIntegral A h1.tower_top
  have hRC'' : R ≤ C'' := by
    rintro r ⟨x, hx, rfl⟩
    exact (hmemC'' _).mpr ⟨hBA x hx, x.2⟩
  have hRfin : (letI : Algebra ↥C' ↥R := (Subring.inclusion hC'R).toAlgebra; Module.Finite ↥C' ↥R)
    := by
    let algCR : Algebra ↥C' ↥R := (Subring.inclusion hC'R).toAlgebra
    let g : ↥B →ₐ[↥C'] ↥R :=
      { toFun := fun x => ⟨((x : ↥E) : L), ⟨(x : ↥E), x.2, rfl⟩⟩
        map_one' := Subtype.ext rfl
        map_mul' := fun x y => Subtype.ext rfl
        map_zero' := Subtype.ext rfl
        map_add' := fun x y => Subtype.ext rfl
        commutes' := fun c => Subtype.ext rfl }
    have hsurj : Function.Surjective g := by
      rintro ⟨r, x, hx, rfl⟩
      exact ⟨⟨x, hx⟩, rfl⟩
    exact Module.Finite.of_surjective g.toLinearMap hsurj
  have hBO' : ∀ b : ↥B, algebraMap ↥B ↥E b ∈ O' := fun b => (hmemO' _).mpr (hBA b b.2)
  have hloc : ∀ c : L, c ∈ C'' → ∃ r s : L, r ∈ R ∧ s ∈ R ∧ s ≠ 0 ∧ s⁻¹ ∈ C'' ∧ c * s = r := by
    intro c hc
    obtain ⟨b, s, hs0, hsu, hcs⟩ := GenLoc.exists_frac_unit_of_mem_valuationSubring O' hBO' hO'ne
      ⟨c, hC''E c hc⟩ ((hmemO' _).mpr (hC''A c hc))
    have hs0E : algebraMap ↥B ↥E s ≠ 0 := (map_ne_zero_iff _ (IsFractionRing.injective ↥B ↥E)).mpr
      hs0
    have hsunit : IsUnit (⟨algebraMap ↥B ↥E s, hBO' s⟩ : ↥O') := by
      by_contra hu
      exact hsu ((ValuationSubring.coe_mem_nonunits_iff (A := O') (a := ⟨_, hBO' s⟩)).2
        ((IsLocalRing.mem_maximalIdeal _).2 hu))
    have hsi : (algebraMap ↥B ↥E s)⁻¹ ∈ O' := inv_mem_of_isUnit O'.toSubring ⟨algebraMap ↥B ↥E s,
      hBO' s⟩ hsunit
    refine ⟨((b : ↥E) : L), ((s : ↥E) : L), ⟨(b : ↥E), b.2, rfl⟩, ⟨(s : ↥E), s.2, rfl⟩,
      fun h => hs0E (Subtype.ext h), (hmemC'' _).mpr ⟨hsi, inv_mem (s : ↥E).2⟩, ?_⟩
    exact congrArg Subtype.val hcs
  exact ⟨C'', inferInstance, hC''dvr, ϖ'', e, R, hC'C'', hC'R, hC''A, hSC'',
    fun c => (hmemC'' c).trans ⟨fun h => ⟨h.1, (hEclos c).mp h.2⟩, fun h => ⟨h.1, (hEclos c).mpr
      h.2⟩⟩,
    hϖ'', hdiv, he1, hv, hRC'', hRfin, hloc⟩