GaloisFullRootCoverActualRoot.lean

theorem fullRootCover_actualRoot_prime_of_regular_pair
    {R : Type u} [CommRing R] [IsDomain R] [IsLocalRing R]
    [IsNoetherianRing R]
    {s : ℕ} (n : Fin (s + 1) → ℕ) (a : Fin (s + 1) → R)
    (k : Fin (s + 1)) (hother : ∀ l, l ≠ k → n l = 1)
    (hnk : 0 < n k) {N : ℕ} (hN : 0 < N) {y : R}
    (hreg : IsRegular R [y, a k])
    (hgen : Ideal.ofList [y, a k] = maximalIdeal R) :
    let B := iteratedRadical R (s + 1) n a
    let F : B[X] := X ^ N - C (algebraMap R B y)
    Prime
      (algebraMap B (AdjoinRoot F)
        (iteratedRadicalRoot R n a k)) := by
  dsimp only
  let n₁ : Fin 1 → ℕ := fun _ ↦ N
  let a₁ : Fin 1 → R := fun _ ↦ y
  let Y := iteratedRadical R 1 n₁ a₁
  let py : R[X] := X ^ N - C y
  let Yroot := AdjoinRoot py
  have hgeometryY :=
    oneRootCover_selectedDivisor_geometry hN hreg hgen
  have hother₁ : ∀ l : Fin 1, l ≠ (0 : Fin 1) → n₁ l = 1 := by
    intro l hl
    exact (hl (Subsingleton.elim l 0)).elim
  let eY : Y ≃ₐ[R] Yroot :=
    iteratedRadicalSingleRootAlgEquiv n₁ a₁ 0 hother₁
  have hdomainY : IsDomain Y := by
    simpa only [Y, n₁, a₁] using hgeometryY.2.1
  let : IsDomain Y := hdomainY
  let : IsDomain Yroot := eY.symm.toMulEquiv.isDomain Y
  have haPrimeY : Prime (algebraMap R Yroot (a k)) := by
    rw [← eY.commutes]
    apply (MulEquiv.prime_iff eY).mpr
    simpa only [Y, n₁, a₁] using hgeometryY.2.2.1
  let B := iteratedRadical R (s + 1) n a
  let F : B[X] := X ^ N - C (algebraMap R B y)
  let G : Yroot[X] := X ^ n k - C (algebraMap R Yroot (a k))
  have hrootPrime : Prime (AdjoinRoot.root G) := by
    exact prime_adjoinRoot_root_of_prime hnk haPrimeY
  let eD : AdjoinRoot F ≃ₐ[R] AdjoinRoot G :=
    fullRootCoverActualRootLastAlgEquiv n a k hother N y
  apply (MulEquiv.prime_iff eD).mp
  rw [fullRootCoverActualRootLastAlgEquiv_algebraMap_root]
  exact hrootPrime

theorem heightOnePrime_eq_span_fullRootCover_actualRoot_of_regular_pair
    {R : Type u} [CommRing R] [IsDomain R] [IsLocalRing R]
    [IsNoetherianRing R]
    {s : ℕ} (n : Fin (s + 1) → ℕ) (a : Fin (s + 1) → R)
    (k : Fin (s + 1)) (hother : ∀ l, l ≠ k → n l = 1)
    (hnk : 0 < n k) {N : ℕ} (hN : 0 < N) {y : R}
    (hreg : IsRegular R [y, a k])
    (hgen : Ideal.ofList [y, a k] = maximalIdeal R) :
    let B := iteratedRadical R (s + 1) n a
    let F : B[X] := X ^ N - C (algebraMap R B y)
    let D := AdjoinRoot F
    ∀ (q : Ideal D) [q.IsPrime] [IsDomain D], q.height = 1 →
      q.under B = Ideal.span
        ({iteratedRadicalRoot R n a k} : Set B) →
      q = Ideal.span
        ({algebraMap B D (iteratedRadicalRoot R n a k)} : Set D) := by
  dsimp only
  intro q _ _ hqHeight hunder
  have hrootPrime :=
    fullRootCover_actualRoot_prime_of_regular_pair
      n a k hother hnk hN hreg hgen
  have hrootMem :
      algebraMap (iteratedRadical R (s + 1) n a)
          (AdjoinRoot
            (X ^ N - C
              (algebraMap R (iteratedRadical R (s + 1) n a) y)))
          (iteratedRadicalRoot R n a k) ∈ q := by
    change iteratedRadicalRoot R n a k ∈
      q.under (iteratedRadical R (s + 1) n a)
    rw [hunder]
    exact Ideal.mem_span_singleton_self _
  exact q.eq_span_singleton_of_height_eq_one
    hqHeight hrootMem hrootPrime

