import Mathlib
import Definitions.Def_Mathlib_RingTheory_RegularLocalRingQuotientRegular
import Theorems.Thm_IsRegularLocalRing_isDomain
import Definitions.Def_AlgebraicGeometry_RegularLocalRingRegularSequenceAscent

set_option autoImplicit false
set_option maxHeartbeats 800000
set_option synthInstance.maxHeartbeats 400000

noncomputable section

open IsLocalRing RingTheory
open scoped Pointwise

namespace RegularFlatLocalAscent

universe u v

def quotSpanSingletonEquivQuotSMulTop {R : Type u} [CommRing R] (x : R) :
    (R ⧸ Ideal.span {x}) ≃ₗ[R ⧸ Ideal.span {x}] QuotSMulTop x R :=
  (Submodule.quotEquivOfEq (Ideal.span {x}) (x • (⊤ : Submodule R R))
    (by rw [← Submodule.ideal_span_singleton_smul, Ideal.smul_eq_mul,
      Ideal.mul_top])).extendScalarsOfSurjective Ideal.Quotient.mk_surjective

theorem exists_isWeaklyRegular_ofList_eq_maximalIdeal_aux :
    ∀ (n : ℕ) (R : Type u) [CommRing R] [IsRegularLocalRing R],
      (maximalIdeal R).spanFinrank = n →
      ∃ rs : List R, Ideal.ofList rs = maximalIdeal R ∧ rs.length = n ∧
        Sequence.IsWeaklyRegular R rs := by
  intro n
  induction n with
  | zero =>
    intro R _ _ hn
    refine ⟨[], ?_, rfl, Sequence.IsWeaklyRegular.nil R R⟩
    rw [Ideal.ofList_nil]
    exact ((Submodule.spanFinrank_eq_zero_iff_eq_bot
      ((maximalIdeal R).fg_of_isNoetherianRing)).mp hn).symm
  | succ n ih =>
    intro R _ _ hn

    have hbot : maximalIdeal R ≠ ⊥ := by
      intro h
      have h0 : (maximalIdeal R).spanFinrank = 0 :=
        (Submodule.spanFinrank_eq_zero_iff_eq_bot
          ((maximalIdeal R).fg_of_isNoetherianRing)).mpr h
      omega

    have hne : maximalIdeal R ^ 2 ≠ maximalIdeal R := by
      intro h
      refine hbot (Submodule.eq_bot_of_le_smul_of_le_jacobson_bot (maximalIdeal R)
        (maximalIdeal R) (IsNoetherian.noetherian _) ?_
        (IsLocalRing.maximalIdeal_le_jacobson _))
      rw [Ideal.smul_eq_mul, ← pow_two]
      exact le_of_eq h.symm
    obtain ⟨x, hx, hx2⟩ := SetLike.exists_of_lt
      (lt_of_le_of_ne (Ideal.pow_le_self two_ne_zero) hne)

    haveI hQ : IsRegularLocalRing (R ⧸ Ideal.span {x}) :=
      RegularQuotientEngine.isRegularLocalRing_quotient_span_singleton R hx hx2
    have hdrop : (maximalIdeal (R ⧸ Ideal.span {x})).spanFinrank + 1
        = (maximalIdeal R).spanFinrank :=
      RegularQuotientEngine.spanFinrank_maximalIdeal_quotient_succ_eq R hx hx2
    obtain ⟨rs', hof', hlen', hreg'⟩ := ih (R ⧸ Ideal.span {x}) (by omega)

    have hsurj : Function.Surjective (Ideal.Quotient.mk (Ideal.span {x})) :=
      Ideal.Quotient.mk_surjective
    obtain ⟨lifts, hliftmap, hliftlen⟩ :
        ∃ lifts : List R,
          lifts.map (Ideal.Quotient.mk (Ideal.span {x})) = rs' ∧
            lifts.length = rs'.length := by
      refine ⟨rs'.map (Function.surjInv hsurj), ?_, by rw [List.length_map]⟩
      rw [List.map_map,
        show (⇑(Ideal.Quotient.mk (Ideal.span {x})) ∘ Function.surjInv hsurj) = id from
          funext fun b => Function.surjInv_eq hsurj b,
        List.map_id]
    haveI : IsLocalHom (Ideal.Quotient.mk (Ideal.span {x})) :=
      IsLocalHom.of_surjective _ hsurj

    have hofeq : Ideal.ofList (x :: lifts) = maximalIdeal R := by
      apply le_antisymm
      · rw [Ideal.ofList_cons, sup_le_iff]
        constructor
        · rwa [Ideal.span_le, Set.singleton_subset_iff]
        · refine Ideal.span_le.mpr fun r hr => ?_
          show r ∈ maximalIdeal R
          have hmkmem : Ideal.Quotient.mk (Ideal.span {x}) r
              ∈ maximalIdeal (R ⧸ Ideal.span {x}) := by
            rw [← hof']
            exact Ideal.subset_span (by
              rw [← hliftmap]
              exact List.mem_map.mpr ⟨r, hr, rfl⟩)
          rw [IsLocalRing.mem_maximalIdeal, mem_nonunits_iff] at hmkmem ⊢
          exact fun hu => hmkmem (RingHom.isUnit_map _ hu)
      · intro a ha
        have hanu : ¬IsUnit a := by
          rwa [IsLocalRing.mem_maximalIdeal, mem_nonunits_iff] at ha
        have hmka : Ideal.Quotient.mk (Ideal.span {x}) a
            ∈ Ideal.map (Ideal.Quotient.mk (Ideal.span {x})) (Ideal.ofList lifts) := by
          rw [Ideal.map_ofList, hliftmap, hof', IsLocalRing.mem_maximalIdeal,
            mem_nonunits_iff]
          exact fun hu => hanu (IsUnit.of_map _ a hu)
        have hcomap : a ∈ Ideal.comap (Ideal.Quotient.mk (Ideal.span {x}))
            (Ideal.map (Ideal.Quotient.mk (Ideal.span {x})) (Ideal.ofList lifts)) :=
          Ideal.mem_comap.mpr hmka
        rw [Ideal.comap_map_of_surjective _ hsurj, ← RingHom.ker_eq_comap_bot,
          Ideal.mk_ker, sup_comm (Ideal.ofList lifts) (Ideal.span {x})] at hcomap
        rw [Ideal.ofList_cons]
        exact hcomap

    haveI : IsDomain R := IsRegularLocalRing.isDomain R
    have hx0 : x ≠ 0 := fun h => hx2 (h ▸ Submodule.zero_mem _)
    have hxreg : IsSMulRegular R x :=
      Module.Flat.isSMulRegular_of_nonZeroDivisors (mem_nonZeroDivisors_of_ne_zero hx0)

    have hwR : Sequence.IsWeaklyRegular R (x :: lifts) := by
      rw [Sequence.isWeaklyRegular_cons_iff']
      refine ⟨hxreg, ?_⟩
      rw [hliftmap]
      exact ((quotSpanSingletonEquivQuotSMulTop x).isWeaklyRegular_congr rs').mp hreg'
    refine ⟨x :: lifts, hofeq, ?_, hwR⟩
    rw [List.length_cons, hliftlen, hlen']

theorem exists_isWeaklyRegular_ofList_eq_maximalIdeal (R : Type u) [CommRing R]
    [IsRegularLocalRing R] :
    ∃ rs : List R, Ideal.ofList rs = maximalIdeal R ∧
      rs.length = (maximalIdeal R).spanFinrank ∧ Sequence.IsWeaklyRegular R rs :=
  exists_isWeaklyRegular_ofList_eq_maximalIdeal_aux ((maximalIdeal R).spanFinrank) R rfl

theorem exists_isRegular_ofList_eq_maximalIdeal (R : Type u) [CommRing R]
    [IsRegularLocalRing R] :
    ∃ rs : List R, Ideal.ofList rs = maximalIdeal R ∧
      rs.length = (maximalIdeal R).spanFinrank ∧ Sequence.IsRegular R rs := by
  obtain ⟨rs, hof, hlen, hw⟩ := exists_isWeaklyRegular_ofList_eq_maximalIdeal R
  refine ⟨rs, hof, hlen,
    Sequence.IsRegular.of_isWeaklyRegular_of_mem_maximalIdeal R (fun r hr => ?_) hw⟩
  rw [← hof]
  exact Ideal.subset_span hr

open RegularLocalRingQuotientAscent in

theorem isRegularLocalRing_of_flat_of_isRegularLocalRing_quotient
    (R : Type u) (S : Type v) [CommRing R] [IsRegularLocalRing R] [CommRing S] [Algebra R S]
    [Module.Flat R S] [IsLocalRing S] [IsLocalHom (algebraMap R S)] [IsNoetherianRing S]
    (hfiber : IsRegularLocalRing (S ⧸ Ideal.map (algebraMap R S) (maximalIdeal R))) :
    IsRegularLocalRing S := by
  obtain ⟨rs, hof, -, hreg⟩ := exists_isWeaklyRegular_ofList_eq_maximalIdeal R
  have hwS : Sequence.IsWeaklyRegular S (rs.map (algebraMap R S)) := hreg.of_flat
  have hmem : ∀ s ∈ rs.map (algebraMap R S), s ∈ maximalIdeal S := by
    intro s hs
    obtain ⟨r, hr, rfl⟩ := List.mem_map.mp hs
    have hrm : r ∈ maximalIdeal R := by
      rw [← hof]
      exact Ideal.subset_span hr
    rw [IsLocalRing.mem_maximalIdeal, mem_nonunits_iff] at hrm ⊢
    exact fun hu => hrm (IsUnit.of_map (algebraMap R S) r hu)
  have hid : Ideal.ofList (rs.map (algebraMap R S))
      = Ideal.map (algebraMap R S) (maximalIdeal R) := by
    rw [← Ideal.map_ofList, hof]
  have hquot : IsRegularLocalRing (S ⧸ Ideal.ofList (rs.map (algebraMap R S))) := by
    rw [hid]
    exact hfiber
  exact isRegularLocalRing_of_isRegularLocalRing_quotient_isWeaklyRegular
    (rs.map (algebraMap R S)) hmem hwS hquot

theorem flatLocalAscent_forall :
    ∀ (R : Type u) (S : Type v) [CommRing R] [CommRing S] [IsRegularLocalRing R]
      [Algebra R S] [Module.Flat R S] [IsLocalRing S] [IsLocalHom (algebraMap R S)]
      [IsNoetherianRing S],
      IsRegularLocalRing (S ⧸ Ideal.map (algebraMap R S) (maximalIdeal R)) →
      IsRegularLocalRing S :=
  fun R S _ _ _ _ _ _ _ _ hfiber =>
    isRegularLocalRing_of_flat_of_isRegularLocalRing_quotient R S hfiber

theorem gate_flat_ascent_runs_at_identity (p : ℕ) [Fact p.Prime] :
    IsRegularLocalRing ℤ_[p] := by
  haveI : IsRegularLocalRing ℤ_[p] :=
    RegularLocalRingQuotientAscent.gate_isRegularLocalRing_padicInt_via_sequence p
  haveI : IsNoetherianRing ℤ_[p] := PrincipalIdealRing.isNoetherianRing
  haveI : IsLocalHom (algebraMap ℤ_[p] ℤ_[p]) := by
    rw [Algebra.algebraMap_self]
    exact ⟨fun a h => h⟩
  have hfib : IsRegularLocalRing
      (ℤ_[p] ⧸ Ideal.map (algebraMap ℤ_[p] ℤ_[p]) (maximalIdeal ℤ_[p])) := by
    rw [Algebra.algebraMap_self, Ideal.map_id, PadicInt.maximalIdeal_eq_span_p,
      ← Ideal.ofList_singleton]
    exact RegularLocalRingQuotientAscent.gate_padicInt_quotient_ofList_isRegularLocalRing p
  exact isRegularLocalRing_of_flat_of_isRegularLocalRing_quotient ℤ_[p] ℤ_[p] hfib

theorem not_forall_ascent_dropping_flat :
    ¬ ∀ (R S : Type) [CommRing R] [CommRing S] [IsRegularLocalRing R] [Algebra R S]
        [IsLocalRing S] [IsLocalHom (algebraMap R S)] [IsNoetherianRing S],
        IsRegularLocalRing (S ⧸ Ideal.map (algebraMap R S) (maximalIdeal R)) →
        IsRegularLocalRing S := by
  intro hforall
  haveI : Fact (Nat.Prime 2) := ⟨Nat.prime_two⟩
  haveI : IsRegularLocalRing ℤ_[2] :=
    RegularLocalRingQuotientAscent.gate_isRegularLocalRing_padicInt_via_sequence 2
  haveI : IsNoetherianRing ℤ_[2] := PrincipalIdealRing.isNoetherianRing

  have hspan : maximalIdeal ℤ_[2] = Ideal.span {((2 : ℕ) : ℤ_[2])} :=
    PadicInt.maximalIdeal_eq_span_p
  have h2m : ((2 : ℕ) : ℤ_[2]) ∈ maximalIdeal ℤ_[2] := by
    rw [hspan]
    exact Ideal.mem_span_singleton_self _
  have h4m : ((2 : ℕ) : ℤ_[2]) ^ 2 ∈ maximalIdeal ℤ_[2] :=
    Ideal.pow_mem_of_mem _ h2m 2 two_pos

  haveI : IsLocalRing (ℤ_[2] ⧸ Ideal.span {((2 : ℕ) : ℤ_[2]) ^ 2}) :=
    RegularQuotientEngine.isLocalRing_quotient_span_singleton ℤ_[2] h4m
  haveI : IsLocalHom (algebraMap ℤ_[2] (ℤ_[2] ⧸ Ideal.span {((2 : ℕ) : ℤ_[2]) ^ 2})) := by
    rw [Ideal.Quotient.algebraMap_eq]
    exact IsLocalHom.of_surjective _ Ideal.Quotient.mk_surjective

  have hsup : Ideal.span {((2 : ℕ) : ℤ_[2]) ^ 2} ⊔ maximalIdeal ℤ_[2]
      = Ideal.span {((2 : ℕ) : ℤ_[2])} := by
    rw [hspan]
    refine sup_eq_right.mpr ?_
    rw [Ideal.span_le, Set.singleton_subset_iff]
    exact Ideal.mem_span_singleton.mpr (dvd_pow_self _ two_ne_zero)
  haveI : IsRegularLocalRing (ℤ_[2] ⧸ Ideal.ofList [((2 : ℕ) : ℤ_[2])]) :=
    RegularLocalRingQuotientAscent.gate_padicInt_quotient_ofList_isRegularLocalRing 2
  have hofeq2 : Ideal.ofList [((2 : ℕ) : ℤ_[2])]
      = Ideal.span {((2 : ℕ) : ℤ_[2]) ^ 2} ⊔ maximalIdeal ℤ_[2] := by
    rw [Ideal.ofList_singleton]
    exact hsup.symm
  have hfib : IsRegularLocalRing
      ((ℤ_[2] ⧸ Ideal.span {((2 : ℕ) : ℤ_[2]) ^ 2}) ⧸
        Ideal.map (algebraMap ℤ_[2] (ℤ_[2] ⧸ Ideal.span {((2 : ℕ) : ℤ_[2]) ^ 2}))
          (maximalIdeal ℤ_[2])) := by
    rw [Ideal.Quotient.algebraMap_eq]
    exact IsRegularLocalRing.of_ringEquiv
      ((Ideal.quotEquivOfEq hofeq2).trans
        (DoubleQuot.quotQuotEquivQuotSup _ _).symm)

  have hSreg : IsRegularLocalRing (ℤ_[2] ⧸ Ideal.span {((2 : ℕ) : ℤ_[2]) ^ 2}) :=
    hforall ℤ_[2] (ℤ_[2] ⧸ Ideal.span {((2 : ℕ) : ℤ_[2]) ^ 2}) hfib

  haveI := hSreg
  haveI : IsDomain (ℤ_[2] ⧸ Ideal.span {((2 : ℕ) : ℤ_[2]) ^ 2}) :=
    IsRegularLocalRing.isDomain _
  have hmk0 : (Ideal.Quotient.mk (Ideal.span {((2 : ℕ) : ℤ_[2]) ^ 2}) ((2 : ℕ) : ℤ_[2])) ^ 2
      = 0 := by
    rw [← map_pow, Ideal.Quotient.eq_zero_iff_mem]
    exact Ideal.mem_span_singleton_self _
  have hmkne : Ideal.Quotient.mk (Ideal.span {((2 : ℕ) : ℤ_[2]) ^ 2}) ((2 : ℕ) : ℤ_[2])
      ≠ 0 := by
    rw [ne_eq, Ideal.Quotient.eq_zero_iff_mem, Ideal.mem_span_singleton]
    intro hdvd
    obtain ⟨c, hc⟩ := hdvd
    have h2ne : ((2 : ℕ) : ℤ_[2]) ≠ 0 := Nat.cast_ne_zero.mpr two_ne_zero
    have hcancel : (1 : ℤ_[2]) = ((2 : ℕ) : ℤ_[2]) * c := by
      refine mul_left_cancel₀ h2ne ?_
      rw [mul_one]
      calc ((2 : ℕ) : ℤ_[2]) = ((2 : ℕ) : ℤ_[2]) ^ 2 * c := hc
        _ = ((2 : ℕ) : ℤ_[2]) * (((2 : ℕ) : ℤ_[2]) * c) := by ring
    have h2nu : ¬IsUnit ((2 : ℕ) : ℤ_[2]) := by
      rwa [IsLocalRing.mem_maximalIdeal, mem_nonunits_iff] at h2m
    exact h2nu (IsUnit.of_mul_eq_one c hcancel.symm)
  exact hmkne (pow_eq_zero_iff two_ne_zero |>.mp hmk0)

end RegularFlatLocalAscent

end