import Mathlib

set_option autoImplicit false

noncomputable section

open IsLocalRing

namespace RegularLocalRingQuotientAscent

section GeneratorCounting

variable {A B : Type*} [CommRing A] [CommRing B]

theorem spanFinrank_comap_le_of_surjective {f : A →+* B} (hf : Function.Surjective f)
    {J : Ideal B} (hJ : Submodule.FG J) (hker : Submodule.FG (RingHom.ker f)) :
    (J.comap f).spanFinrank ≤ J.spanFinrank + (RingHom.ker f).spanFinrank := by
  classical
  obtain ⟨s, hscard, hsspan⟩ := Submodule.FG.exists_span_finset_card_eq_spanFinrank hJ
  obtain ⟨t, htcard, htspan⟩ := Submodule.FG.exists_span_finset_card_eq_spanFinrank hker
  rw [Ideal.submodule_span_eq] at hsspan htspan

  set S : Finset A := s.image (Function.surjInv hf) with hSdef
  have hfS : ⇑f '' (S : Set A) = (s : Set B) := by
    rw [hSdef, Finset.coe_image, Set.image_image]
    simp [Function.surjInv_eq hf]

  have h1 : Ideal.map f (Ideal.span (S : Set A)) = J := by
    rw [Ideal.map_span, hfS, hsspan]
  have hcomap : J.comap f = Ideal.span (((S ∪ t : Finset A)) : Set A) := by
    calc J.comap f
        = (Ideal.map f (Ideal.span (S : Set A))).comap f := by rw [h1]
      _ = Ideal.span (S : Set A) ⊔ Ideal.comap f ⊥ :=
          Ideal.comap_map_of_surjective f hf _
      _ = Ideal.span (S : Set A) ⊔ RingHom.ker f := by
          rw [← RingHom.ker_eq_comap_bot]
      _ = Ideal.span (S : Set A) ⊔ Ideal.span (t : Set A) := by
          rw [htspan]
      _ = Ideal.span ((S : Set A) ∪ (t : Set A)) := (Ideal.span_union _ _).symm
      _ = Ideal.span (((S ∪ t : Finset A)) : Set A) := by rw [Finset.coe_union]
  rw [hcomap]
  calc (Ideal.span (((S ∪ t : Finset A)) : Set A)).spanFinrank
      ≤ (((S ∪ t : Finset A)) : Set A).ncard :=
        Submodule.spanFinrank_span_le_ncard_of_finite (S ∪ t).finite_toSet
    _ = (S ∪ t).card := Set.ncard_coe_finset _
    _ ≤ S.card + t.card := Finset.card_union_le _ _
    _ ≤ s.card + t.card := by
        have hS : S.card ≤ s.card := Finset.card_image_le
        omega
    _ = J.spanFinrank + (RingHom.ker f).spanFinrank := by rw [hscard, htcard]

theorem spanFinrank_maximalIdeal_le_of_surjective [IsLocalRing A] [IsLocalRing B]
    [IsNoetherianRing B] (f : A →+* B) (hf : Function.Surjective f)
    (hker : Submodule.FG (RingHom.ker f)) :
    (maximalIdeal A).spanFinrank ≤ (maximalIdeal B).spanFinrank + (RingHom.ker f).spanFinrank := by
  haveI : IsLocalHom f := IsLocalHom.of_surjective f hf
  have hcomap : Ideal.comap f (maximalIdeal B) = maximalIdeal A :=
    IsLocalRing.maximalIdeal_comap f
  calc (maximalIdeal A).spanFinrank
      = (Ideal.comap f (maximalIdeal B)).spanFinrank := by rw [hcomap]
    _ ≤ (maximalIdeal B).spanFinrank + (RingHom.ker f).spanFinrank :=
        spanFinrank_comap_le_of_surjective hf (IsNoetherian.noetherian _) hker

