LocalizationAtRootPrime.lean

theorem span_root_liesOver_span_radicand
    {R : Type u} [CommRing R] [IsDomain R]
    {N : ℕ} (hN : 0 < N) {p : R} (hp : Prime p) :
    let P := Ideal.span ({p} : Set R)
    let D := AdjoinRoot (X ^ N - C p)
    let q := Ideal.span
      ({AdjoinRoot.root (X ^ N - C p)} : Set D)
    letI : P.IsPrime := Ideal.isPrime_span_singleton_of_prime hp
    letI : q.IsPrime := Ideal.isPrime_span_singleton_of_prime
      (prime_adjoinRoot_root_of_prime hN hp)
    q.LiesOver P := by
  dsimp only
  let P := Ideal.span ({p} : Set R)
  let D := AdjoinRoot (X ^ N - C p)
  let q := Ideal.span
    ({AdjoinRoot.root (X ^ N - C p)} : Set D)
  let : P.IsPrime := Ideal.isPrime_span_singleton_of_prime hp
  let : q.IsPrime := Ideal.isPrime_span_singleton_of_prime
    (prime_adjoinRoot_root_of_prime hN hp)
  apply Ideal.LiesOver.mk
  symm
  ext x
  change algebraMap R D x ∈ q ↔ x ∈ P
  have hqker : q = RingHom.ker (adjoinRootToQuotient hN p) :=
    (ker_adjoinRootToQuotient hN p).symm
  rw [hqker]
  change adjoinRootToQuotient hN p (algebraMap R D x) = 0 ↔ x ∈ P
  simp [adjoinRootToQuotient, P, D,
    Ideal.Quotient.eq_zero_iff_mem]

def adjoinRootLocalizationBaseChangeAlgEquiv
    (R : Type u) [CommRing R] (N : ℕ) (p : R) (hp : Prime p) :
    let P := Ideal.span ({p} : Set R)
    letI : P.IsPrime := Ideal.isPrime_span_singleton_of_prime hp
    let V := Localization.AtPrime P
    let D := AdjoinRoot (X ^ N - C p)
    let Rn := AdjoinRoot (X ^ N - C (algebraMap R V p))
    (V ⊗[R] D) ≃ₐ[V] Rn := by
  dsimp only
  let P := Ideal.span ({p} : Set R)
  letI : P.IsPrime := Ideal.isPrime_span_singleton_of_prime hp
  let V := Localization.AtPrime P
  let fR : R[X] := X ^ N - C p
  let fV : V[X] := X ^ N - C (algebraMap R V p)
  exact (adjoinRootBaseChangeAlgEquiv fR).trans
    (AdjoinRoot.algEquivOfEq V _ _ (by simp [fR]))

def adjoinRootLocalizationBaseChangeAlgebra
    (R : Type u) [CommRing R] (N : ℕ) (p : R) (hp : Prime p) :
    let P := Ideal.span ({p} : Set R)
    letI : P.IsPrime := Ideal.isPrime_span_singleton_of_prime hp
    let V := Localization.AtPrime P
    let D := AdjoinRoot (X ^ N - C p)
    let Rn := AdjoinRoot (X ^ N - C (algebraMap R V p))
    Algebra D Rn := by
  dsimp only
  let P := Ideal.span ({p} : Set R)
  letI : P.IsPrime := Ideal.isPrime_span_singleton_of_prime hp
  let V := Localization.AtPrime P
  let D := AdjoinRoot (X ^ N - C p)
  let Rn := AdjoinRoot (X ^ N - C (algebraMap R V p))
  exact
    ((adjoinRootLocalizationBaseChangeAlgEquiv R N p hp).toRingHom.comp
      (Algebra.TensorProduct.includeRight :
        D →ₐ[R] V ⊗[R] D).toRingHom).toAlgebra