theorem fullRootCoverActualRootLastAlgEquiv_map_actualRoot_span
    {R : Type u} [CommRing R]
    {s : ℕ} (n : Fin (s + 1) → ℕ) (a : Fin (s + 1) → R)
    (k : Fin (s + 1)) (hother : ∀ l, l ≠ k → n l = 1)
    (N : ℕ) (y : R) :
    let B := iteratedRadical R (s + 1) n a
    let F : B[X] := X ^ N - C (algebraMap R B y)
    let py : R[X] := X ^ N - C y
    let Yroot := AdjoinRoot py
    let G : Yroot[X] := X ^ n k - C (algebraMap R Yroot (a k))
    (Ideal.span
      ({(algebraMap B (AdjoinRoot F)
        (iteratedRadicalRoot R n a k))} : Set (AdjoinRoot F))).map
        (fullRootCoverActualRootLastAlgEquiv
          n a k hother N y).toRingEquiv =
      Ideal.span ({AdjoinRoot.root G} : Set (AdjoinRoot G)) := by
  dsimp only
  rw [Ideal.map_span]
  simp only [Set.image_singleton]
  let eD := fullRootCoverActualRootLastAlgEquiv n a k hother N y
  change Ideal.span
      ({(eD
        (algebraMap (iteratedRadical R (s + 1) n a)
          (AdjoinRoot
            (X ^ N - C
              (algebraMap R (iteratedRadical R (s + 1) n a) y)))
          (iteratedRadicalRoot R n a k)))} :
        Set (AdjoinRoot
          (X ^ n k - C
            (algebraMap R (AdjoinRoot (X ^ N - C y)) (a k))))) = _
  rw [fullRootCoverActualRootLastAlgEquiv_algebraMap_root]

theorem fullRootCoverActualRootLast_root_prime_of_regular_pair
    {R : Type u} [CommRing R] [IsDomain R] [IsLocalRing R]
    [IsNoetherianRing R]
    {s : ℕ} (n : Fin (s + 1) → ℕ) (a : Fin (s + 1) → R)
    (k : Fin (s + 1)) (hother : ∀ l, l ≠ k → n l = 1)
    (hnk : 0 < n k) {N : ℕ} (hN : 0 < N) {y : R}
    (hreg : IsRegular R [y, a k])
    (hgen : Ideal.ofList [y, a k] = maximalIdeal R) :
    let py : R[X] := X ^ N - C y
    let Yroot := AdjoinRoot py
    let G : Yroot[X] := X ^ n k - C (algebraMap R Yroot (a k))
    Prime (AdjoinRoot.root G) := by
  dsimp only
  let B := iteratedRadical R (s + 1) n a
  let F : B[X] := X ^ N - C (algebraMap R B y)
  let py : R[X] := X ^ N - C y
  let Yroot := AdjoinRoot py
  let G : Yroot[X] := X ^ n k - C (algebraMap R Yroot (a k))
  let eD : AdjoinRoot F ≃ₐ[R] AdjoinRoot G :=
    fullRootCoverActualRootLastAlgEquiv n a k hother N y
  have hprime := fullRootCover_actualRoot_prime_of_regular_pair
    n a k hother hnk hN hreg hgen
  have hmapped : Prime
      (eD (algebraMap B (AdjoinRoot F)
        (iteratedRadicalRoot R n a k))) :=
    (MulEquiv.prime_iff eD).mpr hprime
  rw [fullRootCoverActualRootLastAlgEquiv_algebraMap_root] at hmapped
  exact hmapped