theorem finrank_cotangentSpace_le_of_surjective [IsLocalRing A] [IsLocalRing B]
    [IsNoetherianRing A] [IsNoetherianRing B] (f : A →+* B) (hf : Function.Surjective f) :
    Module.finrank (ResidueField A) (CotangentSpace A)
      ≤ Module.finrank (ResidueField B) (CotangentSpace B) + (RingHom.ker f).spanFinrank := by
  rw [← IsLocalRing.spanFinrank_maximalIdeal_eq_finrank_cotangentSpace A,
    ← IsLocalRing.spanFinrank_maximalIdeal_eq_finrank_cotangentSpace B]
  exact spanFinrank_maximalIdeal_le_of_surjective f hf (IsNoetherian.noetherian _)

end GeneratorCounting

section Ascent

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

theorem isRegularLocalRing_of_isRegularLocalRing_quotient {x : A} (hx : x ∈ maximalIdeal A)
    (hnzd : x ∈ nonZeroDivisors A)
    (hquot : IsRegularLocalRing (A ⧸ Ideal.span {x})) :
    IsRegularLocalRing A := by
  haveI := hquot

  have hker_eq : RingHom.ker (Ideal.Quotient.mk (Ideal.span {x})) = Ideal.span {x} := Ideal.mk_ker
  have hkerfg : Submodule.FG (RingHom.ker (Ideal.Quotient.mk (Ideal.span {x}))) := by
    rw [hker_eq]
    exact Submodule.fg_span (Set.finite_singleton x)
  have hker_le_one : (RingHom.ker (Ideal.Quotient.mk (Ideal.span {x}))).spanFinrank ≤ 1 := by
    rw [hker_eq]
    calc (Ideal.span {x}).spanFinrank
        ≤ ({x} : Set A).ncard :=
          Submodule.spanFinrank_span_le_ncard_of_finite (Set.finite_singleton x)
      _ = 1 := Set.ncard_singleton x

  have hkey : (maximalIdeal A).spanFinrank
      ≤ (maximalIdeal (A ⧸ Ideal.span {x})).spanFinrank + 1 := by
    have h1 := spanFinrank_maximalIdeal_le_of_surjective (Ideal.Quotient.mk (Ideal.span {x}))
      Ideal.Quotient.mk_surjective hkerfg
    omega

  have hq : ((maximalIdeal (A ⧸ Ideal.span {x})).spanFinrank : WithBot ℕ∞)
      = ringKrullDim (A ⧸ Ideal.span {x}) := hquot.spanFinrank_maximalIdeal

  have hdim : ringKrullDim (A ⧸ Ideal.span {x}) + 1 = ringKrullDim A :=
    ringKrullDim_quotient_span_singleton_succ_eq_ringKrullDim_of_mem_nonZeroDivisors hnzd hx

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

theorem isRegularLocalRing_of_surjective_ker_span_singleton {B : Type*} [CommRing B]
    (f : A →+* B) (hf : Function.Surjective f) {x : A}
    (hker : RingHom.ker f = Ideal.span {x}) (hx : x ∈ maximalIdeal A)
    (hnzd : x ∈ nonZeroDivisors A) (hB : IsRegularLocalRing B) :
    IsRegularLocalRing A := by
  haveI := hB

  have e : (A ⧸ Ideal.span {x}) ≃+* B :=
    (Ideal.quotEquivOfEq hker.symm).trans (RingHom.quotientKerEquivOfSurjective hf)
  exact isRegularLocalRing_of_isRegularLocalRing_quotient hx hnzd
    (IsRegularLocalRing.of_ringEquiv e.symm)

end Ascent

section Gates

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

def padicIntQuotientSpanPEquiv : (ℤ_[p] ⧸ Ideal.span {(p : ℤ_[p])}) ≃+* ZMod p :=
  (Ideal.quotEquivOfEq (by rw [PadicInt.ker_toZMod, PadicInt.maximalIdeal_eq_span_p])).trans
    (RingHom.quotientKerEquivOfSurjective (ZMod.ringHom_surjective PadicInt.toZMod))

