NYLL
Module

Completion.lean

Nyll.EtaleFundamentalGroups.Kummer.SelectedRoot.Prime.Completion
5 declarations indexed from sourceView source ↗

Module documentation

Completion of the selected root divisor

At the prime generated by a positive Kummer root, the local root cover is already the root cover of the localized radicand DVR. This file combines that localization comparison with the canonical DVR completion comparison. Thus the completed selected local ring is the same completed root ring used by the complete higher-radical actual-factor theorem; no second root cover is introduced.

Imports6
Imported by5

Declarations

theorem

charZero_standardDVFCompletionCompleteDVF_residueField

L38 ↗
EtaleFundamentalGroups.Kummer.charZero_standardDVFCompletionCompleteDVF_residueField
Documentation

Characteristic zero of a DVR residue ring passes to the residue field of its canonical complete DVF.

Source context 6 commands

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

noncomputable section
open scoped TensorProduct
namespace EtaleFundamentalGroups.Kummer
open Polynomial
open ValuationTheory.DiscreteValuationField
universe uR uK uK₀ uL
Lean source · statement
theorem charZero_standardDVFCompletionCompleteDVF_residueField
    (V : Type uR) (K : Type uK)
    [CommRing V] [IsDomain V] [IsDiscreteValuationRing V]
    [Field K] [Algebra V K] [IsFractionRing V K]
    (hCharZero : CharZero
      (V ⧸ IsLocalRing.maximalIdeal V)) :
    CharZero (standardDVFCompletionCompleteDVF V K).residueField
def

adjoinRootLocalizationAtRootPrimeCompletionAlgEquiv

L61 ↗
EtaleFundamentalGroups.Kummer.adjoinRootLocalizationAtRootPrimeCompletionAlgEquiv
Documentation

The completion base change of the selected local root cover is the completed root ring over the radicand DVR.

The source is the actual local ring at the root prime. The target is formed by completing the radicand DVR first and adjoining the same root there.

Source context 6 commands

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

noncomputable section
open scoped TensorProduct
namespace EtaleFundamentalGroups.Kummer
open Polynomial
open ValuationTheory.DiscreteValuationField
universe uR uK uK₀ uL
Lean source · full declaration
def adjoinRootLocalizationAtRootPrimeCompletionAlgEquiv
    {R : Type uR} [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)
    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)
    letI : q.LiesOver P := span_root_liesOver_span_radicand hN hp
    letI : Algebra V (Localization.AtPrime q) :=
      Localization.AtPrime.algebraOfLiesOver P q
    Vhat ⊗[V] Localization.AtPrime q ≃ₐ[Vhat] Rhat := 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
  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 Rn := AdjoinRoot (X ^ N - C pV)
  let pHat := standardDVRCompletionValuationSubringElement V K pV
  let Rhat := AdjoinRoot (X ^ N - C pHat)
  letI : q.LiesOver P := span_root_liesOver_span_radicand hN hp
  letI : Algebra V (Localization.AtPrime q) :=
    Localization.AtPrime.algebraOfLiesOver P q
  let eLocal : Rn ≃ₐ[V] Localization.AtPrime q :=
    adjoinRootLocalizationAtRootPrimeAlgEquiv hN hp
  let eTensor :
      (Vhat ⊗[V] Localization.AtPrime q) ≃ₐ[Vhat]
        (Vhat ⊗[V] Rn) :=
    Algebra.TensorProduct.congr
      (AlgEquiv.refl : Vhat ≃ₐ[Vhat] Vhat) eLocal.symm
  exact eTensor.trans (standardDVRRootCompletionAlgEquiv V K N pV)
def

adjoinRootLocalizationAtRootPrimeCompletionAlgebra

L121 ↗
EtaleFundamentalGroups.Kummer.adjoinRootLocalizationAtRootPrimeCompletionAlgebra
Documentation

The canonical algebra structure on the completed root ring, read from the actual selected local ring through completion base change.

Source context 6 commands

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

