ConditionalRootCover.lean

def iteratedRadicalTailOneAlgEquiv
    {R : Type u} [CommRing R] :
    {r : ℕ} → (n : Fin (r + 1) → ℕ) → (a : Fin (r + 1) → R) →
      (∀ i : Fin r, n i.succ = 1) →
      iteratedRadical R (r + 1) n a ≃ₐ[R]
        iteratedRadical R 1 (fun _ ↦ n 0) (fun _ ↦ a 0)
  | 0, n, a, _ => by
      exact AlgEquiv.refl
  | r + 1, n, a, htail => by
      let nInit : Fin (r + 1) → ℕ := Fin.init n
      let aInit : Fin (r + 1) → R := Fin.init a
      let T : CommAlgCat R := iteratedRadical R (r + 1) nInit aInit
      have hlast : n (Fin.last (r + 1)) = 1 := by
        simpa using htail (Fin.last r)
      have htailInit : ∀ i : Fin r, nInit i.succ = 1 := by
        intro i
        change n i.succ.castSucc = 1
        convert htail i.castSucc using 1
        apply congrArg n
        ext
        rfl
      let c : T := algebraMap R T (a (Fin.last (r + 1)))
      let f : T[X] := X ^ n (Fin.last (r + 1)) - C c
      have hf : f = X ^ 1 - C c := by simp [f, hlast]
      let eT : AdjoinRoot f ≃ₐ[T] T :=
        (AdjoinRoot.algEquivOfEq T f (X ^ 1 - C c) hf).trans
          (adjoinRootOneAlgEquiv c)
      let eR : AdjoinRoot f ≃ₐ[R] T := eT.restrictScalars R
      let eLast : iteratedRadical R (r + 2) n a ≃ₐ[R] T := eR
      exact eLast.trans
        (iteratedRadicalTailOneAlgEquiv nInit aInit htailInit)

def iteratedRadicalAllOneAlgEquiv
    {R : Type u} [CommRing R] :
    {r : ℕ} → (n : Fin r → ℕ) → (a : Fin r → R) →
      (∀ i, n i = 1) → iteratedRadical R r n a ≃ₐ[R] R
  | 0, _, _, _ => AlgEquiv.refl
  | r + 1, n, a, hall => by
      let eTail : iteratedRadical R (r + 1) n a ≃ₐ[R]
          iteratedRadical R 1 (fun _ ↦ n 0) (fun _ ↦ a 0) :=
        iteratedRadicalTailOneAlgEquiv n a (fun i ↦ hall i.succ)
      let eHead :
          iteratedRadical R 1 (fun _ ↦ n 0) (fun _ ↦ a 0) ≃ₐ[R] R := by
        let c : R := algebraMap R R (a 0)
        let f : R[X] := X ^ n 0 - C c
        have hf : f = X ^ 1 - C (a 0) := by
          simp [f, c, hall 0]
        change AdjoinRoot f ≃ₐ[R] R
        exact (AdjoinRoot.algEquivOfEq R f (X ^ 1 - C (a 0)) hf).trans
          (adjoinRootOneAlgEquiv (a 0))
      exact eTail.trans eHead

theorem selectedDivisorGeometry_of_algEquiv
    {R B C : Type u} [CommRing R] [CommRing B] [CommRing C]
    [Algebra R B] [Algebra R C]
    (e : B ≃ₐ[R] C) {y : R}
    (hC : IsRegularLocalRing C ∧ IsDomain C ∧
      Prime (algebraMap R C y) ∧
      IsDomain (C ⧸ Ideal.span ({algebraMap R C y} : Set C)) ∧
      IsRegularLocalRing
        (C ⧸ Ideal.span ({algebraMap R C y} : Set C))) :
    IsRegularLocalRing B ∧ IsDomain B ∧
      Prime (algebraMap R B y) ∧
      IsDomain (B ⧸ Ideal.span ({algebraMap R B y} : Set B)) ∧
      IsRegularLocalRing
        (B ⧸ Ideal.span ({algebraMap R B y} : Set B))

theorem allOneRootCover_selectedDivisor_geometry
    {R : Type u} [CommRing R] [IsDomain R] [IsLocalRing R]
    [IsNoetherianRing R]
    {r : ℕ} (n : Fin r → ℕ) (a : Fin r → R)
    (hall : ∀ i, n i = 1) {y z : R}
    (hreg : IsRegular R [y, z])
    (hgen : Ideal.ofList [y, z] = maximalIdeal R) :
    let B := iteratedRadical R r n a
    IsRegularLocalRing B ∧ IsDomain B ∧
      Prime (algebraMap R B y) ∧
      IsDomain (B ⧸ Ideal.span ({algebraMap R B y} : Set B)) ∧
      IsRegularLocalRing
        (B ⧸ Ideal.span ({algebraMap R B y} : Set B)) := by
  dsimp only
  let e : iteratedRadical R r n a ≃ₐ[R] R :=
    iteratedRadicalAllOneAlgEquiv n a hall
  apply selectedDivisorGeometry_of_algEquiv e
  have hregR : IsRegularLocalRing R :=
    isRegularLocalRing_of_regularSystem [y, z] hreg hgen
  have hyPrime : Prime y :=
    prime_of_mem_regularSystem hreg hgen (by simp)
  have hyQuotient :=
    quotient_geometry_of_mem_regularSystem hreg hgen (p := y) (by simp)
  simpa using
    (show IsRegularLocalRing R ∧ IsDomain R ∧ Prime y ∧
        IsDomain (R ⧸ Ideal.span ({y} : Set R)) ∧
        IsRegularLocalRing (R ⧸ Ideal.span ({y} : Set R)) from
      ⟨hregR, inferInstance, hyPrime, hyQuotient.1, hyQuotient.2⟩)

theorem oneRootWithTrivialTail_selectedDivisor_geometry
    {R : Type u} [CommRing R] [IsDomain R] [IsLocalRing R]
    [IsNoetherianRing R]
    {r : ℕ} (n : Fin (r + 1) → ℕ) (a : Fin (r + 1) → R)
    (htail : ∀ i : Fin r, n i.succ = 1)
    (hn : 0 < n 0) {y : R}
    (hreg : IsRegular R [a 0, y])
    (hgen : Ideal.ofList [a 0, y] = maximalIdeal R) :
    let B := iteratedRadical R (r + 1) n a
    IsRegularLocalRing B ∧ IsDomain B ∧
      Prime (algebraMap R B y) ∧
      IsDomain (B ⧸ Ideal.span ({algebraMap R B y} : Set B)) ∧
      IsRegularLocalRing
        (B ⧸ Ideal.span ({algebraMap R B y} : Set B)) := by
  dsimp only
  let C := iteratedRadical R 1 (fun _ ↦ n 0) (fun _ ↦ a 0)
  let e : iteratedRadical R (r + 1) n a ≃ₐ[R] C :=
    iteratedRadicalTailOneAlgEquiv n a htail
  apply selectedDivisorGeometry_of_algEquiv e
  exact oneRootCover_selectedDivisor_geometry hn hreg hgen