theorem gate_padicInt_hypotheses :
    (p : ℤ_[p]) ∈ maximalIdeal ℤ_[p] ∧ (p : ℤ_[p]) ∈ nonZeroDivisors ℤ_[p] ∧
      IsRegularLocalRing (ℤ_[p] ⧸ Ideal.span {(p : ℤ_[p])}) := by
  refine ⟨?_, ?_, ?_⟩
  · rw [PadicInt.maximalIdeal_eq_span_p]
    exact Ideal.mem_span_singleton_self _
  · exact mem_nonZeroDivisors_of_ne_zero
      (Nat.cast_ne_zero.mpr (Fact.out (p := p.Prime)).ne_zero)
  · exact IsRegularLocalRing.of_ringEquiv (padicIntQuotientSpanPEquiv p).symm

theorem gate_isRegularLocalRing_padicInt : IsRegularLocalRing ℤ_[p] := by
  haveI : IsNoetherianRing ℤ_[p] := PrincipalIdealRing.isNoetherianRing
  obtain ⟨h1, h2, h3⟩ := gate_padicInt_hypotheses p
  exact isRegularLocalRing_of_isRegularLocalRing_quotient h1 h2 h3

theorem gate_padicInt_conclusion_consistency : IsRegularLocalRing ℤ_[p] := by
  haveI : IsNoetherianRing ℤ_[p] := PrincipalIdealRing.isNoetherianRing
  infer_instance

theorem gate_padicInt_dimension_jump :
    ringKrullDim (ℤ_[p] ⧸ Ideal.span {(p : ℤ_[p])}) + 1 = ringKrullDim ℤ_[p] := by
  haveI : IsNoetherianRing ℤ_[p] := PrincipalIdealRing.isNoetherianRing
  obtain ⟨h1, h2, _⟩ := gate_padicInt_hypotheses p
  exact ringKrullDim_quotient_span_singleton_succ_eq_ringKrullDim_of_mem_nonZeroDivisors h2 h1

end Gates

section Teeth

def dualNumberFst (K : Type*) [CommRing K] : DualNumber K →+* K where
  toFun := TrivSqZeroExt.fst
  map_one' := TrivSqZeroExt.fst_one
  map_mul' := TrivSqZeroExt.fst_mul
  map_zero' := TrivSqZeroExt.fst_zero
  map_add' := TrivSqZeroExt.fst_add

@[simp] theorem dualNumberFst_apply (K : Type*) [CommRing K] (x : DualNumber K) :
    dualNumberFst K x = TrivSqZeroExt.fst x := rfl

theorem ker_dualNumberFst (K : Type*) [CommRing K] :
    RingHom.ker (dualNumberFst K) = Ideal.span {(DualNumber.eps : DualNumber K)} := by
  ext x
  rw [RingHom.mem_ker, Ideal.mem_span_singleton, dualNumberFst_apply]
  exact DualNumber.fst_eq_zero_iff_eps_dvd

theorem dualNumberFst_surjective (K : Type*) [CommRing K] :
    Function.Surjective (dualNumberFst K) :=
  fun r => ⟨TrivSqZeroExt.inl r, TrivSqZeroExt.fst_inl K r⟩

def dualNumberQuotientSpanEpsEquiv (K : Type*) [CommRing K] :
    (DualNumber K ⧸ Ideal.span {(DualNumber.eps : DualNumber K)}) ≃+* K :=
  (Ideal.quotEquivOfEq (ker_dualNumberFst K).symm).trans
    (RingHom.quotientKerEquivOfSurjective (dualNumberFst_surjective K))

theorem quotient_span_eps_isRegularLocalRing :
    IsRegularLocalRing (DualNumber ℚ ⧸ Ideal.span {(DualNumber.eps : DualNumber ℚ)}) :=
  IsRegularLocalRing.of_ringEquiv (dualNumberQuotientSpanEpsEquiv ℚ).symm

