import Mathlib
import Definitions.Def_AlgebraicGeometry_RegularLocalRingQuotientNonZeroDivisorAscent

set_option autoImplicit false
set_option maxHeartbeats 800000
set_option synthInstance.maxHeartbeats 400000

noncomputable section

open IsLocalRing RingTheory Pointwise

namespace RegularLocalRingQuotientAscent

universe u

section Preliminaries

variable {A : Type*} [CommRing A]

theorem mem_nonZeroDivisors_of_isSMulRegular {x : A} (h : IsSMulRegular A x) :
    x ∈ nonZeroDivisors A := by
  rw [mem_nonZeroDivisors_iff]
  constructor
  · intro a ha
    apply h
    simp only [smul_eq_mul, mul_zero]
    exact ha
  · intro a ha
    apply h
    simp only [smul_eq_mul, mul_zero]
    rw [mul_comm]
    exact ha

theorem ofList_ne_top_of_isRegular {rs : List A} (h : Sequence.IsRegular A rs) :
    Ideal.ofList rs ≠ ⊤ := by
  intro htop
  apply h.top_ne_smul
  rw [htop]
  simp

theorem mem_maximalIdeal_of_isRegular [IsLocalRing A] {rs : List A}
    (h : Sequence.IsRegular A rs) :
    ∀ r ∈ rs, r ∈ maximalIdeal A := fun _ hr =>
  IsLocalRing.le_maximalIdeal (ofList_ne_top_of_isRegular h) (Ideal.subset_span hr)

theorem spanFinrank_ofList_le_length (rs : List A) :
    (Ideal.ofList rs).spanFinrank ≤ rs.length := by
  classical

  have hset : {r : A | r ∈ rs} = (↑rs.toFinset : Set A) := by
    ext r
    simp
  have hfin : Set.Finite {r : A | r ∈ rs} := by
    rw [hset]
    exact rs.toFinset.finite_toSet
  have hcard : ({r : A | r ∈ rs}).ncard ≤ rs.length := by
    rw [hset, Set.ncard_coe_finset]
    exact rs.toFinset_card_le

  have hspan : (Submodule.span A {r : A | r ∈ rs}).spanFinrank ≤ ({r : A | r ∈ rs}).ncard :=
    Submodule.spanFinrank_span_le_ncard_of_finite hfin
  rw [Ideal.submodule_span_eq] at hspan
  exact hspan.trans hcard

end Preliminaries

section Ascent

variable {A : Type*} [CommRing A] [IsLocalRing A] [IsNoetherianRing A]

theorem spanFinrank_maximalIdeal_le_quotient_ofList_add_length (rs : List A)
    [IsLocalRing (A ⧸ Ideal.ofList rs)] :
    (maximalIdeal A).spanFinrank
      ≤ (maximalIdeal (A ⧸ Ideal.ofList rs)).spanFinrank + rs.length := by

  have hker_eq : RingHom.ker (Ideal.Quotient.mk (Ideal.ofList rs)) = Ideal.ofList rs :=
    Ideal.mk_ker
  have hkerfg : Submodule.FG (RingHom.ker (Ideal.Quotient.mk (Ideal.ofList rs))) := by
    rw [hker_eq]
    exact IsNoetherian.noetherian _
  have hker_le : (RingHom.ker (Ideal.Quotient.mk (Ideal.ofList rs))).spanFinrank
      ≤ rs.length := by
    rw [hker_eq]
    exact spanFinrank_ofList_le_length rs

  have h1 := spanFinrank_maximalIdeal_le_of_surjective (Ideal.Quotient.mk (Ideal.ofList rs))
    Ideal.Quotient.mk_surjective hkerfg
  omega

theorem isRegularLocalRing_of_isRegularLocalRing_quotient_ofList (rs : List A)
    (hreg : Sequence.IsRegular A rs)
    (hquot : IsRegularLocalRing (A ⧸ Ideal.ofList rs)) :
    IsRegularLocalRing A := by
  haveI := hquot

  have hkey : (maximalIdeal A).spanFinrank
      ≤ (maximalIdeal (A ⧸ Ideal.ofList rs)).spanFinrank + rs.length :=
    spanFinrank_maximalIdeal_le_quotient_ofList_add_length rs

  have hq : ((maximalIdeal (A ⧸ Ideal.ofList rs)).spanFinrank : WithBot ℕ∞)
      = ringKrullDim (A ⧸ Ideal.ofList rs) := hquot.spanFinrank_maximalIdeal

  have hdim : ringKrullDim (A ⧸ Ideal.ofList rs) + rs.length = ringKrullDim A :=
    ringKrullDim_add_length_eq_ringKrullDim_of_isRegular rs hreg

  refine IsRegularLocalRing.of_spanFinrank_maximalIdeal_le A ?_
  rw [← hdim, ← hq]
  exact_mod_cast hkey

