IteratedRegularSystem.lean

theorem ideal_ofList_eq_of_perm
    {R : Type u} [CommRing R] {xs ys : List R} (h : xs.Perm ys) :
    Ideal.ofList xs = Ideal.ofList ys

theorem constructionList_cons
    {A : Type u} [CommRing A] {r : ℕ} (n : Fin r → ℕ) (a : Fin r → A)
    (x : A) (rs : List A) :
    iteratedLocalRootCoverConstructionList A n a (x :: rs) =
      algebraMap A (iteratedRadical A r n a) x ::
        iteratedLocalRootCoverConstructionList A n a rs

theorem iteratedConstructionList_regularSystem
    {A : Type u} [CommRing A] [IsLocalRing A] [IsNoetherianRing A]
    {r : ℕ} (n : Fin r → ℕ) (a : Fin r → A) (rs : List A)
    (hn : ∀ i, 0 < n i)
    (hreg : IsRegular A (List.ofFn a ++ rs))
    (hgen : Ideal.ofList (List.ofFn a ++ rs) = maximalIdeal A)
    [IsLocalRing (iteratedRadical A r n a)]
    [IsNoetherianRing (iteratedRadical A r n a)] :
    IsRegular (iteratedRadical A r n a)
        (iteratedLocalRootCoverConstructionList A n a rs) ∧
      Ideal.ofList (iteratedLocalRootCoverConstructionList A n a rs) =
        maximalIdeal (iteratedRadical A r n a)

theorem iteratedLocalRootCoverParameterList_regularSystem
    {A : Type u} [CommRing A] [IsLocalRing A] [IsNoetherianRing A]
    {r : ℕ} (n : Fin r → ℕ) (a : Fin r → A) (rs : List A)
    (hn : ∀ i, 0 < n i)
    (hreg : IsRegular A (List.ofFn a ++ rs))
    (hgen : Ideal.ofList (List.ofFn a ++ rs) = maximalIdeal A) :
    let B := iteratedRadical A r n a
    let bs := iteratedLocalRootCoverParameterList A n a rs
    letI : IsLocalRing B := isLocalRing_iteratedRadical n a hn (fun i => by
      rw [← hgen]
      exact Ideal.subset_span (by simp))
    IsRegular B bs ∧ Ideal.ofList bs = maximalIdeal B := by
  dsimp only
  let B := iteratedRadical A r n a
  have ha : ∀ i, a i ∈ maximalIdeal A := by
    intro i
    rw [← hgen]
    exact Ideal.subset_span (by simp)
  let : IsLocalRing B := isLocalRing_iteratedRadical n a hn ha
  let : Module.Finite A B := finite_iteratedRadical n a hn
  let : IsNoetherianRing B := IsNoetherianRing.of_finite A B
  have hconstruction :=
    iteratedConstructionList_regularSystem n a rs hn hreg hgen
  have hperm :
      (iteratedLocalRootCoverConstructionList A n a rs).Perm
        (iteratedLocalRootCoverParameterList A n a rs) := by
    exact (List.reverse_perm
      (iteratedLocalRootCoverConstructionList A n a rs)).symm
  exact ⟨IsLocalRing.isRegular_of_perm hconstruction.1 hperm,
    (ideal_ofList_eq_of_perm hperm).symm.trans hconstruction.2⟩

theorem iteratedRadicalRoot_mem_parameterList
    {A : Type u} [CommRing A] {r : ℕ}
    (n : Fin r → ℕ) (a : Fin r → A) (rs : List A) (i : Fin r) :
    iteratedRadicalRoot A n a i ∈
      iteratedLocalRootCoverParameterList A n a rs

theorem algebraMap_mem_iteratedLocalRootCoverParameterList
    {A : Type u} [CommRing A] {r : ℕ}
    (n : Fin r → ℕ) (a : Fin r → A) (rs : List A)
    {x : A} (hx : x ∈ rs) :
    algebraMap A (iteratedRadical A r n a) x ∈
      iteratedLocalRootCoverParameterList A n a rs