def localizationAtFullRootCoverActualRootAlgEquiv_of_regular_pair
    {R : Type u} [CommRing R] [IsDomain R] [IsLocalRing R]
    [IsNoetherianRing R]
    {s : ℕ} (n : Fin (s + 1) → ℕ) (a : Fin (s + 1) → R)
    (k : Fin (s + 1)) (hother : ∀ l, l ≠ k → n l = 1)
    (hnk : 0 < n k) {N : ℕ} (hN : 0 < N) {y : R}
    (hreg : IsRegular R [y, a k])
    (hgen : Ideal.ofList [y, a k] = maximalIdeal R) :
    let B := iteratedRadical R (s + 1) n a
    let F : B[X] := X ^ N - C (algebraMap R B y)
    let D := AdjoinRoot F
    let py : R[X] := X ^ N - C y
    let Yroot := AdjoinRoot py
    let G : Yroot[X] := X ^ n k - C (algebraMap R Yroot (a k))
    let hrootPrime : Prime (AdjoinRoot.root G) :=
      fullRootCoverActualRootLast_root_prime_of_regular_pair
        n a k hother hnk hN hreg hgen
    letI : (Ideal.span
      ({AdjoinRoot.root G} : Set (AdjoinRoot G))).IsPrime :=
        Ideal.isPrime_span_singleton_of_prime hrootPrime
    ∀ (q : Ideal D) [q.IsPrime] [IsDomain D], q.height = 1 →
      q.under B = Ideal.span
        ({iteratedRadicalRoot R n a k} : Set B) →
      Localization.AtPrime q ≃ₐ[R]
        Localization.AtPrime
          (Ideal.span ({AdjoinRoot.root G} : Set (AdjoinRoot G))) := by
  dsimp only
  intro q _ _ hqHeight hunder
  let B := iteratedRadical R (s + 1) n a
  let F : B[X] := X ^ N - C (algebraMap R B y)
  let D := AdjoinRoot F
  let py : R[X] := X ^ N - C y
  let Yroot := AdjoinRoot py
  let G : Yroot[X] := X ^ n k - C (algebraMap R Yroot (a k))
  have hrootPrime : Prime (AdjoinRoot.root G) :=
    fullRootCoverActualRootLast_root_prime_of_regular_pair
      n a k hother hnk hN hreg hgen
  letI : (Ideal.span
      ({AdjoinRoot.root G} : Set (AdjoinRoot G))).IsPrime :=
    Ideal.isPrime_span_singleton_of_prime hrootPrime
  let eD : D ≃ₐ[R] AdjoinRoot G :=
    fullRootCoverActualRootLastAlgEquiv n a k hother N y
  have hqEq : q = Ideal.span
      ({algebraMap B D (iteratedRadicalRoot R n a k)} : Set D) :=
    heightOnePrime_eq_span_fullRootCover_actualRoot_of_regular_pair
      n a k hother hnk hN hreg hgen q hqHeight hunder
  have hmapEq : q.map eD.toRingEquiv =
      Ideal.span ({AdjoinRoot.root G} : Set (AdjoinRoot G)) := by
    rw [hqEq]
    exact fullRootCoverActualRootLastAlgEquiv_map_actualRoot_span
      n a k hother N y
  have hcompl : Submonoid.map eD q.primeCompl =
      (Ideal.span
        ({AdjoinRoot.root G} : Set (AdjoinRoot G))).primeCompl := by
    rw [EtaleFundamentalGroups.localizationAtMappedPrime_map_primeCompl]
    ext x
    change x ∉ q.map eD.toRingEquiv ↔
      x ∉ Ideal.span ({AdjoinRoot.root G} : Set (AdjoinRoot G))
    rw [hmapEq]
  exact IsLocalization.algEquivOfAlgEquiv
    (Localization.AtPrime q)
    (Localization.AtPrime
      (Ideal.span ({AdjoinRoot.root G} : Set (AdjoinRoot G))))
    eD hcompl