noncomputable section
open scoped TensorProduct
namespace EtaleFundamentalGroups.Kummer
open Polynomial
open ValuationTheory.DiscreteValuationField
universe uR uK uK₀ uL
Lean source · full declaration
def adjoinRootLocalizationAtRootPrimeCompletionAlgebra
    {R : Type uR} [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)
    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)
    letI : q.LiesOver P := span_root_liesOver_span_radicand hN hp
    letI : Algebra V (Localization.AtPrime q) :=
      Localization.AtPrime.algebraOfLiesOver P q
    Algebra (Localization.AtPrime q) Rhat := 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
  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)
  letI : q.LiesOver P := span_root_liesOver_span_radicand hN hp
  letI : Algebra V (Localization.AtPrime q) :=
    Localization.AtPrime.algebraOfLiesOver P q
  let T := Vhat ⊗[V] Localization.AtPrime q
  let e := adjoinRootLocalizationAtRootPrimeCompletionAlgEquiv hN hp
  exact
    (e.toRingEquiv.toRingHom.comp
      (Algebra.TensorProduct.includeRight :
        Localization.AtPrime q →ₐ[V] T).toRingHom).toAlgebra
theorem

adjoinRootLocalizationAtRootPrimeCompletion_faithfullyFlat

L177 ↗
EtaleFundamentalGroups.Kummer.adjoinRootLocalizationAtRootPrimeCompletion_faithfullyFlat
Documentation

Completion of the selected local root cover is faithfully flat over the actual local ring at the root prime.

Source context 6 commands

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

