NYLL
Module

StandardCompletion.lean

Nyll.EtaleFundamentalGroups.Kummer.SelectedRoot.Prime.StandardCompletion
4 declarations indexed from sourceView source ↗

Module documentation

The actual completion of the selected root divisor

The completed-base-change ring attached to the selected root divisor is not merely faithfully flat over the selected local ring: it is its canonical adic, hence valued-field, completion. The essential calculation is that the image of the maximal ideal of the radicand DVR is the N-th power of the maximal ideal generated by the adjoined root.

Imports3
Imported by5

Declarations

theorem

adjoinRootLocalizationAtRootPrime_isDomain

L33 ↗
EtaleFundamentalGroups.Kummer.adjoinRootLocalizationAtRootPrime_isDomain
Documentation

The selected local root ring is a domain, transported from the pure-root DVR over the localization at the radicand divisor.

Source context 5 commands

Surrounding namespaces, section variables, and local commands at this declaration.

noncomputable section
open scoped TensorProduct
namespace EtaleFundamentalGroups.Kummer
open Polynomial
universe u
Lean source · full declaration
theorem adjoinRootLocalizationAtRootPrime_isDomain
    {R : Type u} [CommRing R] [IsDomain R] [IsRegularRing 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)
    letI : q.LiesOver P := span_root_liesOver_span_radicand hN hp
    let V := Localization.AtPrime P
    letI : Algebra V (Localization.AtPrime q) :=
      Localization.AtPrime.algebraOfLiesOver P q
    IsDomain (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)
  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 : IsDiscreteValuationRing V :=
    EtaleFundamentalGroups.isDiscreteValuationRing_localizationAtSpan_of_prime
      R p hp
  let pV : V := algebraMap R V p
  have hmaxV : IsLocalRing.maximalIdeal V =
      Ideal.span ({pV} : Set V) :=
    localizationAtPrime_maximalIdeal_eq_span_of_eq_span P p rfl
  have hpVne : pV ≠ 0 := by
    intro hpVzero
    apply hp.ne_zero
    exact (IsLocalization.injective V P.primeCompl_le_nonZeroDivisors)
      (by simpa only [map_zero] using hpVzero)
  have hpV : Prime pV :=
    (IsDiscreteValuationRing.irreducible_of_span_eq_maximalIdeal
      pV hpVne hmaxV).prime
  let Rn := AdjoinRoot (X ^ N - C pV)
  let : IsDomain Rn :=
    isDomain_adjoinRoot_X_pow_sub_C_of_prime hN pV hpV
  let : Algebra D Rn :=
    adjoinRootLocalizationBaseChangeAlgebra R N p hp
  let W := Localization.AtPrime q
  let : Algebra V W :=
    Localization.AtPrime.algebraOfLiesOver P q
  let eLocal : Rn ≃ₐ[V] W :=
    adjoinRootLocalizationAtRootPrimeAlgEquiv hN hp
  exact eLocal.symm.toMulEquiv.isDomain Rn
theorem

adjoinRootLocalizationAtRootPrime_isDiscreteValuationRing

L87 ↗
EtaleFundamentalGroups.Kummer.adjoinRootLocalizationAtRootPrime_isDiscreteValuationRing
Documentation

The selected local root ring is a DVR. This is the transported DVR structure on the pure-root ring over the radicand DVR.

Source context 5 commands

Surrounding namespaces, section variables, and local commands at this declaration.