theorem
    splitStrictNormalCrossings_heightTwo_galoisFullRootCover_actualRoot_prime
    {A : Type uA} {K : Type uK} {L : Type uL}
    [CommRing A] [IsDomain A] [IsLocalRing A] [IsRegularRing A]
    [Field K] [Field L]
    [Algebra A K] [IsFractionRing A K]
    [Algebra K L] [Algebra A L] [IsScalarTower A K L]
    [FiniteDimensional K L] [IsGalois K L]
    {s r : ℕ} {f : A} {t : Fin (s + 2) → A}
    (hNC : IsSplitStrictNormalCrossingsAt f t r)
    (i : Fin (s + 2))
    (P : Ideal A) [P.IsPrime] (hP : P.height = 2)
    (htiP : t i ∈ P)
    (σ : Equiv.Perm (Fin (s + 1))) (k : Fin (s + 1))
    (hkActive : (i.succAbove (σ k)).1 < r)
    (htkP : t (i.succAbove (σ k)) ∈ P) :
    let e := heightTwoOtherBranchGaloisRamificationIndex
      (K := K) (L := L) t hNC i
    let N := heightTwoSelectedBranchGaloisRamificationIndex
      (K := K) (L := L) t hNC i
    let R := Localization.AtPrime P
    let n := heightTwoConditionalOtherExponent t i r P e σ
    let a : Fin (s + 1) → R :=
      heightTwoConditionalOtherRadicand t i P σ
    let B := iteratedRadical R (s + 1) n a
    let y : R := algebraMap A R (t i)
    let F : B[X] := X ^ N - C (algebraMap R B y)
    Prime
      (algebraMap B (AdjoinRoot F)
        (iteratedRadicalRoot R n a k)) := by
  dsimp only
  classical
  let e := heightTwoOtherBranchGaloisRamificationIndex
    (K := K) (L := L) t hNC i
  let N := heightTwoSelectedBranchGaloisRamificationIndex
    (K := K) (L := L) t hNC i
  let R := Localization.AtPrime P
  let n := heightTwoConditionalOtherExponent t i r P e σ
  let a : Fin (s + 1) → R :=
    heightTwoConditionalOtherRadicand t i P σ
  let y : R := algebraMap A R (t i)
  let j : Fin (s + 2) := i.succAbove (σ k)
  have hother : ∀ l, l ≠ k → n l = 1 :=
    heightTwoConditionalOtherExponent_eq_one_of_ne_actual
      hNC i P hP htiP e σ k hkActive htkP
  have hnk : 0 < n k := by
    change 0 < if (i.succAbove (σ k)).1 < r ∧
      t (i.succAbove (σ k)) ∈ P then e (σ k) else 1
    rw [ite_eq_left ⟨hkActive, htkP⟩]
    exact heightTwoOtherBranchGaloisRamificationIndex_pos
      (K := K) (L := L) t hNC i (σ k)
  have hN : 0 < N :=
    heightTwoSelectedBranchGaloisRamificationIndex_pos
      (K := K) (L := L) t hNC i
  have hij : i ≠ j := (Fin.succAbove_ne i (σ k)).symm
  have hpair :=
    regular_pair_localizationAtPrime_of_two_splitStrictNormalCrossingsParameters
      hNC i j hij P hP htiP htkP
  have hreg : IsRegular R [y, a k] := by
    simpa only [R, y, a, heightTwoConditionalOtherRadicand, j] using
      hpair.1
  have hgen : Ideal.ofList [y, a k] = maximalIdeal R := by
    simpa only [R, y, a, heightTwoConditionalOtherRadicand, j] using
      hpair.2
  exact fullRootCover_actualRoot_prime_of_regular_pair
    n a k hother hnk hN hreg hgen