noncomputable section
open scoped TensorProduct
namespace EtaleFundamentalGroups.Kummer
open Polynomial
open ValuationTheory.DiscreteValuationField
universe uR uK uK₀ uL
Lean source · full declaration
theorem adjoinRootLocalizationAtRootPrimeCompletion_faithfullyFlat
    {R : Type uR} [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)
    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)
    letI : q.LiesOver P := span_root_liesOver_span_radicand hN hp
    letI : Algebra V (Localization.AtPrime q) :=
      Localization.AtPrime.algebraOfLiesOver P q
    letI : Algebra (Localization.AtPrime q) Rhat :=
      adjoinRootLocalizationAtRootPrimeCompletionAlgebra hN hp
    Module.FaithfullyFlat (Localization.AtPrime q) Rhat := 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 : IsDiscreteValuationRing V :=
    EtaleFundamentalGroups.isDiscreteValuationRing_localizationAtSpan_of_prime
      R p hp
  let K := FractionRing V
  let Vhat := standardDVFCompletionValuationSubring V K
  let : 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 : q.LiesOver P := span_root_liesOver_span_radicand hN hp
  let : Algebra V (Localization.AtPrime q) :=
    Localization.AtPrime.algebraOfLiesOver P q
  let : Algebra (Localization.AtPrime q) Rhat :=
    adjoinRootLocalizationAtRootPrimeCompletionAlgebra hN hp
  let T := Vhat ⊗[V] Localization.AtPrime q
  let T' := Localization.AtPrime q ⊗[V] Vhat
  let : Module.FaithfullyFlat V Vhat :=
    standardDVRCompletionValuationSubring_faithfullyFlat
      (V := V) (K := K)
  let : Algebra (Localization.AtPrime q) T :=
    Algebra.TensorProduct.rightAlgebra
  let : Module.FaithfullyFlat (Localization.AtPrime q) T' :=
    inferInstance
  let eComm : T ≃ₐ[Localization.AtPrime q] T' :=
    AlgEquiv.ofRingEquiv (R := Localization.AtPrime q)
      (f := (Algebra.TensorProduct.comm V Vhat
        (Localization.AtPrime q)).toRingEquiv)
      (fun _ ↦ rfl)
  let : Module.FaithfullyFlat (Localization.AtPrime q) T :=
    Module.FaithfullyFlat.of_linearEquiv
      (R := Localization.AtPrime q) (M := T') eComm.toLinearEquiv
  let eCompletion :=
    adjoinRootLocalizationAtRootPrimeCompletionAlgEquiv hN hp
  let eRoot : T ≃ₐ[Localization.AtPrime q] Rhat :=
    AlgEquiv.ofRingEquiv (R := Localization.AtPrime q)
      (f := eCompletion.toRingEquiv) (fun _ ↦ rfl)
  exact Module.FaithfullyFlat.of_linearEquiv
    (R := Localization.AtPrime q) (M := T) eRoot.symm.toLinearEquiv
theorem

integralClosure_standardDVRCompletionFactorialRoot_originalTensorProduct_etale

L260 ↗
EtaleFundamentalGroups.Kummer.integralClosure_standardDVRCompletionFactorialRoot_originalTensorProduct_etale
Documentation

The canonical completion of a DVR supplies all complete-base inputs for the factorial-root tensor-product theorem.

Only the displayed generator of the original maximal ideal and residue characteristic are required. The completed uniformizer, the complete-DVF residue characteristic, every tensor component, and the product normalization are produced internally.

Source context 6 commands

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

noncomputable section
open scoped TensorProduct
namespace EtaleFundamentalGroups.Kummer
open Polynomial
open ValuationTheory.DiscreteValuationField
universe uR uK uK₀ uL
Lean source · full declaration
theorem
    integralClosure_standardDVRCompletionFactorialRoot_originalTensorProduct_etale
    (V : Type uR) (K : Type uK)
    [CommRing V] [IsDomain V] [IsDiscreteValuationRing V]
    [Field K] [Algebra V K] [IsFractionRing V K]
    (pi : V)
    (hpi : IsLocalRing.maximalIdeal V = Ideal.span ({pi} : Set V))
    (hCharZero : CharZero (V ⧸ IsLocalRing.maximalIdeal V))
    {K₀ : Type uK₀} {L : Type uL}
    [Field K₀] [Field L]
    [Algebra K₀ (standardDVFCompletionField V K)] [Algebra K₀ L]
    [FiniteDimensional K₀ L] [Algebra.IsSeparable K₀ L]
    (D : ℕ) (hdegree : Module.finrank K₀ L ≤ D) :
    let H := standardDVFCompletionCompleteDVF V K
    let Vhat := H.valuationSubring
    let Khat := standardDVFCompletionField V K
    let varpi := standardDVRCompletionValuationSubringElement V K pi
    letI : IsFractionRing Vhat Khat :=
      H.toDVF.valuationSubring_isFractionRing
    letI : IsIntegrallyClosed Vhat :=
      H.toDVF.valuationSubring_isIntegrallyClosed
    let N := D.factorial
    let Rhat := AdjoinRoot (X ^ N - C varpi)
    letI : IsDomain Rhat :=
      completeDVFFactorialRootRing_isDomain H varpi
        (standardDVRCompletionValuationSubringElement_isUniformizer
          V K pi hpi) D
    let Fhat := FractionRing Rhat
    letI : Algebra Khat Fhat :=
      completeDVFFactorialRootFractionFieldAlgebra H varpi
        (standardDVRCompletionValuationSubringElement_isUniformizer
          V K pi hpi) D
    letI : IsScalarTower Vhat Khat Fhat :=
      completeDVFFactorialRootFractionField_isScalarTower H varpi
        (standardDVRCompletionValuationSubringElement_isUniformizer
          V K pi hpi) D
    letI : Algebra K₀ Fhat :=
      ((algebraMap Khat Fhat).comp (algebraMap K₀ Khat)).toAlgebra
    letI : IsScalarTower K₀ Khat Fhat :=
      IsScalarTower.of_algebraMap_eq fun _ ↦ rfl
    let G := Fhat ⊗[K₀] L
    letI : Algebra Rhat G :=
      genericTensorProductLeftScalarAlgebra
        (R := Rhat) (K := K₀) (F := Fhat) (L := L)
    Algebra.Etale Rhat (integralClosure Rhat G) := by
  dsimp only
  let H := standardDVFCompletionCompleteDVF V K
  let varpi := standardDVRCompletionValuationSubringElement V K pi
  have hvarpi : H.valuation.IsUniformizer
      (varpi : standardDVFCompletionField V K) :=
    standardDVRCompletionValuationSubringElement_isUniformizer
      V K pi hpi
  let : CharZero H.residueField :=
    charZero_standardDVFCompletionCompleteDVF_residueField
      V K hCharZero
  exact
    integralClosure_completeDVFFactorialRoot_originalTensorProduct_etale
      H varpi hvarpi D hdegree

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