theorem eps_ne_zero : (DualNumber.eps : DualNumber ℚ) ≠ 0 := by
  intro heq
  have h1 := congrArg TrivSqZeroExt.snd heq
  simp at h1

theorem eps_notMem_nonZeroDivisors :
    (DualNumber.eps : DualNumber ℚ) ∉ nonZeroDivisors (DualNumber ℚ) := by
  intro h
  exact eps_ne_zero
    ((mem_nonZeroDivisors_iff.mp h).2 DualNumber.eps DualNumber.eps_mul_eps)

theorem eps_mem_maximalIdeal :
    (DualNumber.eps : DualNumber ℚ) ∈ maximalIdeal (DualNumber ℚ) := by
  rw [DualNumber.maximalIdeal_eq_span_singleton_eps]
  exact Ideal.mem_span_singleton_self _

theorem not_isRegularLocalRing_dualNumber : ¬ IsRegularLocalRing (DualNumber ℚ) := by
  intro h

  have hnil : nilradical (DualNumber ℚ) = Ideal.span {(DualNumber.eps : DualNumber ℚ)} := by
    rcases DualNumber.ideal_trichotomy (nilradical (DualNumber ℚ)) with h0 | h1 | h2
    · exfalso
      have hin : (DualNumber.eps : DualNumber ℚ) ∈ nilradical (DualNumber ℚ) :=
        mem_nilradical.mpr DualNumber.isNilpotent_eps
      rw [h0] at hin
      exact eps_ne_zero (by simpa using hin)
    · exact h1
    · exfalso
      have hone : IsNilpotent (1 : DualNumber ℚ) :=
        mem_nilradical.mp (h2 ▸ Submodule.mem_top)
      obtain ⟨n, hn⟩ := hone
      rw [one_pow] at hn
      exact one_ne_zero hn
  haveI : (nilradical (DualNumber ℚ)).IsMaximal := by
    rw [hnil]
    exact DualNumber.isMaximal_span_singleton_eps
  haveI : Ring.KrullDimLE 0 (DualNumber ℚ) :=
    Ring.KrullDimLE.of_isMaximal_nilradical (DualNumber ℚ)
  have hdim : ringKrullDim (DualNumber ℚ) = 0 :=
    ringKrullDimZero_iff_ringKrullDim_eq_zero.mp inferInstance

  have hspan := h.spanFinrank_maximalIdeal
  rw [hdim] at hspan
  have hspan0 : (maximalIdeal (DualNumber ℚ)).spanFinrank = 0 := by exact_mod_cast hspan
  have hbot : maximalIdeal (DualNumber ℚ) = ⊥ :=
    (Submodule.spanFinrank_eq_zero_iff_eq_bot (IsNoetherian.noetherian _)).mp hspan0
  rw [DualNumber.maximalIdeal_eq_span_singleton_eps, Ideal.span_singleton_eq_bot] at hbot
  exact eps_ne_zero hbot

theorem not_forall_isRegularLocalRing_of_quotient_dropping_nonZeroDivisor :
    ¬ (∀ (A : Type) [CommRing A] [IsLocalRing A] [IsNoetherianRing A] (x : A),
        x ∈ maximalIdeal A → IsRegularLocalRing (A ⧸ Ideal.span {x}) →
        IsRegularLocalRing A) := by
  intro hclaim
  haveI : IsNoetherianRing (DualNumber ℚ) := PrincipalIdealRing.isNoetherianRing
  exact not_isRegularLocalRing_dualNumber
    (hclaim (DualNumber ℚ) DualNumber.eps eps_mem_maximalIdeal
      quotient_span_eps_isRegularLocalRing)

end Teeth

end RegularLocalRingQuotientAscent

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

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

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

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

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

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

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

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

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

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

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

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

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

end