theorem
    splitStrictNormalCrossings_heightTwo_galoisFullRootCover_heightOnePrime_eq_span_actualRoot
    {A : Type uA} {K : Type uK} {L : Type uL}
    [CommRing A] [IsDomain A] [IsLocalRing A] [IsRegularRing A]
    [Field K] [Field L]
    [Algebra A K] [IsFractionRing A K]
    [Algebra K L] [Algebra A L] [IsScalarTower A K L]
    [FiniteDimensional K L] [IsGalois K L]
    {s r : ℕ} {f : A} {t : Fin (s + 2) → A}
    (hNC : IsSplitStrictNormalCrossingsAt f t r)
    (i : Fin (s + 2))
    (P : Ideal A) [P.IsPrime] (hP : P.height = 2)
    (htiP : t i ∈ P)
    (σ : Equiv.Perm (Fin (s + 1))) (k : Fin (s + 1))
    (hkActive : (i.succAbove (σ k)).1 < r)
    (htkP : t (i.succAbove (σ k)) ∈ P) :
    let e := heightTwoOtherBranchGaloisRamificationIndex
      (K := K) (L := L) t hNC i
    let N := heightTwoSelectedBranchGaloisRamificationIndex
      (K := K) (L := L) t hNC i
    let R := Localization.AtPrime P
    let n := heightTwoConditionalOtherExponent t i r P e σ
    let a : Fin (s + 1) → R :=
      heightTwoConditionalOtherRadicand t i P σ
    let B := iteratedRadical R (s + 1) n a
    let y : R := algebraMap A R (t i)
    let F : B[X] := X ^ N - C (algebraMap R B y)
    let D := AdjoinRoot F
    ∀ (q : Ideal D) [q.IsPrime] [IsDomain D], q.height = 1 →
      q.under B = Ideal.span
        ({iteratedRadicalRoot R n a k} : Set B) →
      q = Ideal.span
        ({algebraMap B D (iteratedRadicalRoot R n a k)} : Set D) := by
  dsimp only
  intro q _ _ hqHeight hunder
  have hrootPrime :=
    splitStrictNormalCrossings_heightTwo_galoisFullRootCover_actualRoot_prime
      (K := K) (L := L) hNC i P hP htiP σ k hkActive htkP
  have hrootMem :
      algebraMap
          (iteratedRadical (Localization.AtPrime P) (s + 1)
            (heightTwoConditionalOtherExponent t i r P
              (heightTwoOtherBranchGaloisRamificationIndex
                (K := K) (L := L) t hNC i) σ)
            (heightTwoConditionalOtherRadicand t i P σ))
          (AdjoinRoot
            (X ^ (heightTwoSelectedBranchGaloisRamificationIndex
                    (K := K) (L := L) t hNC i) -
              C (algebraMap (Localization.AtPrime P)
                (iteratedRadical (Localization.AtPrime P) (s + 1)
                  (heightTwoConditionalOtherExponent t i r P
                    (heightTwoOtherBranchGaloisRamificationIndex
                      (K := K) (L := L) t hNC i) σ)
                  (heightTwoConditionalOtherRadicand t i P σ))
                (algebraMap A (Localization.AtPrime P) (t i)))))
          (iteratedRadicalRoot (Localization.AtPrime P)
            (heightTwoConditionalOtherExponent t i r P
              (heightTwoOtherBranchGaloisRamificationIndex
                (K := K) (L := L) t hNC i) σ)
            (heightTwoConditionalOtherRadicand t i P σ) k) ∈ q := by
    change iteratedRadicalRoot (Localization.AtPrime P)
        (heightTwoConditionalOtherExponent t i r P
          (heightTwoOtherBranchGaloisRamificationIndex
            (K := K) (L := L) t hNC i) σ)
        (heightTwoConditionalOtherRadicand t i P σ) k ∈
      q.under
        (iteratedRadical (Localization.AtPrime P) (s + 1)
          (heightTwoConditionalOtherExponent t i r P
            (heightTwoOtherBranchGaloisRamificationIndex
              (K := K) (L := L) t hNC i) σ)
          (heightTwoConditionalOtherRadicand t i P σ))
    rw [hunder]
    exact Ideal.mem_span_singleton_self _
  exact q.eq_span_singleton_of_height_eq_one
    hqHeight hrootMem hrootPrime