noncomputable section
open scoped TensorProduct
namespace EtaleFundamentalGroups.Kummer
open Polynomial
universe u
Lean source · full declaration
theorem adjoinRootLocalizationAtRootPrime_isDiscreteValuationRing
    {R : Type u} [CommRing R] [IsDomain R] [IsRegularRing 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)
    letI : q.LiesOver P := span_root_liesOver_span_radicand hN hp
    let V := Localization.AtPrime P
    letI : Algebra V (Localization.AtPrime q) :=
      Localization.AtPrime.algebraOfLiesOver P q
    letI : IsDomain (Localization.AtPrime q) :=
      adjoinRootLocalizationAtRootPrime_isDomain hN hp
    IsDiscreteValuationRing (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)
  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 : IsDiscreteValuationRing V :=
    EtaleFundamentalGroups.isDiscreteValuationRing_localizationAtSpan_of_prime
      R p hp
  let pV : V := algebraMap R V p
  have hmaxV : IsLocalRing.maximalIdeal V =
      Ideal.span ({pV} : Set V) :=
    localizationAtPrime_maximalIdeal_eq_span_of_eq_span P p rfl
  have hpVne : pV ≠ 0 := by
    intro hpVzero
    apply hp.ne_zero
    exact (IsLocalization.injective V P.primeCompl_le_nonZeroDivisors)
      (by simpa only [map_zero] using hpVzero)
  have hpV : Prime pV :=
    (IsDiscreteValuationRing.irreducible_of_span_eq_maximalIdeal
      pV hpVne hmaxV).prime
  let Rn := AdjoinRoot (X ^ N - C pV)
  let : IsDomain Rn :=
    isDomain_adjoinRoot_X_pow_sub_C_of_prime hN pV hpV
  let : IsDiscreteValuationRing Rn :=
    isDiscreteValuationRing_adjoinRoot_X_pow_sub_C_of_prime hN pV hpV
  let : Algebra D Rn :=
    adjoinRootLocalizationBaseChangeAlgebra R N p hp
  let W := Localization.AtPrime q
  let : Algebra V W :=
    Localization.AtPrime.algebraOfLiesOver P q
  let eLocal : Rn ≃ₐ[V] W :=
    adjoinRootLocalizationAtRootPrimeAlgEquiv hN hp
  let : IsDomain W :=
    adjoinRootLocalizationAtRootPrime_isDomain hN hp
  exact
    IsDiscreteValuationRing.RingEquivClass.isDiscreteValuationRing
      eLocal.toRingEquiv
theorem

adjoinRootLocalizationAtRootPrime_maximalIdeal_map_eq_pow

L151 ↗
EtaleFundamentalGroups.Kummer.adjoinRootLocalizationAtRootPrime_maximalIdeal_map_eq_pow
Documentation

In the selected root localization, the image of the radicand DVR's maximal ideal is exactly the N-th power of the root DVR's maximal ideal. This equality is the cofinality input identifying completed base change with the actual completion of the selected local ring.

Source context 5 commands

Surrounding namespaces, section variables, and local commands at this declaration.