theorem adjoinRootLocalizationBaseChangeAlgebra_root
    {R : Type u} [CommRing R] (N : ℕ) (p : R) (hp : Prime p) :
    let P := Ideal.span ({p} : Set R)
    letI : P.IsPrime := Ideal.isPrime_span_singleton_of_prime hp
    let V := Localization.AtPrime P
    let D := AdjoinRoot (X ^ N - C p)
    let Rn := AdjoinRoot (X ^ N - C (algebraMap R V p))
    letI : Algebra D Rn :=
      adjoinRootLocalizationBaseChangeAlgebra R N p hp
    algebraMap D Rn (AdjoinRoot.root (X ^ N - C p)) =
      AdjoinRoot.root (X ^ N - C (algebraMap R V p)) := by
  dsimp only
  let P := Ideal.span ({p} : Set R)
  let : P.IsPrime := Ideal.isPrime_span_singleton_of_prime hp
  let V := Localization.AtPrime P
  let fR : R[X] := X ^ N - C p
  let fV : V[X] := X ^ N - C (algebraMap R V p)
  let D := AdjoinRoot fR
  let Rn := AdjoinRoot fV
  let : Algebra D Rn :=
    adjoinRootLocalizationBaseChangeAlgebra R N p hp
  have hmap : fR.map (algebraMap R V) = fV := by simp [fR, fV]
  change ((adjoinRootBaseChangeAlgEquiv fR).trans
      (AdjoinRoot.algEquivOfEq V _ _ hmap))
    (1 ⊗ₜ[R] AdjoinRoot.root fR) = AdjoinRoot.root fV
  rw [AlgEquiv.trans_apply, adjoinRootBaseChangeAlgEquiv_tmul_root,
    AdjoinRoot.algEquivOfEq_root]

theorem adjoinRootLocalizationBaseChangeAlgebra_base
    {R : Type u} [CommRing R] (N : ℕ) (p r : R) (hp : Prime p) :
    let P := Ideal.span ({p} : Set R)
    letI : P.IsPrime := Ideal.isPrime_span_singleton_of_prime hp
    let V := Localization.AtPrime P
    let D := AdjoinRoot (X ^ N - C p)
    let Rn := AdjoinRoot (X ^ N - C (algebraMap R V p))
    letI : Algebra D Rn :=
      adjoinRootLocalizationBaseChangeAlgebra R N p hp
    algebraMap D Rn (algebraMap R D r) =
      algebraMap V Rn (algebraMap R V r) := by
  dsimp only
  let P := Ideal.span ({p} : Set R)
  let : P.IsPrime := Ideal.isPrime_span_singleton_of_prime hp
  let V := Localization.AtPrime P
  let D := AdjoinRoot (X ^ N - C p)
  let Rn := AdjoinRoot (X ^ N - C (algebraMap R V p))
  let eV := adjoinRootLocalizationBaseChangeAlgEquiv R N p hp
  change eV (1 ⊗ₜ[R] algebraMap R D r) =
    algebraMap V Rn (algebraMap R V r)
  calc
    eV (1 ⊗ₜ[R] algebraMap R D r) =
        eV (algebraMap V (V ⊗[R] D) (algebraMap R V r)) := by
      congr 1
      exact (Algebra.TensorProduct.tmul_one_eq_one_tmul r).symm
    _ = _ := eV.commutes _