theorem iteratedRadical_regularSystem_geometry
    {A : Type u} [CommRing A] [IsLocalRing A] [IsNoetherianRing A]
    {r : ℕ} (n : Fin r → ℕ) (a : Fin r → A) (rs : List A)
    (hn : ∀ i, 0 < n i)
    (hreg : IsRegular A (List.ofFn a ++ rs))
    (hgen : Ideal.ofList (List.ofFn a ++ rs) = maximalIdeal A) :
    let B := iteratedRadical A r n a
    let bs := iteratedLocalRootCoverParameterList A n a rs
    letI : IsLocalRing B := isLocalRing_iteratedRadical n a hn (fun i => by
      rw [← hgen]
      exact Ideal.subset_span (by simp))
    IsNoetherianRing B ∧ IsDomain B ∧ IsRegularLocalRing B ∧
      IsRegular B bs ∧ Ideal.ofList bs = maximalIdeal B ∧
      (∀ p ∈ bs, Prime p) ∧
      (∀ p ∈ bs,
        IsDomain (B ⧸ Ideal.span {p}) ∧
          IsRegularLocalRing (B ⧸ Ideal.span {p})) := by
  dsimp only
  let B := iteratedRadical A r n a
  have ha : ∀ i, a i ∈ maximalIdeal A := by
    intro i
    rw [← hgen]
    exact Ideal.subset_span (by simp)
  let : IsLocalRing B := isLocalRing_iteratedRadical n a hn ha
  let : Module.Finite A B := finite_iteratedRadical n a hn
  let : IsNoetherianRing B := IsNoetherianRing.of_finite A B
  have hsystem := iteratedLocalRootCoverParameterList_regularSystem
    n a rs hn hreg hgen
  have hdomain : IsDomain B :=
    isDomain_of_regularSystem _ hsystem.1 hsystem.2
  let : IsDomain B := hdomain
  have hregularLocal : IsRegularLocalRing B :=
    isRegularLocalRing_of_regularSystem _ hsystem.1 hsystem.2
  refine ⟨inferInstance, hdomain, hregularLocal, hsystem.1, hsystem.2,
    ?_, ?_⟩
  · intro p hp
    exact prime_of_mem_regularSystem hsystem.1 hsystem.2 hp
  · intro p hp
    exact quotient_geometry_of_mem_regularSystem hsystem.1 hsystem.2 hp

theorem isDomain_iteratedRadical_of_regular_parameters
    {A : Type u} [CommRing A] [IsLocalRing A] [IsNoetherianRing A]
    {r : ℕ} (n : Fin r → ℕ) (a : Fin r → A) (rs : List A)
    (hn : ∀ i, 0 < n i)
    (hreg : IsRegular A (List.ofFn a ++ rs))
    (hgen : Ideal.ofList (List.ofFn a ++ rs) = maximalIdeal A) :
    IsDomain (iteratedRadical A r n a)

theorem iteratedRadicalRoot_geometry_of_regular_parameters
    {A : Type u} [CommRing A] [IsLocalRing A] [IsNoetherianRing A]
    {r : ℕ} (n : Fin r → ℕ) (a : Fin r → A) (rs : List A)
    (hn : ∀ i, 0 < n i)
    (hreg : IsRegular A (List.ofFn a ++ rs))
    (hgen : Ideal.ofList (List.ofFn a ++ rs) = maximalIdeal A) :
    let B := iteratedRadical A r n a
    letI : IsLocalRing B := isLocalRing_iteratedRadical n a hn (fun i => by
      rw [← hgen]
      exact Ideal.subset_span (by simp))
    ∀ i,
      Prime (iteratedRadicalRoot A n a i) ∧
        IsDomain (B ⧸ Ideal.span {iteratedRadicalRoot A n a i}) ∧
        IsRegularLocalRing
          (B ⧸ Ideal.span {iteratedRadicalRoot A n a i}) := by
  dsimp only
  let B := iteratedRadical A r n a
  have ha : ∀ i, a i ∈ maximalIdeal A := by
    intro i
    rw [← hgen]
    exact Ideal.subset_span (by simp)
  let : IsLocalRing B := isLocalRing_iteratedRadical n a hn ha
  obtain ⟨_, _, _, _, _, hprime, hquot⟩ :=
    iteratedRadical_regularSystem_geometry n a rs hn hreg hgen
  intro i
  have hi := iteratedRadicalRoot_mem_parameterList n a rs i
  exact ⟨hprime _ hi, (hquot _ hi).1, (hquot _ hi).2⟩