noncomputable section
open scoped TensorProduct
namespace EtaleFundamentalGroups.Kummer
open Polynomial
universe u
Lean source · full declaration
theorem adjoinRootLocalizationAtRootPrime_maximalIdeal_map_eq_pow
    {R : Type u} [CommRing R] [IsDomain R] [IsRegularRing 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)
    letI : q.LiesOver P := span_root_liesOver_span_radicand hN hp
    let V := Localization.AtPrime P
    let W := Localization.AtPrime q
    letI : Algebra V W :=
      Localization.AtPrime.algebraOfLiesOver P q
    (IsLocalRing.maximalIdeal V).map (algebraMap V W) =
      IsLocalRing.maximalIdeal W ^ N := by
  dsimp only
  let P := Ideal.span ({p} : Set R)
  let fR : R[X] := X ^ N - C p
  let D := AdjoinRoot fR
  let rootR := AdjoinRoot.root fR
  let q := Ideal.span ({rootR} : 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 W := Localization.AtPrime q
  let : Algebra D Rn :=
    adjoinRootLocalizationBaseChangeAlgebra R N p hp
  let : Algebra V W :=
    Localization.AtPrime.algebraOfLiesOver P q
  let eLocal : Rn ≃ₐ[V] W :=
    adjoinRootLocalizationAtRootPrimeAlgEquiv hN hp
  let rootV := AdjoinRoot.root fV
  let rootW : W := algebraMap D W rootR
  have hmaxV : IsLocalRing.maximalIdeal V =
      Ideal.span ({pV} : Set V) :=
    localizationAtPrime_maximalIdeal_eq_span_of_eq_span P p rfl
  have hmaxW : IsLocalRing.maximalIdeal W =
      Ideal.span ({rootW} : Set W) :=
    localizationAtPrime_maximalIdeal_eq_span_of_eq_span q rootR rfl
  have hroot : eLocal rootV = rootW := by
    simpa only [fR, D, rootR, pV, fV, Rn, W, rootV, rootW] using
      adjoinRootLocalizationAtRootPrimeAlgEquiv_root hN hp
  have hrootPow : rootV ^ N = algebraMap V Rn pV := by
    rw [AdjoinRoot.algebraMap_eq]
    simpa only [fV, rootV] using adjoinRoot_root_pow N pV
  have hpMap : algebraMap V W pV = rootW ^ N := by
    calc
      algebraMap V W pV = eLocal (algebraMap V Rn pV) :=
        (eLocal.commutes pV).symm
      _ = eLocal (rootV ^ N) := by rw [hrootPow]
      _ = rootW ^ N := by rw [map_pow, hroot]
  calc
    (IsLocalRing.maximalIdeal V).map (algebraMap V W) =
        (Ideal.span ({pV} : Set V)).map (algebraMap V W) := by
      rw [hmaxV]
    _ = Ideal.span ({algebraMap V W pV} : Set W) := by
      rw [Ideal.map_span, Set.image_singleton]
    _ = Ideal.span ({rootW ^ N} : Set W) := by rw [hpMap]
    _ = IsLocalRing.maximalIdeal W ^ N := by
      rw [hmaxW, Ideal.span_singleton_pow]
def

adjoinRootLocalizationAtRootPrimeStandardCompletionAlgEquiv

L226 ↗
EtaleFundamentalGroups.Kummer.adjoinRootLocalizationAtRootPrimeStandardCompletionAlgEquiv
Documentation

The valuation subring in the standard valued-field completion of the actual selected local ring is canonically the completed pure-root ring over the standard completion of the radicand DVR.

The equivalence is an equivalence over the actual local ring W. Thus it identifies the canonical completion map from W with the map to the completed root ring already used by the complete higher-radical theorem.

Source context 5 commands

Surrounding namespaces, section variables, and local commands at this declaration.

noncomputable section
open scoped TensorProduct
namespace EtaleFundamentalGroups.Kummer
open Polynomial
universe u
Lean source · full declaration
def
    adjoinRootLocalizationAtRootPrimeStandardCompletionAlgEquiv
    {R : Type u} [CommRing R] [IsDomain R] [IsRegularRing 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)
    letI : q.LiesOver P := span_root_liesOver_span_radicand hN hp
    let V := Localization.AtPrime P
    letI : IsDiscreteValuationRing V :=
      EtaleFundamentalGroups.isDiscreteValuationRing_localizationAtSpan_of_prime
        R p hp
    let K := FractionRing V
    let Vhat := standardDVFCompletionValuationSubring V K
    letI : Algebra V Vhat :=
      standardDVFCompletionValuationSubringAlgebra V K
    let pV := algebraMap R V p
    let pHat := standardDVRCompletionValuationSubringElement V K pV
    let Rhat := AdjoinRoot (X ^ N - C pHat)
    let W := Localization.AtPrime q
    letI : Algebra V W :=
      Localization.AtPrime.algebraOfLiesOver P q
    letI : IsDomain W :=
      adjoinRootLocalizationAtRootPrime_isDomain hN hp
    letI : IsDiscreteValuationRing W :=
      adjoinRootLocalizationAtRootPrime_isDiscreteValuationRing hN hp
    let L := FractionRing W
    let What := standardDVFCompletionValuationSubring W L
    letI : Algebra W What :=
      standardDVFCompletionValuationSubringAlgebra W L
    letI : Algebra W Rhat :=
      adjoinRootLocalizationAtRootPrimeCompletionAlgebra hN hp
    What ≃ₐ[W] Rhat := 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)
  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)
  letI : q.LiesOver P := span_root_liesOver_span_radicand hN hp
  let V := Localization.AtPrime P
  letI : IsDiscreteValuationRing V :=
    EtaleFundamentalGroups.isDiscreteValuationRing_localizationAtSpan_of_prime
      R p hp
  let K := FractionRing V
  let Vhat := standardDVFCompletionValuationSubring V K
  letI : Algebra V Vhat :=
    standardDVFCompletionValuationSubringAlgebra V K
  let pV : V := algebraMap R V p
  let fV : V[X] := X ^ N - C pV
  let Rn := AdjoinRoot fV
  let pHat := standardDVRCompletionValuationSubringElement V K pV
  let Rhat := AdjoinRoot (X ^ N - C pHat)
  let W := Localization.AtPrime q
  letI : Algebra D Rn :=
    adjoinRootLocalizationBaseChangeAlgebra R N p hp
  letI : Algebra V W :=
    Localization.AtPrime.algebraOfLiesOver P q
  let eLocal : Rn ≃ₐ[V] W :=
    adjoinRootLocalizationAtRootPrimeAlgEquiv hN hp
  letI : IsDomain W :=
    adjoinRootLocalizationAtRootPrime_isDomain hN hp
  letI : IsDiscreteValuationRing W :=
    adjoinRootLocalizationAtRootPrime_isDiscreteValuationRing hN hp
  let L := FractionRing W
  let What := standardDVFCompletionValuationSubring W L
  letI : Algebra W What :=
    standardDVFCompletionValuationSubringAlgebra W L
  letI : Algebra W Rhat :=
    adjoinRootLocalizationAtRootPrimeCompletionAlgebra hN hp
  let I := IsLocalRing.maximalIdeal V
  let J := IsLocalRing.maximalIdeal W
  letI : Module.Finite V Rn :=
    (Polynomial.monic_X_pow_sub_C pV hN.ne').finite_adjoinRoot
  letI : Module.Free V Rn :=
    (Polynomial.monic_X_pow_sub_C pV hN.ne').free_adjoinRoot
  letI : Module.Finite V W :=
    Module.Finite.equiv eLocal.toLinearEquiv
  letI : Module.Free V W :=
    Module.Free.of_equiv eLocal.toLinearEquiv
  let eBase : AdicCompletion I V ≃ₐ[V] Vhat :=
    standardDVRAdicCompletionEquivCompletionValuationSubring V K
  let T := Vhat ⊗[V] W
  let T₀ := AdicCompletion I V ⊗[V] W
  letI : Algebra W T := Algebra.TensorProduct.rightAlgebra
  letI : Algebra W T₀ := Algebra.TensorProduct.rightAlgebra
  let eTensor₀ : T ≃ₐ[V] T₀ :=
    Algebra.TensorProduct.congr eBase.symm (AlgEquiv.refl : W ≃ₐ[V] W)
  let eTensor : T ≃ₐ[W] T₀ :=
    AlgEquiv.ofRingEquiv (R := W) (f := eTensor₀.toRingEquiv) (fun w ↦ by
      change eTensor₀ (Algebra.TensorProduct.includeRight w) =
        Algebra.TensorProduct.includeRight w
      change (Algebra.TensorProduct.congr eBase.symm
        (AlgEquiv.refl : W ≃ₐ[V] W)) (1 ⊗ₜ[V] w) = 1 ⊗ₜ[V] w
      rw [Algebra.TensorProduct.congr_apply,
        Algebra.TensorProduct.map_tmul]
      simp)
  let eMapped₀ : T₀ ≃+*
      AdicCompletion (I.map (algebraMap V W)) W :=
    tensorProductMappedIdealCompletionFreeRingEquiv I
  let eMapped : T₀ ≃ₐ[W]
      AdicCompletion (I.map (algebraMap V W)) W :=
    AlgEquiv.ofRingEquiv (R := W) (f := eMapped₀) (fun w ↦ by
      change eMapped₀ (Algebra.TensorProduct.includeRight w) =
        AdicCompletion.of (I.map (algebraMap V W)) W w
      exact
        tensorProductMappedIdealCompletionFreeRingEquiv_includeRight_apply
          I w)
  let ePower : AdicCompletion (I.map (algebraMap V W)) W ≃ₐ[W]
      AdicCompletion J W := by
    rw [adjoinRootLocalizationAtRootPrime_maximalIdeal_map_eq_pow hN hp]
    exact adicCompletionPowerAlgEquiv J N hN
  let eActual : AdicCompletion J W ≃ₐ[W] What :=
    standardDVRAdicCompletionEquivCompletionValuationSubring W L
  let eCompletion₀ : T ≃ₐ[Vhat] Rhat :=
    adjoinRootLocalizationAtRootPrimeCompletionAlgEquiv hN hp
  let eCompletion : T ≃ₐ[W] Rhat :=
    AlgEquiv.ofRingEquiv (R := W) (f := eCompletion₀.toRingEquiv)
      (fun _ ↦ rfl)
  exact
    (((eActual.symm.trans ePower.symm).trans eMapped.symm).trans
      eTensor.symm).trans eCompletion

Statements and documentation are read from the Lean source at the revision shown. Source entries are not a measure of mathematical completeness.