theorem isLocalization_adjoinRootLocalizationAtRootPrime
    {R : Type u} [CommRing R] [IsDomain R]
    {N : ℕ} (hN : 0 < N) {p : R} (hp : Prime p) :
    let P := Ideal.span ({p} : Set R)
    let D := AdjoinRoot (X ^ N - C p)
    let q := Ideal.span
      ({AdjoinRoot.root (X ^ N - C p)} : Set D)
    letI : P.IsPrime := Ideal.isPrime_span_singleton_of_prime hp
    letI : q.IsPrime := Ideal.isPrime_span_singleton_of_prime
      (prime_adjoinRoot_root_of_prime hN hp)
    let V := Localization.AtPrime P
    let Rn := AdjoinRoot (X ^ N - C (algebraMap R V p))
    letI : Algebra D Rn :=
      adjoinRootLocalizationBaseChangeAlgebra R N p hp
    letI : q.LiesOver P := span_root_liesOver_span_radicand hN hp
    IsLocalization q.primeCompl Rn := by
  dsimp only
  let P := Ideal.span ({p} : Set R)
  let fR : R[X] := X ^ N - C p
  let D := AdjoinRoot fR
  let q := Ideal.span ({AdjoinRoot.root fR} : Set D)
  let : P.IsPrime := Ideal.isPrime_span_singleton_of_prime hp
  let : q.IsPrime := Ideal.isPrime_span_singleton_of_prime
    (prime_adjoinRoot_root_of_prime hN hp)
  let : q.LiesOver P := span_root_liesOver_span_radicand hN hp
  let V := Localization.AtPrime P
  let pV : V := algebraMap R V p
  let fV : V[X] := X ^ N - C pV
  let Rn := AdjoinRoot fV
  let eV : (V ⊗[R] D) ≃ₐ[V] Rn :=
    adjoinRootLocalizationBaseChangeAlgEquiv R N p hp
  let : Algebra D (V ⊗[R] D) := Algebra.TensorProduct.rightAlgebra
  let : Algebra D Rn :=
    adjoinRootLocalizationBaseChangeAlgebra R N p hp
  let eD : (V ⊗[R] D) ≃ₐ[D] Rn :=
    { eV.toRingEquiv with commutes' := fun _ ↦ rfl }
  let M := Algebra.algebraMapSubmonoid D P.primeCompl
  have hTensor : IsLocalization M (V ⊗[R] D) := by
    infer_instance
  have hRnM : IsLocalization M Rn :=
    IsLocalization.isLocalization_of_algEquiv M eD
  have hpMem : pV ∈ IsLocalRing.maximalIdeal V := by
    change algebraMap R V p ∈ IsLocalRing.maximalIdeal V
    rw [← IsLocalization.AtPrime.map_eq_maximalIdeal P]
    exact Ideal.mem_map_of_mem (algebraMap R V)
      (Ideal.mem_span_singleton_self p)
  let : IsLocalRing Rn :=
    isLocalRing_adjoinRoot_X_pow_sub_C hN hpMem
  let J : Ideal D :=
    (IsLocalRing.maximalIdeal Rn).comap (algebraMap D Rn)
  have hrootMap : algebraMap D Rn (AdjoinRoot.root fR) =
      AdjoinRoot.root fV := by
    exact adjoinRootLocalizationBaseChangeAlgebra_root N p hp
  have hbaseMap (r : R) : algebraMap D Rn (algebraMap R D r) =
      algebraMap V Rn (algebraMap R V r) := by
    exact adjoinRootLocalizationBaseChangeAlgebra_base N p r hp
  have hqJ : q ≤ J := by
    rw [Ideal.span_le]
    rintro _ (rfl : _ = AdjoinRoot.root fR)
    change algebraMap D Rn (AdjoinRoot.root fR) ∈
      IsLocalRing.maximalIdeal Rn
    rw [hrootMap]
    apply (inferInstance : (IsLocalRing.maximalIdeal Rn).IsPrime).mem_of_pow_mem N
    rw [adjoinRoot_root_pow]
    rw [maximalIdeal_adjoinRoot_X_pow_sub_C hN hpMem]
    exact
      (show Ideal.map (AdjoinRoot.of fV) (IsLocalRing.maximalIdeal V) ≤
          localRootCoverClosedIdeal V N pV from le_sup_left)
        (Ideal.mem_map_of_mem (AdjoinRoot.of fV) hpMem)
  have hJUnder : J.under R = P := by
    apply le_antisymm
    · intro r hr
      by_contra hrP
      have hrUnitV : IsUnit (algebraMap R V r) :=
        IsLocalization.map_units V (⟨r, hrP⟩ : P.primeCompl)
      have hrUnitRn : IsUnit (algebraMap V Rn (algebraMap R V r)) :=
        hrUnitV.map (algebraMap V Rn)
      have hnonmem : algebraMap D Rn (algebraMap R D r) ∉
          IsLocalRing.maximalIdeal Rn := by
        rw [hbaseMap]
        exact IsLocalRing.notMem_maximalIdeal.mpr hrUnitRn
      exact hnonmem hr
    · rw [Ideal.LiesOver.over (P := q) (p := P)]
      exact Ideal.comap_mono hqJ
  have hJq : J = q := by
    apply le_antisymm
    · by_contra hnot
      have hne : q ≠ J := by
        intro heq
        exact hnot heq.ge
      have hlt : q < J := lt_of_le_of_ne hqJ hne
      have : Module.Finite R D :=
        (Polynomial.monic_X_pow_sub_C p hN.ne').finite_adjoinRoot
      have : Algebra.IsIntegral R D := Algebra.IsIntegral.of_finite R D
      have hstrict :=
        Ideal.IsIntegral.under_lt_under (R := R) (A := D) hlt
      exact (ne_of_lt hstrict)
        ((Ideal.LiesOver.over (P := q) (p := P)).symm.trans
          hJUnder.symm)
    · exact hqJ
  have hMle : M ≤ q.primeCompl := by
    rintro _ ⟨r, hr, rfl⟩
    change algebraMap R D r ∉ q
    intro hmem
    exact hr ((Ideal.mem_of_liesOver (P := q) (p := P) r).mpr hmem)
  have hCofinal : ∀ d ∈ q.primeCompl, ∃ m ∈ M, d ∣ m := by
    intro d hd
    have hdUnit : IsUnit (algebraMap D Rn d) := by
      rw [← IsLocalRing.notMem_maximalIdeal]
      intro hdMax
      have : d ∈ J := hdMax
      rw [hJq] at this
      exact hd this
    exact (IsLocalization.algebraMap_isUnit_iff (M := M)).mp hdUnit
  have hRnq : IsLocalization q.primeCompl Rn :=
    (IsLocalization.iff_of_le_of_exists_dvd (M := M)
      q.primeCompl hMle hCofinal).mp hRnM
  exact hRnq

def adjoinRootLocalizationAtRootPrimeAlgEquiv
    {R : Type u} [CommRing R] [IsDomain R]
    {N : ℕ} (hN : 0 < N) {p : R} (hp : Prime p) :
    let P := Ideal.span ({p} : Set R)
    let D := AdjoinRoot (X ^ N - C p)
    let q := Ideal.span
      ({AdjoinRoot.root (X ^ N - C p)} : Set D)
    letI : P.IsPrime := Ideal.isPrime_span_singleton_of_prime hp
    letI : q.IsPrime := Ideal.isPrime_span_singleton_of_prime
      (prime_adjoinRoot_root_of_prime hN hp)
    let V := Localization.AtPrime P
    let Rn := AdjoinRoot (X ^ N - C (algebraMap R V p))
    letI : Algebra D Rn :=
      adjoinRootLocalizationBaseChangeAlgebra R N p hp
    letI : q.LiesOver P := span_root_liesOver_span_radicand hN hp
    letI : Algebra V (Localization.AtPrime q) :=
      Localization.AtPrime.algebraOfLiesOver P q
    Rn ≃ₐ[V] Localization.AtPrime q := by
  dsimp only
  let P := Ideal.span ({p} : Set R)
  let D := AdjoinRoot (X ^ N - C p)
  let q := Ideal.span
    ({AdjoinRoot.root (X ^ N - C p)} : Set D)
  letI : P.IsPrime := Ideal.isPrime_span_singleton_of_prime hp
  letI : q.IsPrime := Ideal.isPrime_span_singleton_of_prime
    (prime_adjoinRoot_root_of_prime hN hp)
  let V := Localization.AtPrime P
  let Rn := AdjoinRoot (X ^ N - C (algebraMap R V p))
  letI : Algebra D Rn :=
    adjoinRootLocalizationBaseChangeAlgebra R N p hp
  letI : q.LiesOver P := span_root_liesOver_span_radicand hN hp
  letI : IsLocalization q.primeCompl Rn :=
    isLocalization_adjoinRootLocalizationAtRootPrime hN hp
  let Dq := Localization.AtPrime q
  let eRoot : Rn ≃ₐ[D] Dq :=
    IsLocalization.algEquiv q.primeCompl Rn Dq
  letI : Algebra V Dq :=
    Localization.AtPrime.algebraOfLiesOver P q
  have hcommutes : eRoot.toRingHom.comp (algebraMap V Rn) =
      algebraMap V Dq := by
    apply IsLocalization.ringHom_ext P.primeCompl
    rw [RingHom.comp_assoc]
    ext r
    change eRoot (algebraMap V Rn (algebraMap R V r)) =
      algebraMap V Dq (algebraMap R V r)
    rw [← adjoinRootLocalizationBaseChangeAlgebra_base N p r hp]
    calc
      eRoot (algebraMap D Rn (algebraMap R D r)) =
          algebraMap D Dq (algebraMap R D r) := eRoot.commutes _
      _ = algebraMap V Dq (algebraMap R V r) := by
        rw [← IsScalarTower.algebraMap_apply R D Dq,
          ← IsScalarTower.algebraMap_apply R V Dq]
  exact
    { eRoot.toRingEquiv with
      commutes' := fun v ↦ DFunLike.congr_fun hcommutes v }

theorem adjoinRootLocalizationAtRootPrimeAlgEquiv_root
    {R : Type u} [CommRing R] [IsDomain R]
    {N : ℕ} (hN : 0 < N) {p : R} (hp : Prime p) :
    let P := Ideal.span ({p} : Set R)
    let D := AdjoinRoot (X ^ N - C p)
    let q := Ideal.span
      ({AdjoinRoot.root (X ^ N - C p)} : Set D)
    letI : P.IsPrime := Ideal.isPrime_span_singleton_of_prime hp
    letI : q.IsPrime := Ideal.isPrime_span_singleton_of_prime
      (prime_adjoinRoot_root_of_prime hN hp)
    let V := Localization.AtPrime P
    let Rn := AdjoinRoot (X ^ N - C (algebraMap R V p))
    letI : Algebra D Rn :=
      adjoinRootLocalizationBaseChangeAlgebra R N p hp
    letI : q.LiesOver P := span_root_liesOver_span_radicand hN hp
    letI : Algebra V (Localization.AtPrime q) :=
      Localization.AtPrime.algebraOfLiesOver P q
    adjoinRootLocalizationAtRootPrimeAlgEquiv hN hp
        (AdjoinRoot.root (X ^ N - C (algebraMap R V p))) =
      algebraMap D (Localization.AtPrime q)
        (AdjoinRoot.root (X ^ N - C p)) := by
  dsimp only
  let P := Ideal.span ({p} : Set R)
  let D := AdjoinRoot (X ^ N - C p)
  let q := Ideal.span
    ({AdjoinRoot.root (X ^ N - C p)} : Set D)
  let : P.IsPrime := Ideal.isPrime_span_singleton_of_prime hp
  let : q.IsPrime := Ideal.isPrime_span_singleton_of_prime
    (prime_adjoinRoot_root_of_prime hN hp)
  let V := Localization.AtPrime P
  let Rn := AdjoinRoot (X ^ N - C (algebraMap R V p))
  let : Algebra D Rn :=
    adjoinRootLocalizationBaseChangeAlgebra R N p hp
  let : q.LiesOver P := span_root_liesOver_span_radicand hN hp
  let : IsLocalization q.primeCompl Rn :=
    isLocalization_adjoinRootLocalizationAtRootPrime hN hp
  let Dq := Localization.AtPrime q
  let eRoot : Rn ≃ₐ[D] Dq :=
    IsLocalization.algEquiv q.primeCompl Rn Dq
  let : Algebra V Dq :=
    Localization.AtPrime.algebraOfLiesOver P q
  change eRoot (AdjoinRoot.root (X ^ N - C (algebraMap R V p))) =
    algebraMap D Dq (AdjoinRoot.root (X ^ N - C p))
  rw [← adjoinRootLocalizationBaseChangeAlgebra_root N p hp]
  exact eRoot.commutes _