theorem isRegularLocalRing_of_isRegularLocalRing_quotient_isWeaklyRegular (rs : List A)
    (hmem : ∀ r ∈ rs, r ∈ maximalIdeal A)
    (hreg : Sequence.IsWeaklyRegular A rs)
    (hquot : IsRegularLocalRing (A ⧸ Ideal.ofList rs)) :
    IsRegularLocalRing A :=
  isRegularLocalRing_of_isRegularLocalRing_quotient_ofList rs
    (Sequence.IsRegular.of_isWeaklyRegular_of_mem_maximalIdeal A hmem hreg) hquot

theorem isRegularLocalRing_of_isRegularLocalRing_quotient_regularSequence (rs : List A)
    (hmem : ∀ r ∈ rs, r ∈ maximalIdeal A)
    (hreg : Sequence.IsRegular A rs)
    (hquot : IsRegularLocalRing (A ⧸ Ideal.ofList rs)) :
    IsRegularLocalRing A :=
  isRegularLocalRing_of_isRegularLocalRing_quotient_isWeaklyRegular rs hmem
    hreg.toIsWeaklyRegular hquot

theorem isRegularLocalRing_of_surjective_ker_ofList {B : Type*} [CommRing B]
    (f : A →+* B) (hf : Function.Surjective f) (rs : List A)
    (hker : RingHom.ker f = Ideal.ofList rs)
    (hreg : Sequence.IsRegular A rs)
    (hB : IsRegularLocalRing B) :
    IsRegularLocalRing A := by
  haveI := hB

  have e : (A ⧸ Ideal.ofList rs) ≃+* B :=
    (Ideal.quotEquivOfEq hker.symm).trans (RingHom.quotientKerEquivOfSurjective hf)
  exact isRegularLocalRing_of_isRegularLocalRing_quotient_ofList rs hreg
    (IsRegularLocalRing.of_ringEquiv e.symm)

end Ascent

section IteratedAscent