theorem iteratedRadicalMappedRadicand_geometry_of_exponent_one
    {A : Type u} [CommRing A] [IsLocalRing A] [IsNoetherianRing A]
    {r : ℕ} (n : Fin r → ℕ) (a : Fin r → A) (rs : List A)
    (hn : ∀ i, 0 < n i)
    (hreg : IsRegular A (List.ofFn a ++ rs))
    (hgen : Ideal.ofList (List.ofFn a ++ rs) = maximalIdeal A)
    (i : Fin r) (hi : n i = 1) :
    let B := iteratedRadical A r n a
    letI : IsLocalRing B := isLocalRing_iteratedRadical n a hn (fun j => by
      rw [← hgen]
      exact Ideal.subset_span (by simp))
    Prime (algebraMap A B (a i)) ∧
      IsDomain (B ⧸ Ideal.span {algebraMap A B (a i)}) ∧
      IsRegularLocalRing (B ⧸ Ideal.span {algebraMap A B (a i)}) := by
  dsimp only
  let B := iteratedRadical A r n a
  have ha : ∀ j, a j ∈ maximalIdeal A := by
    intro j
    rw [← hgen]
    exact Ideal.subset_span (by simp)
  let : IsLocalRing B := isLocalRing_iteratedRadical n a hn ha
  have hroot :=
    iteratedRadicalRoot_geometry_of_regular_parameters n a rs hn hreg hgen i
  have heq : iteratedRadicalRoot A n a i = algebraMap A B (a i) := by
    have hpow := iteratedRadicalRoot_pow n a i
    rw [hi] at hpow
    simpa using hpow
  rw [← heq]
  exact hroot

theorem iteratedRadicalRemainingParameter_geometry
    {A : Type u} [CommRing A] [IsLocalRing A] [IsNoetherianRing A]
    {r : ℕ} (n : Fin r → ℕ) (a : Fin r → A) (rs : List A)
    (hn : ∀ i, 0 < n i)
    (hreg : IsRegular A (List.ofFn a ++ rs))
    (hgen : Ideal.ofList (List.ofFn a ++ rs) = maximalIdeal A) :
    let B := iteratedRadical A r n a
    letI : IsLocalRing B := isLocalRing_iteratedRadical n a hn (fun i => by
      rw [← hgen]
      exact Ideal.subset_span (by simp))
    ∀ x ∈ rs,
      Prime (algebraMap A B x) ∧
        IsDomain (B ⧸ Ideal.span {algebraMap A B x}) ∧
        IsRegularLocalRing (B ⧸ Ideal.span {algebraMap A B x}) := by
  dsimp only
  let B := iteratedRadical A r n a
  have ha : ∀ i, a i ∈ maximalIdeal A := by
    intro i
    rw [← hgen]
    exact Ideal.subset_span (by simp)
  let : IsLocalRing B := isLocalRing_iteratedRadical n a hn ha
  obtain ⟨_, _, _, _, _, hprime, hquot⟩ :=
    iteratedRadical_regularSystem_geometry n a rs hn hreg hgen
  intro x hx
  have hx' := algebraMap_mem_iteratedLocalRootCoverParameterList n a rs hx
  exact ⟨hprime _ hx', (hquot _ hx').1, (hquot _ hx').2⟩