theorem
    splitStrictNormalCrossings_heightTwo_galoisFullRootCover_actualRootLast_map_heightOnePrime
    {A : Type uA} {K : Type uK} {L : Type uL}
    [CommRing A] [IsDomain A] [IsLocalRing A] [IsRegularRing A]
    [Field K] [Field L]
    [Algebra A K] [IsFractionRing A K]
    [Algebra K L] [Algebra A L] [IsScalarTower A K L]
    [FiniteDimensional K L] [IsGalois K L]
    {s r : ℕ} {f : A} {t : Fin (s + 2) → A}
    (hNC : IsSplitStrictNormalCrossingsAt f t r)
    (i : Fin (s + 2))
    (P : Ideal A) [P.IsPrime] (hP : P.height = 2)
    (htiP : t i ∈ P)
    (σ : Equiv.Perm (Fin (s + 1))) (k : Fin (s + 1))
    (hkActive : (i.succAbove (σ k)).1 < r)
    (htkP : t (i.succAbove (σ k)) ∈ P) :
    let e := heightTwoOtherBranchGaloisRamificationIndex
      (K := K) (L := L) t hNC i
    let N := heightTwoSelectedBranchGaloisRamificationIndex
      (K := K) (L := L) t hNC i
    let R := Localization.AtPrime P
    let n := heightTwoConditionalOtherExponent t i r P e σ
    let a : Fin (s + 1) → R :=
      heightTwoConditionalOtherRadicand t i P σ
    let B := iteratedRadical R (s + 1) n a
    let y : R := algebraMap A R (t i)
    let F : B[X] := X ^ N - C (algebraMap R B y)
    let D := AdjoinRoot F
    let py : R[X] := X ^ N - C y
    let Yroot := AdjoinRoot py
    let G : Yroot[X] := X ^ n k - C (algebraMap R Yroot (a k))
    let hother : ∀ l, l ≠ k → n l = 1 :=
      heightTwoConditionalOtherExponent_eq_one_of_ne_actual
        hNC i P hP htiP e σ k hkActive htkP
    ∀ (q : Ideal D) [q.IsPrime] [IsDomain D], q.height = 1 →
      q.under B = Ideal.span
        ({iteratedRadicalRoot R n a k} : Set B) →
      q.map
          (fullRootCoverActualRootLastAlgEquiv
            n a k hother N y).toRingEquiv =
        Ideal.span ({AdjoinRoot.root G} : Set (AdjoinRoot G)) := by
  intro e N R n a B y F D py Yroot G hother q _ _ hqHeight hunder
  classical
  have hqEq : q = Ideal.span
      ({algebraMap B D (iteratedRadicalRoot R n a k)} : Set D) :=
    splitStrictNormalCrossings_heightTwo_galoisFullRootCover_heightOnePrime_eq_span_actualRoot
      (K := K) (L := L) hNC i P hP htiP σ k hkActive htkP
        q hqHeight hunder
  rw [hqEq]
  exact fullRootCoverActualRootLastAlgEquiv_map_actualRoot_span
    n a k hother N y