theorem isRegularLocalRing_of_isRegularLocalRing_quotient_ofList_iterated :
    ∀ (n : ℕ) (A : Type u) [CommRing A] [IsLocalRing A] [IsNoetherianRing A] (rs : List A),
      rs.length = n → Sequence.IsRegular A rs →
      IsRegularLocalRing (A ⧸ Ideal.ofList rs) → IsRegularLocalRing A := by
  intro n
  induction n with
  | zero =>
    intro A _ _ _ rs hlen hreg hquot
    cases rs with
    | nil =>

      rw [Ideal.ofList_nil] at hquot
      haveI := hquot
      exact IsRegularLocalRing.of_ringEquiv (RingEquiv.quotientBot A)
    | cons x rest => exact absurd hlen (by simp)
  | succ n IH =>
    intro A _ _ _ rs hlen hreg hquot
    cases rs with
    | nil => exact absurd hlen (by simp)
    | cons x rest =>
      have hrestlen : rest.length = n := by simpa using hlen

      obtain ⟨hxreg, hrestreg⟩ := (Sequence.isRegular_cons_iff' A x rest).mp hreg

      have hxm : x ∈ maximalIdeal A :=
        mem_maximalIdeal_of_isRegular hreg x (by simp)
      have hxnzd : x ∈ nonZeroDivisors A := mem_nonZeroDivisors_of_isSMulRegular hxreg

      have hxne : Ideal.span {x} ≠ ⊤ := by
        rw [Ne, Ideal.span_singleton_eq_top]
        intro hu
        exact (maximalIdeal.isMaximal A).ne_top (Ideal.eq_top_of_isUnit_mem _ hxm hu)
      haveI : Nontrivial (A ⧸ Ideal.span {x}) := Ideal.Quotient.nontrivial_iff.mpr hxne
      haveI : IsLocalRing (A ⧸ Ideal.span {x}) :=
        IsLocalRing.of_surjective' (Ideal.Quotient.mk (Ideal.span {x}))
          Ideal.Quotient.mk_surjective

      have hsub : (Ideal.span {x} : Submodule A A) = x • (⊤ : Submodule A A) := by
        rw [← Submodule.ideal_span_singleton_smul]
        simp
      have e' : (A ⧸ Ideal.span {x}) ≃ₗ[A ⧸ Ideal.span {x}] QuotSMulTop x A :=
        LinearEquiv.extendScalarsOfSurjective
          (by rw [Ideal.Quotient.algebraMap_eq]; exact Ideal.Quotient.mk_surjective)
          (Submodule.quotEquivOfEq _ _ hsub)
      have hrestreg' : Sequence.IsRegular (A ⧸ Ideal.span {x})
          (rest.map (Ideal.Quotient.mk (Ideal.span {x}))) :=
        (LinearEquiv.isRegular_congr e' _).mpr hrestreg

      have hquot' : IsRegularLocalRing ((A ⧸ Ideal.span {x}) ⧸
          Ideal.ofList (rest.map (Ideal.Quotient.mk (Ideal.span {x})))) := by
        haveI := hquot
        refine IsRegularLocalRing.of_ringEquiv (R := A ⧸ Ideal.ofList (x :: rest)) ?_
        exact (Ideal.quotEquivOfEq (Ideal.ofList_cons x rest)).trans
          (((DoubleQuot.quotQuotEquivQuotSup (Ideal.span {x}) (Ideal.ofList rest)).symm).trans
            (Ideal.quotEquivOfEq (Ideal.map_ofList _ _)))

      have hB : IsRegularLocalRing (A ⧸ Ideal.span {x}) :=
        IH (A ⧸ Ideal.span {x}) (rest.map (Ideal.Quotient.mk (Ideal.span {x})))
          (by rw [List.length_map]; exact hrestlen) hrestreg' hquot'

      exact isRegularLocalRing_of_isRegularLocalRing_quotient hxm hxnzd hB

theorem isRegularLocalRing_of_isRegularLocalRing_quotient_ofList_via_iterated_ascent
    {A : Type u} [CommRing A] [IsLocalRing A] [IsNoetherianRing A] (rs : List A)
    (hreg : Sequence.IsRegular A rs)
    (hquot : IsRegularLocalRing (A ⧸ Ideal.ofList rs)) :
    IsRegularLocalRing A :=
  isRegularLocalRing_of_isRegularLocalRing_quotient_ofList_iterated rs.length A rs rfl
    hreg hquot

end IteratedAscent

section Gates

variable (p : ℕ) [Fact p.Prime]

theorem gate_padicInt_isRegular_singleton_p :
    Sequence.IsRegular ℤ_[p] [(p : ℤ_[p])] := by
  haveI : IsNoetherianRing ℤ_[p] := PrincipalIdealRing.isNoetherianRing
  apply Sequence.IsRegular.of_isWeaklyRegular_of_mem_maximalIdeal
  · intro r hr
    rw [List.mem_singleton] at hr
    subst hr
    rw [PadicInt.maximalIdeal_eq_span_p]
    exact Ideal.mem_span_singleton_self _
  · rw [Sequence.isWeaklyRegular_singleton_iff]
    exact Module.Flat.isSMulRegular_of_nonZeroDivisors
      (mem_nonZeroDivisors_of_ne_zero
        (Nat.cast_ne_zero.mpr (Fact.out (p := p.Prime)).ne_zero))

theorem gate_padicInt_quotient_ofList_isRegularLocalRing :
    IsRegularLocalRing (ℤ_[p] ⧸ Ideal.ofList [(p : ℤ_[p])]) := by
  rw [Ideal.ofList_singleton]
  exact IsRegularLocalRing.of_ringEquiv (padicIntQuotientSpanPEquiv p).symm

theorem gate_isRegularLocalRing_padicInt_via_sequence : IsRegularLocalRing ℤ_[p] := by
  haveI : IsNoetherianRing ℤ_[p] := PrincipalIdealRing.isNoetherianRing
  exact isRegularLocalRing_of_isRegularLocalRing_quotient_ofList _
    (gate_padicInt_isRegular_singleton_p p)
    (gate_padicInt_quotient_ofList_isRegularLocalRing p)

theorem gate_isRegularLocalRing_padicInt_via_iterated_ascent : IsRegularLocalRing ℤ_[p] := by
  haveI : IsNoetherianRing ℤ_[p] := PrincipalIdealRing.isNoetherianRing
  exact isRegularLocalRing_of_isRegularLocalRing_quotient_ofList_via_iterated_ascent _
    (gate_padicInt_isRegular_singleton_p p)
    (gate_padicInt_quotient_ofList_isRegularLocalRing p)

theorem gate_padicInt_dimension_jump_length :
    ringKrullDim (ℤ_[p] ⧸ Ideal.ofList [(p : ℤ_[p])])
      + ([(p : ℤ_[p])].length : WithBot ℕ∞) = ringKrullDim ℤ_[p] := by
  haveI : IsNoetherianRing ℤ_[p] := PrincipalIdealRing.isNoetherianRing
  exact ringKrullDim_add_length_eq_ringKrullDim_of_isRegular _
    (gate_padicInt_isRegular_singleton_p p)

end Gates

section Teeth

theorem not_isRegular_dualNumber_singleton_eps :
    ¬ Sequence.IsRegular (DualNumber ℚ) [(DualNumber.eps : DualNumber ℚ)] := by
  intro h
  obtain ⟨h1, -⟩ := (Sequence.isRegular_cons_iff' (DualNumber ℚ) DualNumber.eps []).mp h
  exact eps_notMem_nonZeroDivisors (mem_nonZeroDivisors_of_isSMulRegular h1)

theorem not_forall_isRegularLocalRing_of_quotient_ofList_dropping_isRegular :
    ¬ (∀ (A : Type) [CommRing A] [IsLocalRing A] [IsNoetherianRing A] (rs : List A),
        (∀ r ∈ rs, r ∈ maximalIdeal A) → IsRegularLocalRing (A ⧸ Ideal.ofList rs) →
        IsRegularLocalRing A) := by
  intro hclaim
  haveI : IsNoetherianRing (DualNumber ℚ) := PrincipalIdealRing.isNoetherianRing
  refine not_isRegularLocalRing_dualNumber
    (hclaim (DualNumber ℚ) [DualNumber.eps] ?_ ?_)
  · intro r hr
    rw [List.mem_singleton] at hr
    subst hr
    exact eps_mem_maximalIdeal
  · rw [Ideal.ofList_singleton]
    exact quotient_span_eps_isRegularLocalRing

end Teeth

end RegularLocalRingQuotientAscent

/--
info: 'RegularLocalRingQuotientAscent.mem_nonZeroDivisors_of_isSMulRegular' depends on axioms: [propext, Quot.sound]
-/
#guard_msgs in
#print axioms RegularLocalRingQuotientAscent.mem_nonZeroDivisors_of_isSMulRegular

/--
info: 'RegularLocalRingQuotientAscent.ofList_ne_top_of_isRegular' depends on axioms: [propext, Classical.choice, Quot.sound]
-/
#guard_msgs in
#print axioms RegularLocalRingQuotientAscent.ofList_ne_top_of_isRegular

/--
info: 'RegularLocalRingQuotientAscent.mem_maximalIdeal_of_isRegular' depends on axioms: [propext,
 Classical.choice,
 Quot.sound]
-/
#guard_msgs in
#print axioms RegularLocalRingQuotientAscent.mem_maximalIdeal_of_isRegular

/--
info: 'RegularLocalRingQuotientAscent.spanFinrank_ofList_le_length' depends on axioms: [propext, Classical.choice, Quot.sound]
-/
#guard_msgs in
#print axioms RegularLocalRingQuotientAscent.spanFinrank_ofList_le_length

/--
info: 'RegularLocalRingQuotientAscent.spanFinrank_maximalIdeal_le_quotient_ofList_add_length' depends on axioms: [propext,
 Classical.choice,
 Quot.sound]
-/
#guard_msgs in
#print axioms RegularLocalRingQuotientAscent.spanFinrank_maximalIdeal_le_quotient_ofList_add_length

/--
info: 'RegularLocalRingQuotientAscent.isRegularLocalRing_of_isRegularLocalRing_quotient_ofList' depends on axioms: [propext,
 Classical.choice,
 Quot.sound]
-/
#guard_msgs in
#print axioms RegularLocalRingQuotientAscent.isRegularLocalRing_of_isRegularLocalRing_quotient_ofList

/--
info: 'RegularLocalRingQuotientAscent.isRegularLocalRing_of_isRegularLocalRing_quotient_isWeaklyRegular' depends on axioms: [propext,
 Classical.choice,
 Quot.sound]
-/
#guard_msgs in
#print axioms RegularLocalRingQuotientAscent.isRegularLocalRing_of_isRegularLocalRing_quotient_isWeaklyRegular

/--
info: 'RegularLocalRingQuotientAscent.isRegularLocalRing_of_isRegularLocalRing_quotient_regularSequence' depends on axioms: [propext,
 Classical.choice,
 Quot.sound]
-/
#guard_msgs in
#print axioms RegularLocalRingQuotientAscent.isRegularLocalRing_of_isRegularLocalRing_quotient_regularSequence

/--
info: 'RegularLocalRingQuotientAscent.isRegularLocalRing_of_surjective_ker_ofList' depends on axioms: [propext,
 Classical.choice,
 Quot.sound]
-/
#guard_msgs in
#print axioms RegularLocalRingQuotientAscent.isRegularLocalRing_of_surjective_ker_ofList

/--
info: 'RegularLocalRingQuotientAscent.isRegularLocalRing_of_isRegularLocalRing_quotient_ofList_iterated' depends on axioms: [propext,
 Classical.choice,
 Quot.sound]
-/
#guard_msgs in
#print axioms RegularLocalRingQuotientAscent.isRegularLocalRing_of_isRegularLocalRing_quotient_ofList_iterated

/--
info: 'RegularLocalRingQuotientAscent.isRegularLocalRing_of_isRegularLocalRing_quotient_ofList_via_iterated_ascent' depends on axioms: [propext,
 Classical.choice,
 Quot.sound]
-/
#guard_msgs in
#print axioms RegularLocalRingQuotientAscent.isRegularLocalRing_of_isRegularLocalRing_quotient_ofList_via_iterated_ascent

/--
info: 'RegularLocalRingQuotientAscent.gate_padicInt_isRegular_singleton_p' depends on axioms: [propext,
 Classical.choice,
 Quot.sound]
-/
#guard_msgs in
#print axioms RegularLocalRingQuotientAscent.gate_padicInt_isRegular_singleton_p

/--
info: 'RegularLocalRingQuotientAscent.gate_padicInt_quotient_ofList_isRegularLocalRing' depends on axioms: [propext,
 Classical.choice,
 Quot.sound]
-/
#guard_msgs in
#print axioms RegularLocalRingQuotientAscent.gate_padicInt_quotient_ofList_isRegularLocalRing

/--
info: 'RegularLocalRingQuotientAscent.gate_isRegularLocalRing_padicInt_via_sequence' depends on axioms: [propext,
 Classical.choice,
 Quot.sound]
-/
#guard_msgs in
#print axioms RegularLocalRingQuotientAscent.gate_isRegularLocalRing_padicInt_via_sequence

/--
info: 'RegularLocalRingQuotientAscent.gate_isRegularLocalRing_padicInt_via_iterated_ascent' depends on axioms: [propext,
 Classical.choice,
 Quot.sound]
-/
#guard_msgs in
#print axioms RegularLocalRingQuotientAscent.gate_isRegularLocalRing_padicInt_via_iterated_ascent

/--
info: 'RegularLocalRingQuotientAscent.gate_padicInt_dimension_jump_length' depends on axioms: [propext,
 Classical.choice,
 Quot.sound]
-/
#guard_msgs in
#print axioms RegularLocalRingQuotientAscent.gate_padicInt_dimension_jump_length

/--
info: 'RegularLocalRingQuotientAscent.not_isRegular_dualNumber_singleton_eps' depends on axioms: [propext,
 Classical.choice,
 Quot.sound]
-/
#guard_msgs in
#print axioms RegularLocalRingQuotientAscent.not_isRegular_dualNumber_singleton_eps

/--
info: 'RegularLocalRingQuotientAscent.not_forall_isRegularLocalRing_of_quotient_ofList_dropping_isRegular' depends on axioms: [propext,
 Classical.choice,
 Quot.sound]
-/
#guard_msgs in
#print axioms RegularLocalRingQuotientAscent.not_forall_isRegularLocalRing_of_quotient_ofList_dropping_isRegular

end