Module

ExponentUnitCompletion.lean

Nyll.EtaleFundamentalGroups.Kummer.NormalCrossings.SelectedBranch.ExponentUnitCompletion

38 declarations indexed from sourceView source ↗

Module documentation

The selected exponent from the retained completed component

The selected full-root component supplies a height-one/closed prime chain in its finite normalization. Maximal-adic completion retains that literal chain. Contracting it through the canonical intermediate normalization selects the prefix component in the same completed factor.

The prefix component is then embedded in the fraction field of the retained closed factor. Its finite-etale residue-lift compositum carries both the original boundary-Away statement and the exact selected ramification prime, so the complete one-root terminal forces the exponent to be a unit.

Every component, prime, and comparison map used below is generated from the single global component returned by the strict-normal-crossings source theorem. In particular, the statement exposes no completed component comparison, right-coordinate bijectivity, or ramification-index hypothesis.

Imports17

Imported by3

theorem

prefixEmbedding_exactPrimeBoundaryAway_terminal_isUnit

L60 ↗

EtaleFundamentalGroups.Kummer.prefixEmbedding_exactPrimeBoundaryAway_terminal_isUnit

Documentation

Close the exact-prime terminal after selecting the literal compositum component determined by a prefix embedding. Keeping this construction in a separate opaque declaration prevents the actual-compositum definitions from being unfolded while checking the much larger selected-branch proof below.

Source context 7 commands

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

noncomputable section
open scoped TensorProduct
namespace EtaleFundamentalGroups.Kummer
open IsLocalRing
open Polynomial
open RingTheory.Sequence
universe u

Lean source · full declaration

theorem
    prefixEmbedding_exactPrimeBoundaryAway_terminal_isUnit
    {A C F KC M P : Type u}
    [CommRing A] [IsLocalRing A] [IsNoetherianRing A]
    [CommRing C] [IsLocalRing C] [Algebra A C]
    [Module.Finite A C] [Algebra.Etale A C] [FaithfulSMul A C]
    [Field F] [Algebra A F] [IsFractionRing A F]
    [Field KC] [Algebra C KC] [IsFractionRing C KC]
    [Algebra A KC] [IsScalarTower A C KC]
    [Algebra F KC] [IsScalarTower A F KC]
    [Field M] [Algebra A M] [Algebra F M]
    [IsScalarTower A F M] [FiniteDimensional F M] [IsGalois F M]
    [Field P] [Algebra A P] [Algebra C P] [IsScalarTower A C P]
    [Algebra F P] [IsScalarTower A F P]
    [Algebra KC P] [IsScalarTower C KC P]
    [Module.Finite A (integralClosure A M)]
    (y z : A)
    (hreg : RingTheory.Sequence.IsRegular A [y, z])
    (hgen : Ideal.ofList [y, z] = IsLocalRing.maximalIdeal A)
    (hdim : ringKrullDim A = ((2 : ℕ∞) : WithBot ℕ∞))
    (N : ℕ)
    (fPrefix : M →ₐ[F] P)
    (q : Ideal (integralClosure A M))
    (hqPrime : q.IsPrime)
    (hqOver : q.LiesOver (Ideal.span ({y} : Set A)))
    (hqExact : q.ramificationIdx A = N)
    (hAway :
      (Localization.awayMap
        (algebraMap A (integralClosure A M)) y).Etale)
    (hTerminal :
      ∀ {K₀ L₀ : Type u} [Field K₀] [Field L₀]
        [Algebra K₀ KC] [Algebra K₀ L₀]
        [FiniteDimensional K₀ L₀] [IsGalois K₀ L₀],
        ∀ (m : Ideal (KC ⊗[K₀] L₀)) (hm : m.IsMaximal),
          letI : m.IsMaximal := hm
          let Omega := GenericTensorFieldComponent m
          letI : Algebra C Omega :=
            ((algebraMap KC Omega).comp (algebraMap C KC)).toAlgebra
          letI : @IsScalarTower C KC Omega
              (inferInstance : Algebra C KC).toSMul
              (inferInstance : Algebra KC Omega).toSMul
              (((algebraMap KC Omega).comp
                (algebraMap C KC)).toAlgebra).toSMul :=
            by
              refine @IsScalarTower.of_algebraMap_eq C KC Omega
                _ _ _ (inferInstance : Algebra C KC)
                  (inferInstance : Algebra KC Omega)
                  (((algebraMap KC Omega).comp
                    (algebraMap C KC)).toAlgebra) ?_
              intro x
              rfl
          ∀ [Algebra Omega P] [IsScalarTower KC Omega P],
            let pC := Ideal.span ({algebraMap A C y} : Set C)
            ∀ (Q : Ideal (integralClosure C Omega)) [Q.IsPrime]
              [Q.LiesOver pC],
              Q.ramificationIdx C = N →
                (Localization.awayMap
                  (algebraMap C (integralClosure C Omega))
                  (algebraMap A C y)).Etale →
                  IsUnit (N : A)) :
    IsUnit (N : A) := by
  classical
  obtain
      ⟨mKC, hmKC, omegaToP, hTowerCKCOmega, hTowerOmega,
        hAwayOmega, QOmega, hQOmegaPrime, hQOmegaOver, hQOmegaExact⟩ :=
    completeRegularPair_prefixEmbedding_actualCompositum_exactPrime_boundaryAway
      (A := A) (C := C) (F := F) (KC := KC) (M := M) (P := P)
      y z hreg hgen hdim N fPrefix q hqPrime hqOver hqExact hAway
  let Omega := GenericTensorFieldComponent mKC
  let cOmegaAlgebra : Algebra C Omega :=
    ((algebraMap KC Omega).comp (algebraMap C KC)).toAlgebra
  let : Algebra Omega P := omegaToP.toRingHom.toAlgebra
  exact hTerminal (K₀ := F) (L₀ := M)
    mKC hmKC QOmega hQOmegaExact hAwayOmega

theorem

selectedExponent_prefix_localization_dvr

L138 ↗

EtaleFundamentalGroups.Kummer.selectedExponent_prefix_localization_dvr

Documentation

Produce only the domain/DVR facts needed from the retained vertical localization. The localization algebra and flatness instances stay inside this small scope.

Source context 7 commands

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

noncomputable section
open scoped TensorProduct
namespace EtaleFundamentalGroups.Kummer
open IsLocalRing
open Polynomial
open RingTheory.Sequence
universe u

Lean source · statement

theorem selectedExponent_prefix_localization_dvr
    {R S R' : Type u}
    [CommRing R] [CommRing S] [CommRing R']
    [Algebra R S] [Algebra R R']
    [IsDomain S] [IsIntegrallyClosed S] [IsNoetherianRing S]
    [hR'Noetherian : IsNoetherianRing R']
    [Module.Finite R S] [Module.Flat R R']
    (y : R)
    (q : Ideal S) [q.IsPrime]
    [q.LiesOver (Ideal.span ({y} : Set R))]
    (Q : Ideal (R' ⊗[R] S)) [hQPrime : Q.IsPrime]
    [_hQBranch : Q.LiesOver
      (Ideal.span ({algebraMap R R' y} : Set R'))]
    (hQRight :
      Q.comap Algebra.TensorProduct.includeRight.toRingHom = q)
    (hqHeight : q.height = 1)
    [hCharZero : CharZero (R ⧸ Ideal.span ({y} : Set R))] :
    ∃ _hWDomain : IsDomain (Localization.AtPrime Q),
      IsDiscreteValuationRing (Localization.AtPrime Q)

def

SelectedCompletedPrimeChainPackage

L203 ↗

EtaleFundamentalGroups.Kummer.SelectedCompletedPrimeChainPackage

Documentation

Opaque output of the first completed-prime stage. All completed tensor coordinates are deterministic; only the retained chain is stored.

Source context 7 commands

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

noncomputable section
open scoped TensorProduct
namespace EtaleFundamentalGroups.Kummer
open IsLocalRing
open Polynomial
open RingTheory.Sequence
universe u

Lean source · statement

def SelectedCompletedPrimeChainPackage
    {B E : Type u}
    [CommRing B] [IsLocalRing B]
    [CommRing E] [Algebra B E]
    (yB : B) (qGlobal p : Ideal E) : Prop

theorem

selectedExponent_completed_prime_chain_source

L233 ↗

EtaleFundamentalGroups.Kummer.selectedExponent_completed_prime_chain_source

Documentation

Produce the retained completed prime chain before any prefix contraction or normalization instances are introduced.

Source context 7 commands

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

noncomputable section
open scoped TensorProduct
namespace EtaleFundamentalGroups.Kummer
open IsLocalRing
open Polynomial
open RingTheory.Sequence
universe u

Lean source · statement

theorem selectedExponent_completed_prime_chain_source
    {B E : Type u}
    [CommRing B] [IsDomain B] [IsRegularLocalRing B]
    [CommRing E] [Algebra B E] [Module.Flat B E]
    (yB zB : B)
    (hregB : IsRegular B [yB, zB])
    (hgenB : Ideal.ofList [yB, zB] = maximalIdeal B)
    (qGlobal p : Ideal E)
    (hqGlobalPrime : qGlobal.IsPrime)
    (hqGlobalOverB : qGlobal.LiesOver (Ideal.span ({yB} : Set B)))
    (hqGlobalLe : qGlobal ≤ p)
    (hpMax : p.IsMaximal)
    (hpOverB : p.LiesOver (maximalIdeal B)) :
    SelectedCompletedPrimeChainPackage yB qGlobal p

theorem

selectedExponent_contracted_prefix_source

L280 ↗

EtaleFundamentalGroups.Kummer.selectedExponent_contracted_prefix_source

Documentation

Contract the retained completed chain and compute its exact boundary index in a fresh tensor context.

Source context 7 commands

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

noncomputable section
open scoped TensorProduct
namespace EtaleFundamentalGroups.Kummer
open IsLocalRing
open Polynomial
open RingTheory.Sequence
universe u

Lean source · full declaration

theorem selectedExponent_contracted_prefix_source
    {R R' S₀ S₁ : Type u}
    [CommRing R] [CommRing R'] [CommRing S₀] [CommRing S₁]
    [Algebra R R'] [Algebra R S₀] [Algebra R S₁]
    [Module.Finite R S₀] [Module.Flat R R']
    (y : R)
    (q₀ : Ideal S₀) [_hq₀Prime : q₀.IsPrime]
    [_hq₀Over : q₀.LiesOver (Ideal.span ({y} : Set R))]
    (g : S₀ →ₐ[R] S₁)
    (q₁ : Ideal S₁) [_hq₁Prime : q₁.IsPrime]
    (hq₁q₀ : q₁.comap g.toRingHom = q₀)
    (N Q : Ideal (R' ⊗[R] S₁))
    [_hNPrime : N.IsPrime] [_hNOver : N.LiesOver (⊥ : Ideal R')]
    [_hQPrime : Q.IsPrime]
    (hQq₁ : Q.comap
      (Algebra.TensorProduct.includeRight
        (R := R) (A := R') (B := S₁)).toRingHom = q₁)
    [hQBranch : Q.LiesOver
      (Ideal.span ({algebraMap R R' y} : Set R'))]
    (hNQ : N ≤ Q)
    [hCharZero : CharZero (R ⧸ Ideal.span ({y} : Set R))]
    {e : ℕ} (hq₀Exact : q₀.ramificationIdx R = e) :
    let f := completedFiniteModelTowerAlgHom
      (R := R) (R' := R') (S₀ := S₀) (S₁ := S₁) g
    let N₀ := N.comap f.toRingHom
    let Q₀ := Q.comap f.toRingHom
    N₀ ≤ Q₀ ∧ N₀.IsPrime ∧
      N₀.LiesOver (⊥ : Ideal R') ∧
      Q₀.IsPrime ∧ Q₀.LiesOver
        (Ideal.span ({algebraMap R R' y} : Set R')) ∧
      Q₀.comap
        (Algebra.TensorProduct.includeRight
          (R := R) (A := R') (B := S₀)).toRingHom = q₀ ∧
      Q₀.ramificationIdx R' = e := by
  classical
  dsimp only
  let : Algebra S₁ (R' ⊗[R] S₁) :=
    Algebra.TensorProduct.rightAlgebra
  have hQOver : Q.LiesOver q₁ :=
    (Ideal.liesOver_iff Q q₁).mpr hQq₁.symm
  let f := completedFiniteModelTowerAlgHom
    (R := R) (R' := R') (S₀ := S₀) (S₁ := S₁) g
  let N₀ := N.comap f.toRingHom
  let Q₀ := Q.comap f.toRingHom
  obtain
      ⟨hN₀Q₀, hN₀Prime, hN₀Over, hQ₀Prime, hQ₀Over⟩ :=
    completedFiniteModelTower_contract_primeChain
      (R := R) (R' := R') (S₀ := S₀) (S₁ := S₁)
      g q₀ q₁ hq₁q₀ N Q hNQ
  let : Algebra S₀ (R' ⊗[R] S₀) :=
    Algebra.TensorProduct.rightAlgebra
  have hQ₀Branch : Q₀.LiesOver
      (Ideal.span ({algebraMap R R' y} : Set R')) := by
    constructor
    calc
      Ideal.span ({algebraMap R R' y} : Set R') = Q.under R' :=
        hQBranch.over
      _ = Q₀.under R' := by
        ext x
        change algebraMap R' (R' ⊗[R] S₁) x ∈ Q ↔
          f (algebraMap R' (R' ⊗[R] S₀) x) ∈ Q
        rw [f.commutes x]
  have hQ₀Right :
      Q₀.comap Algebra.TensorProduct.includeRight.toRingHom = q₀ := by
    change Q₀.comap (algebraMap S₀ (R' ⊗[R] S₀)) = q₀
    exact (Q₀.over_def q₀).symm
  have hQ₀Exact : Q₀.ramificationIdx R' = e :=
    ramificationIdx_tensorProduct_span_eq_of_finite_flat_charZero_of_eq
      (R := R) (S := S₀) (R' := R')
      (y := y) (q := q₀) (Q := Q₀) hQ₀Right hq₀Exact
  exact ⟨hN₀Q₀, hN₀Prime, hN₀Over, hQ₀Prime,
    hQ₀Branch, hQ₀Right, hQ₀Exact⟩

inductive

SelectedPrefixNormalizationPackage

L356 ↗

EtaleFundamentalGroups.Kummer.SelectedPrefixNormalizationPackage

Documentation

Narrow dependent output of the retained prefix-normalization leaf. The inductive wrapper keeps the source theorem's target opaque while its sole field records the source-produced prime and boundary facts.

Source context 7 commands

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

noncomputable section
open scoped TensorProduct
namespace EtaleFundamentalGroups.Kummer
open IsLocalRing
open Polynomial
open RingTheory.Sequence
universe u

Lean source · full declaration

inductive SelectedPrefixNormalizationPackage
    {B KB M₀ : Type u}
    [CommRing B] [IsDomain B] [IsRegularLocalRing B]
    [Field KB] [Algebra B KB] [IsFractionRing B KB]
    [Field M₀] [Algebra B M₀]
    [Algebra KB M₀] [IsScalarTower B KB M₀]
    [FiniteDimensional KB M₀] [Algebra.IsSeparable KB M₀]
    [IsScalarTower B (integralClosure B M₀) M₀]
    [Module.Finite B (integralClosure B M₀)]
    [IsFractionRing (integralClosure B M₀) M₀]
    [IsIntegrallyClosed (integralClosure B M₀)]
    (yB zB : B)
    (hregB : IsRegular B [yB, zB])
    (hgenB : Ideal.ofList [yB, zB] = maximalIdeal B)
    (e : ℕ)
    (Nprefix : Ideal
      ((AdicCompletion (maximalIdeal B) B) ⊗[B]
        (integralClosure B M₀)))
    [Nprefix.IsPrime]
    [Nprefix.LiesOver
      (⊥ : Ideal (AdicCompletion (maximalIdeal B) B))] : Prop where
  | mk :
      (let C₀ := integralClosure B M₀
       let Bhat := AdicCompletion (maximalIdeal B) B
       let hgeometryHat :=
         maximalAdicCompletion_regularPair_geometry hregB hgenB
       letI : IsDomain Bhat := hgeometryHat.1
       letI : IsNoetherianRing Bhat :=
         maximalAdicCompletion_isNoetherianRing_of_regularPair hregB hgenB
       let Khat := FractionRing Bhat
       letI : Module.FaithfullyFlat B Bhat :=
         Module.FaithfullyFlat.of_flat_of_isLocalHom
       letI : FaithfulSMul B Khat := FaithfulSMul.trans B Bhat Khat
       letI : Algebra KB Khat :=
         (IsFractionRing.lift
           (A := B) (K := KB) (L := Khat)
           (FaithfulSMul.algebraMap_injective B Khat)).toAlgebra
       letI : IsScalarTower B KB Khat :=
         IsScalarTower.of_algebraMap_smul fun b x ↦ by
           rw [Algebra.smul_def, Algebra.smul_def]
           change
             (IsFractionRing.lift
               (A := B) (K := KB) (L := Khat)
               (FaithfulSMul.algebraMap_injective B Khat))
                 (algebraMap B KB b) * x =
               algebraMap B Khat b * x
           rw [IsFractionRing.lift_algebraMap]
       let mPrefix := retainedCompletedGenericTensorIdeal
         (R := B) (R' := Bhat) (S := C₀) (K := KB) (L := M₀)
         (K' := Khat) Nprefix
       letI : mPrefix.IsMaximal :=
         retainedCompletedGenericTensorIdeal_isMaximal
           (R := B) (R' := Bhat) (S := C₀) (K := KB) (L := M₀)
           (K' := Khat) Nprefix
       let OmegaPrefix := GenericTensorFieldComponent mPrefix
       let bHatOmegaPrefixAlgebra : Algebra Bhat OmegaPrefix :=
         genericTensorFieldComponentLeftScalarAlgebra (R := Bhat) mPrefix
       letI : Algebra Bhat OmegaPrefix := bHatOmegaPrefixAlgebra
       letI : SMul Bhat OmegaPrefix := bHatOmegaPrefixAlgebra.toSMul
       letI : IsScalarTower Bhat Khat OmegaPrefix :=
         IsScalarTower.of_algebraMap_eq fun _ ↦ rfl
       ∃ qhatPrefix : Ideal (integralClosure Bhat OmegaPrefix),
         ∃ hqhatPrime : qhatPrefix.IsPrime,
           letI : qhatPrefix.IsPrime := hqhatPrime
           ∃ hqhatOver : qhatPrefix.LiesOver
               (Ideal.span ({algebraMap B Bhat yB} : Set Bhat)),
             letI : qhatPrefix.LiesOver
                 (Ideal.span ({algebraMap B Bhat yB} : Set Bhat)) := hqhatOver
             qhatPrefix.ramificationIdx Bhat = e ∧
               (Localization.awayMap
                 (algebraMap Bhat (integralClosure Bhat OmegaPrefix))
                 (algebraMap B Bhat yB)).Etale) →
      SelectedPrefixNormalizationPackage yB zB hregB hgenB e Nprefix

def

selectedPrefixNormalizationRing

L431 ↗

EtaleFundamentalGroups.Kummer.selectedPrefixNormalizationRing

Documentation

Opaque name for the literal retained-prefix normalization ring.

Source context 7 commands

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

noncomputable section
open scoped TensorProduct
namespace EtaleFundamentalGroups.Kummer
open IsLocalRing
open Polynomial
open RingTheory.Sequence
universe u

Lean source · statement

def selectedPrefixNormalizationRing
    {B KB M₀ : Type u}
    [hBComm : CommRing B] [hBDomain : IsDomain B]
    [hBRegular : IsRegularLocalRing B]
    [hKBField : Field KB] [hBKB : Algebra B KB]
    [hKBFrac : IsFractionRing B KB]
    [hM₀Field : Field M₀] [hBM₀ : Algebra B M₀]
    [hKBM₀ : Algebra KB M₀] [hBKBM₀ : IsScalarTower B KB M₀]
    [hBC₀M₀ : IsScalarTower B (integralClosure B M₀) M₀]
    [hC₀Finite : Module.Finite B (integralClosure B M₀)]
    [hC₀Frac : IsFractionRing (integralClosure B M₀) M₀]
    (yB zB : B)
    (hregB : IsRegular B [yB, zB])
    (hgenB : Ideal.ofList [yB, zB] = maximalIdeal B)
    (Nprefix : Ideal
      ((AdicCompletion (maximalIdeal B) B) ⊗[B]
        (integralClosure B M₀)))
    [hNprefixPrime : Nprefix.IsPrime]
    [hNprefixOver : Nprefix.LiesOver
      (⊥ : Ideal (AdicCompletion (maximalIdeal B) B))] : Type u

structure

SelectedAlgebraOwner

L489 ↗

EtaleFundamentalGroups.Kummer.SelectedAlgebraOwner

Documentation

Small owner-explicit carrier for the normalization prime produced by the fresh prefix leaf. It is independent of the finite-model construction.

Source context 7 commands

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

noncomputable section
open scoped TensorProduct
namespace EtaleFundamentalGroups.Kummer
open IsLocalRing
open Polynomial
open RingTheory.Sequence
universe u

Lean source · full declaration

structure SelectedAlgebraOwner
    (R Ω : Type u) [CommRing R] where
  commRingΩ : CommRing Ω
  algebra :
    letI : CommRing Ω := commRingΩ
    Algebra R Ω

def

selectedPrefixNormalizationOwner

L498 ↗

EtaleFundamentalGroups.Kummer.selectedPrefixNormalizationOwner

Documentation

The canonical algebra owner for the opaque retained-prefix normalization ring.

Source context 7 commands

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

noncomputable section
open scoped TensorProduct
namespace EtaleFundamentalGroups.Kummer
open IsLocalRing
open Polynomial
open RingTheory.Sequence
universe u

Lean source · statement

def selectedPrefixNormalizationOwner
    {B KB M₀ : Type u}
    [hBComm : CommRing B] [hBDomain : IsDomain B]
    [hBRegular : IsRegularLocalRing B]
    [hKBField : Field KB] [hBKB : Algebra B KB]
    [hKBFrac : IsFractionRing B KB]
    [hM₀Field : Field M₀] [hBM₀ : Algebra B M₀]
    [hKBM₀ : Algebra KB M₀] [hBKBM₀ : IsScalarTower B KB M₀]
    [hBC₀M₀ : IsScalarTower B (integralClosure B M₀) M₀]
    [hC₀Finite : Module.Finite B (integralClosure B M₀)]
    [hC₀Frac : IsFractionRing (integralClosure B M₀) M₀]
    (yB zB : B)
    (hregB : IsRegular B [yB, zB])
    (hgenB : Ideal.ofList [yB, zB] = maximalIdeal B)
    (Nprefix : Ideal
      ((AdicCompletion (maximalIdeal B) B) ⊗[B]
        (integralClosure B M₀)))
    [hNprefixPrime : Nprefix.IsPrime]
    [hNprefixOver : Nprefix.LiesOver
      (⊥ : Ideal (AdicCompletion (maximalIdeal B) B))] :
    SelectedAlgebraOwner
      (AdicCompletion (maximalIdeal B) B)
      (selectedPrefixNormalizationRing
        (hBComm := hBComm) (hBDomain := hBDomain)
        (hBRegular := hBRegular) (hKBField := hKBField)
        (hBKB := hBKB) (hKBFrac := hKBFrac)
        (hM₀Field := hM₀Field) (hBM₀ := hBM₀)
        (hKBM₀ := hKBM₀) (hBKBM₀ := hBKBM₀)
        (hBC₀M₀ := hBC₀M₀) (hC₀Finite := hC₀Finite)
        (hC₀Frac := hC₀Frac)
        (hNprefixPrime := hNprefixPrime) (hNprefixOver := hNprefixOver)
        yB zB hregB hgenB Nprefix)

inductive

SelectedPrefixNormalizationOutput

L570 ↗

EtaleFundamentalGroups.Kummer.SelectedPrefixNormalizationOutput

Source context 7 commands

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

noncomputable section
open scoped TensorProduct
namespace EtaleFundamentalGroups.Kummer
open IsLocalRing
open Polynomial
open RingTheory.Sequence
universe u

Lean source · full declaration

inductive SelectedPrefixNormalizationOutput
    {R Ω : Type u} [CommRing R]
    (a : SelectedAlgebraOwner R Ω) (y : R) (e : ℕ) : Prop where
  | mk :
      (letI : CommRing Ω := a.commRingΩ
       letI : Algebra R Ω := a.algebra
       ∃ q : Ideal Ω,
         ∃ hqPrime : q.IsPrime,
           letI : q.IsPrime := hqPrime
           ∃ hqOver : q.LiesOver (Ideal.span ({y} : Set R)),
             letI : q.LiesOver (Ideal.span ({y} : Set R)) := hqOver
             q.ramificationIdx R = e ∧
               (Localization.awayMap (algebraMap R Ω) y).Etale) →
      SelectedPrefixNormalizationOutput a y e

theorem

selectedExponent_prefix_normalization_source

L587 ↗

EtaleFundamentalGroups.Kummer.selectedExponent_prefix_normalization_source

Documentation

Lift the contracted retained prime to the selected normalization and transport the boundary-Away statement in a fresh normalization context.

Source context 7 commands

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

noncomputable section
open scoped TensorProduct
namespace EtaleFundamentalGroups.Kummer
open IsLocalRing
open Polynomial
open RingTheory.Sequence
universe u

Lean source · statement

theorem selectedExponent_prefix_normalization_source
    {B KB M₀ : Type u}
    [hBComm : CommRing B] [hBDomain : IsDomain B]
    [hBRegular : IsRegularLocalRing B]
    [hKBField : Field KB] [hBKB : Algebra B KB]
    [hKBFrac : IsFractionRing B KB]
    [hM₀Field : Field M₀] [hBM₀ : Algebra B M₀]
    [hKBM₀ : Algebra KB M₀] [hBKBM₀ : IsScalarTower B KB M₀]
    [hFinKBM₀ : FiniteDimensional KB M₀]
    [hSepKBM₀ : Algebra.IsSeparable KB M₀]
    [hBC₀M₀ : IsScalarTower B (integralClosure B M₀) M₀]
    [hC₀Finite : Module.Finite B (integralClosure B M₀)]
    [hC₀Frac : IsFractionRing (integralClosure B M₀) M₀]
    (yB zB : B)
    (hregB : IsRegular B [yB, zB])
    (hgenB : Ideal.ofList [yB, zB] = maximalIdeal B)
    (hdimB : ringKrullDim B = ((2 : ℕ∞) : WithBot ℕ∞))
    (e : ℕ)
    (Nprefix Qprefix : Ideal
      ((AdicCompletion (maximalIdeal B) B) ⊗[B]
        (integralClosure B M₀)))
    [_hNprefixPrime : Nprefix.IsPrime]
    [_hNprefixOver : Nprefix.LiesOver
      (⊥ : Ideal (AdicCompletion (maximalIdeal B) B))]
    [_hQprefixPrime : Qprefix.IsPrime]
    [hQprefixBranch : Qprefix.LiesOver
      (Ideal.span
        ({algebraMap B (AdicCompletion (maximalIdeal B) B) yB} :
          Set (AdicCompletion (maximalIdeal B) B)))]
    (hNprefixQprefix : Nprefix ≤ Qprefix)
    [_hWprefixDomain : IsDomain (Localization.AtPrime Qprefix)]
    [_hWprefixDVR : IsDiscreteValuationRing (Localization.AtPrime Qprefix)]
    (hQprefixExact :
      Qprefix.ramificationIdx (AdicCompletion (maximalIdeal B) B) = e)
    (hAwayPrefix :
      (Localization.awayMap
        (algebraMap B (integralClosure B M₀)) yB).Etale) :
    SelectedPrefixNormalizationOutput
      (R := AdicCompletion (maximalIdeal B) B)
      (Ω := selectedPrefixNormalizationRing
        (hBComm := hBComm) (hBDomain := hBDomain)
        (hBRegular := hBRegular) (hKBField := hKBField)
        (hBKB := hBKB) (hKBFrac := hKBFrac)
        (hM₀Field := hM₀Field) (hBM₀ := hBM₀)
        (hKBM₀ := hKBM₀) (hBKBM₀ := hBKBM₀)
        (hBC₀M₀ := hBC₀M₀) (hC₀Finite := hC₀Finite)
        (hC₀Frac := hC₀Frac)
        (hNprefixPrime := _hNprefixPrime)
        (hNprefixOver := _hNprefixOver)
        yB zB hregB hgenB Nprefix)
      (selectedPrefixNormalizationOwner
        (hBComm := hBComm) (hBDomain := hBDomain)
        (hBRegular := hBRegular) (hKBField := hKBField)
        (hBKB := hBKB) (hKBFrac := hKBFrac)
        (hM₀Field := hM₀Field) (hBM₀ := hBM₀)
        (hKBM₀ := hKBM₀) (hBKBM₀ := hBKBM₀)
        (hBC₀M₀ := hBC₀M₀) (hC₀Finite := hC₀Finite)
        (hC₀Frac := hC₀Frac)
        (hNprefixPrime := _hNprefixPrime)
        (hNprefixOver := _hNprefixOver)
        yB zB hregB hgenB Nprefix)
      (algebraMap B (AdicCompletion (maximalIdeal B) B) yB) e

def

SelectedExponentPrefixPackageBody

L754 ↗

EtaleFundamentalGroups.Kummer.SelectedExponentPrefixPackageBody

Documentation

The narrow noncanonical output of the completed-prefix construction. All tensor products, contractions, and component fields are deterministic from Nfinal; only the two retained primes and their mathematical facts are stored.

Source context 7 commands

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

noncomputable section
open scoped TensorProduct
namespace EtaleFundamentalGroups.Kummer
open IsLocalRing
open Polynomial
open RingTheory.Sequence
universe u

Lean source · statement

def SelectedExponentPrefixPackageBody
    {B D KB M₀ M : Type u}
    [CommRing B] [IsDomain B] [IsRegularLocalRing B]
    [CommRing D] [IsDomain D] [Algebra B D]
    [Field KB] [Algebra B KB] [IsFractionRing B KB]
    [Field M₀] [Algebra B M₀] [Algebra KB M₀]
    [IsScalarTower B KB M₀]
    [Field M] [Algebra D M] [Algebra B M] [IsScalarTower B D M]
    [Algebra KB M] [IsScalarTower B KB M]
    [IsScalarTower B (integralClosure B M₀) M₀]
    [Module.Finite B (integralClosure B M₀)]
    [IsFractionRing (integralClosure B M₀) M₀]
    [Algebra B (integralClosure D M)]
    (yB zB : B)
    (hregB : IsRegular B [yB, zB])
    (hgenB : Ideal.ofList [yB, zB] = maximalIdeal B)
    (N : ℕ)
    (g : integralClosure B M₀ →ₐ[B] integralClosure D M)
    (p : Ideal (integralClosure D M)) : Prop

inductive

SelectedExponentPrefixPackage

L860 ↗

EtaleFundamentalGroups.Kummer.SelectedExponentPrefixPackage

Source context 7 commands

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

noncomputable section
open scoped TensorProduct
namespace EtaleFundamentalGroups.Kummer
open IsLocalRing
open Polynomial
open RingTheory.Sequence
universe u

Lean source · full declaration

inductive SelectedExponentPrefixPackage
    {B D KB M₀ M : Type u}
    [CommRing B] [IsDomain B] [IsRegularLocalRing B]
    [CommRing D] [IsDomain D] [Algebra B D]
    [Field KB] [Algebra B KB] [IsFractionRing B KB]
    [Field M₀] [Algebra B M₀] [Algebra KB M₀]
    [IsScalarTower B KB M₀]
    [Field M] [Algebra D M] [Algebra B M] [IsScalarTower B D M]
    [Algebra KB M] [IsScalarTower B KB M]
    [IsScalarTower B (integralClosure B M₀) M₀]
    [Module.Finite B (integralClosure B M₀)]
    [IsFractionRing (integralClosure B M₀) M₀]
    [Algebra B (integralClosure D M)]
    (yB zB : B)
    (hregB : IsRegular B [yB, zB])
    (hgenB : Ideal.ofList [yB, zB] = maximalIdeal B)
    (N : ℕ)
    (g : integralClosure B M₀ →ₐ[B] integralClosure D M)
    (p : Ideal (integralClosure D M)) : Prop where
  | mk :
      SelectedExponentPrefixPackageBody
        (B := B) (D := D) (KB := KB) (M₀ := M₀) (M := M)
        yB zB hregB hgenB N g p →
      SelectedExponentPrefixPackage yB zB hregB hgenB N g p

theorem

selectedExponent_completion_prefix

L888 ↗

EtaleFundamentalGroups.Kummer.selectedExponent_completion_prefix

Documentation

Complete the selected-branch argument from the explicit finite models and the retained source primes. The global-source construction owns the models; this core starts with a fresh instance context.

Source context 7 commands

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

noncomputable section
open scoped TensorProduct
namespace EtaleFundamentalGroups.Kummer
open IsLocalRing
open Polynomial
open RingTheory.Sequence
universe u

Lean source · statement

theorem selectedExponent_completion_prefix
    {B D KB M₀ M : Type u}
    [CommRing B] [IsDomain B] [IsRegularLocalRing B]
    [CommRing D] [IsDomain D] [Algebra B D]
    [Field KB] [Algebra B KB] [IsFractionRing B KB]
    [Field M₀] [Algebra B M₀] [Algebra KB M₀]
    [IsScalarTower B KB M₀] [FiniteDimensional KB M₀]
    [Algebra.IsSeparable KB M₀]
    [Field M] [Algebra D M] [Algebra B M] [IsScalarTower B D M]
    [Algebra KB M] [IsScalarTower B KB M]
    [IsScalarTower B (integralClosure B M₀) M₀]
    [Module.Finite B (integralClosure B M₀)]
    [FaithfulSMul B (integralClosure B M₀)]
    [IsFractionRing (integralClosure B M₀) M₀]
    [IsIntegrallyClosed (integralClosure B M₀)]
    [Algebra B (integralClosure D M)]
    [Module.Flat B (integralClosure D M)]
    (yB zB : B) (N : ℕ)
    (hregB : IsRegular B [yB, zB])
    (hgenB : Ideal.ofList [yB, zB] = maximalIdeal B)
    (hdimB : ringKrullDim B = ((2 : ℕ∞) : WithBot ℕ∞))
    (hyBPrime : Prime yB)
    (hCharB : CharZero (B ⧸ Ideal.span ({yB} : Set B)))
    (g : integralClosure B M₀ →ₐ[B] integralClosure D M)
    (qGlobal p : Ideal (integralClosure D M))
    (hqGlobalPrime : qGlobal.IsPrime)
    (hqGlobalOverB : qGlobal.LiesOver (Ideal.span ({yB} : Set B)))
    (hqGlobalLe : qGlobal ≤ p)
    (hpMax : p.IsMaximal)
    (hpOverB : p.LiesOver (maximalIdeal B))
    (qPrefix : Ideal (integralClosure B M₀))
    [hqPrefixPrime : qPrefix.IsPrime]
    [hqPrefixOverB : qPrefix.LiesOver (Ideal.span ({yB} : Set B))]
    (hqGlobalComap : qGlobal.comap g.toRingHom = qPrefix)
    (hqPrefixExact : qPrefix.ramificationIdx B = N)
    (hAwayPrefix :
      (Localization.awayMap
        (algebraMap B (integralClosure B M₀)) yB).Etale) :
    SelectedExponentPrefixPackage
      (B := B) (D := D) (KB := KB) (M₀ := M₀) (M := M)
      yB zB hregB hgenB N g p

theorem

prime_eq_maximalIdeal_of_liesOver_of_finite

L1085 ↗

EtaleFundamentalGroups.Kummer.prime_eq_maximalIdeal_of_liesOver_of_finite

Documentation

In a finite algebra over a local ring, a prime above the closed point is the unique maximal ideal of the local target.

Source context 7 commands

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

noncomputable section
open scoped TensorProduct
namespace EtaleFundamentalGroups.Kummer
open IsLocalRing
open Polynomial
open RingTheory.Sequence
universe u

Lean source · statement

theorem prime_eq_maximalIdeal_of_liesOver_of_finite
    {R S : Type u} [CommRing R] [CommRing S]
    [IsLocalRing R] [IsLocalRing S] [Algebra R S] [Module.Finite R S]
    (Q : Ideal S) (hQPrime : Q.IsPrime)
    (hQOver : Q.LiesOver (maximalIdeal R)) :
    Q = maximalIdeal S

theorem

integralClosure_faithfulSMul_of_fractionField

L1104 ↗

EtaleFundamentalGroups.Kummer.integralClosure_faithfulSMul_of_fractionField

Documentation

The integral closure inside a field extension is faithful over the base domain through the chosen fraction field.

Source context 7 commands

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

noncomputable section
open scoped TensorProduct
namespace EtaleFundamentalGroups.Kummer
open IsLocalRing
open Polynomial
open RingTheory.Sequence
universe u

Lean source · statement

theorem integralClosure_faithfulSMul_of_fractionField
    {R K L : Type u}
    [CommRing R] [IsDomain R]
    [Field K] [Algebra R K] [IsFractionRing R K]
    [Field L] [Algebra R L] [Algebra K L] [IsScalarTower R K L] :
    FaithfulSMul R (integralClosure R L)

theorem

isScalarTower_of_algebra_tower_square

L1126 ↗

EtaleFundamentalGroups.Kummer.isScalarTower_of_algebra_tower_square

Documentation

Compatibility around a square of algebra towers.

Source context 7 commands

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

noncomputable section
open scoped TensorProduct
namespace EtaleFundamentalGroups.Kummer
open IsLocalRing
open Polynomial
open RingTheory.Sequence
universe u

Lean source · statement

theorem isScalarTower_of_algebra_tower_square
    {R S T U : Type u}
    [CommSemiring R] [CommSemiring S] [CommSemiring T] [Semiring U]
    [Algebra R S] [Algebra R T] [Algebra S T]
    [Algebra R U] [Algebra S U] [Algebra T U]
    [IsScalarTower R S T] [IsScalarTower R T U]
    [IsScalarTower S T U] :
    IsScalarTower R S U

theorem

tensorPushoutEquiv_base_isScalarTower

L1147 ↗

EtaleFundamentalGroups.Kummer.tensorPushoutEquiv_base_isScalarTower

Documentation

The algebra structures transported through the completed root pushout form the expected base tower.

Source context 7 commands

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

noncomputable section
open scoped TensorProduct
namespace EtaleFundamentalGroups.Kummer
open IsLocalRing
open Polynomial
open RingTheory.Sequence
universe u

Lean source · full declaration

theorem tensorPushoutEquiv_base_isScalarTower
    {B D Bhat Broot : Type u}
    [CommRing B] [CommRing D] [CommRing Bhat] [CommRing Broot]
    [Algebra B D] [Algebra B Bhat] [Algebra Bhat Broot]
    (e : (Bhat ⊗[B] D) ≃ₐ[Bhat] Broot) :
    let dBrootAlgebra : Algebra D Broot :=
      (e.toRingHom.comp
        Algebra.TensorProduct.includeRight.toRingHom).toAlgebra
    let bBrootAlgebra : Algebra B Broot :=
      ((algebraMap Bhat Broot).comp (algebraMap B Bhat)).toAlgebra
    @IsScalarTower B D Broot
      (inferInstance : Algebra B D).toSMul
      dBrootAlgebra.toSMul bBrootAlgebra.toSMul := by
  let dBrootAlgebra : Algebra D Broot :=
    (e.toRingHom.comp
      Algebra.TensorProduct.includeRight.toRingHom).toAlgebra
  let bBrootAlgebra : Algebra B Broot :=
    ((algebraMap Bhat Broot).comp (algebraMap B Bhat)).toAlgebra
  apply IsScalarTower.of_algebraMap_eq
  intro x
  calc
    algebraMap B Broot x =
        e (algebraMap Bhat (Bhat ⊗[B] D) (algebraMap B Bhat x)) :=
      (e.commutes (algebraMap B Bhat x)).symm
    _ = e (Algebra.TensorProduct.includeRight (algebraMap B D x)) := by
      congr 1
      exact DFunLike.congr_fun
        Algebra.TensorProduct.includeLeftRingHom_comp_algebraMap x
    _ = algebraMap D Broot (algebraMap B D x) := rfl

theorem

exists_retainedCompletedComponentToChosenLocalFractionAlgHom

L1180 ↗

EtaleFundamentalGroups.Kummer.exists_retainedCompletedComponentToChosenLocalFractionAlgHom

Documentation

Package the retained final component map uniformly in the later domain instance. Its construction is checked outside the selected-branch context.

Source context 7 commands

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

noncomputable section
open scoped TensorProduct
namespace EtaleFundamentalGroups.Kummer
open IsLocalRing
open Polynomial
open RingTheory.Sequence
universe u

Lean source · full declaration

theorem exists_retainedCompletedComponentToChosenLocalFractionAlgHom
    {R R' S K L K' : Type u}
    [CommRing R] [IsDomain R]
    [CommRing R'] [IsDomain R'] [Algebra R R']
    [CommRing S] [IsDomain S] [Algebra R S] [Module.Finite R S]
    [Field K] [Algebra R K] [IsFractionRing R K]
    [Field K'] [Algebra R' K'] [IsFractionRing R' K']
    [Field L] [Algebra S L] [IsFractionRing S L]
    [Algebra R L] [IsScalarTower R S L]
    [Algebra K L] [IsScalarTower R K L]
    [Algebra R K'] [IsScalarTower R R' K']
    [Algebra K K'] [IsScalarTower R K K']
    (N P : Ideal (R' ⊗[R] S)) [N.IsPrime]
    [N.LiesOver (⊥ : Ideal R')]
    (hNP : N ≤ P) (hPMax : P.IsMaximal) :
    let m := retainedCompletedGenericTensorIdeal
      (R := R) (R' := R') (S := S) (K := K) (L := L)
      (K' := K') N
    letI : m.IsMaximal := retainedCompletedGenericTensorIdeal_isMaximal
      (R := R) (R' := R') (S := S) (K := K) (L := L)
      (K' := K') N
    let Omega := GenericTensorFieldComponent m
    letI : Algebra R' Omega :=
      genericTensorFieldComponentLeftScalarAlgebra (R := R') m
    ∃ _f : ∀ [IsDomain (Localization.AtPrime P)],
        Omega →ₐ[R'] FractionRing (Localization.AtPrime P),
      True := by
  classical
  dsimp only
  let m := retainedCompletedGenericTensorIdeal
    (R := R) (R' := R') (S := S) (K := K) (L := L)
    (K' := K') N
  let : m.IsMaximal := retainedCompletedGenericTensorIdeal_isMaximal
    (R := R) (R' := R') (S := S) (K := K) (L := L)
    (K' := K') N
  let Omega := GenericTensorFieldComponent m
  let r'OmegaAlgebra : Algebra R' Omega :=
    genericTensorFieldComponentLeftScalarAlgebra (R := R') m
  let : P.IsPrime := hPMax.isPrime
  refine ⟨?_, True.intro⟩
  intro _hDomain
  exact (retainedCompletedComponentToChosenLocalFractionAlgEquiv
    (R := R) (R' := R') (S := S) (K := K) (L := L)
    (K' := K') N P hNP).toAlgHom

theorem

selectedExponent_finish_local_factor

L1228 ↗

EtaleFundamentalGroups.Kummer.selectedExponent_finish_local_factor

Documentation

Close the argument once the finite-etale local factor and its unique closed prime have been constructed.

Source context 7 commands

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

noncomputable section
open scoped TensorProduct
namespace EtaleFundamentalGroups.Kummer
open IsLocalRing
open Polynomial
open RingTheory.Sequence
universe u

Lean source · full declaration

theorem selectedExponent_finish_local_factor
    {A Omega OmegaFinal : Type u}
    [CommRing A] [IsDomain A] [IsRegularLocalRing A]
    [IsAdicComplete (maximalIdeal A) A]
    [Field Omega] [Algebra A Omega] [Algebra (FractionRing A) Omega]
    [IsScalarTower A (FractionRing A) Omega]
    [FiniteDimensional (FractionRing A) Omega]
    [IsGalois (FractionRing A) Omega]
    [Field OmegaFinal] [Algebra A OmegaFinal]
    [Algebra (FractionRing A) OmegaFinal]
    [IsScalarTower A (FractionRing A) OmegaFinal]
    (y z : A)
    (hreg : IsRegular A [y, z])
    (hgen : Ideal.ofList [y, z] = maximalIdeal A)
    (N : ℕ) (hN : 0 < N)
    (hChar : CharZero (A ⧸ Ideal.span ({y} : Set A)))
    (fTower : Omega →ₐ[FractionRing A] OmegaFinal)
    (q : Ideal (integralClosure A Omega))
    (hqPrime : q.IsPrime)
    (hqOver : q.LiesOver (Ideal.span ({y} : Set A)))
    (hqExact : q.ramificationIdx A = N)
    (hAway :
      (Localization.awayMap
        (algebraMap A (integralClosure A Omega)) y).Etale) :
    let n : Fin 1 → ℕ := fun _ ↦ N
    let a : Fin 1 → A := fun _ ↦ y
    let Broot := iteratedRadical A 1 n a
    let hymax : y ∈ maximalIdeal A := by
      rw [← hgen]
      exact Ideal.subset_span (by simp)
    let ha : ∀ i, a i ∈ maximalIdeal A := fun _ ↦ hymax
    letI : IsLocalRing Broot :=
      isLocalRing_iteratedRadical n a (fun _ ↦ hN) ha
    ∀ {Dlocal : Type u} [CommRing Dlocal] [IsLocalRing Dlocal]
      [Algebra A Dlocal] [Algebra Broot Dlocal]
      [IsScalarTower A Broot Dlocal]
      [Module.Finite Broot Dlocal] [Algebra.Etale Broot Dlocal]
      [IsLocalHom (algebraMap Broot Dlocal)] [FaithfulSMul A Dlocal],
      ∀ (qD : Ideal Dlocal) [qD.IsPrime]
        [qD.LiesOver (maximalIdeal Broot)],
        (∀ Q : Ideal Dlocal, Q.IsPrime →
          Q.LiesOver (maximalIdeal Broot) → Q = qD) →
        (∀ [IsDomain Dlocal],
          OmegaFinal →ₐ[A] FractionRing Dlocal) →
        IsUnit (N : A) := by
  classical
  dsimp only
  intro Dlocal _ _ _ _ _ _ _ _ _ qD hqDPrime hqDOver
    huniqueD fFinal
  let n : Fin 1 → ℕ := fun _ ↦ N
  let a : Fin 1 → A := fun _ ↦ y
  let Broot := iteratedRadical A 1 n a
  have hymax : y ∈ maximalIdeal A := by
    rw [← hgen]
    exact Ideal.subset_span (by simp)
  have ha : ∀ i, a i ∈ maximalIdeal A := fun _ ↦ hymax
  let : IsLocalRing Broot :=
    isLocalRing_iteratedRadical n a (fun _ ↦ hN) ha
  have hdimAux :=
    ringKrullDim_add_length_eq_ringKrullDim_of_isRegular [y, z] hreg
  rw [hgen] at hdimAux
  let : Field (A ⧸ maximalIdeal A) :=
    Ideal.Quotient.field (maximalIdeal A)
  have hfieldDim : ringKrullDim (A ⧸ maximalIdeal A) = 0 :=
    ringKrullDim_eq_zero_of_field _
  rw [hfieldDim, zero_add] at hdimAux
  have hdim : ringKrullDim A = ((2 : ℕ∞) : WithBot ℕ∞) := by
    norm_num [List.length_cons, List.length_nil] at hdimAux
    exact hdimAux.symm
  let : Module.Finite A (integralClosure A Omega) :=
    SpecialLocalPurity.integralClosure_finite_of_isRegularLocalRing_dimension_two
      (K := FractionRing A) hdim
  obtain ⟨eResidueTensor, hTerminal⟩ :=
    exists_completeRegularPairChosenFactor_oneRoot_exponent_isUnit_of_exactNormalizationPrime
      (A := A) y z hreg hgen N hN hChar
      (D := Dlocal) qD huniqueD
  let l := ResidueField Dlocal
  let : Module.Finite A Broot :=
    finite_iteratedRadical n a (fun _ ↦ hN)
  let : Module.FaithfullyFlat A Broot :=
    faithfullyFlat_iteratedRadical n a (fun _ ↦ hN)
  let : Algebra.IsIntegral A Broot :=
    Algebra.IsIntegral.of_finite A Broot
  let : IsLocalHom (algebraMap A Broot) :=
    Algebra.IsIntegral.isLocalHom A Broot
  let : IsLocalHom (algebraMap A Dlocal) := by
    rw [IsScalarTower.algebraMap_eq A Broot Dlocal]
    infer_instance
  let k := ResidueField A
  let kRoot := ResidueField Broot
  let eResidue : k ≃ₐ[k] kRoot :=
    AlgEquiv.ofBijective (Algebra.ofId k kRoot)
      (residueFieldMap_bijective_iteratedRadical
        n a (fun _ ↦ hN) ha)
  let : Module.Finite k kRoot :=
    Module.Finite.of_surjective eResidue.toLinearMap eResidue.surjective
  let : Module.Finite k l := Module.Finite.trans kRoot l
  let : Algebra.IsSeparable k kRoot :=
    AlgEquiv.Algebra.isSeparable eResidue
  let : Algebra.IsSeparable k l :=
    Algebra.IsSeparable.trans k kRoot l
  let C₁ := FiniteEtaleResidueLift A l
  let : IsLocalRing C₁ := isLocalRing_finiteEtaleResidueLift A l
  let : Module.Finite A C₁ := moduleFinite_finiteEtaleResidueLift A l
  let : FaithfulSMul A C₁ := faithfulSMul_finiteEtaleResidueLift A l
  let : Algebra.Etale A C₁ := etale_finiteEtaleResidueLift A l
  let : Algebra.IsIntegral A C₁ := Algebra.IsIntegral.of_finite A C₁
  let : IsLocalHom (algebraMap A C₁) :=
    Algebra.IsIntegral.isLocalHom A C₁
  let : Module.FaithfullyFlat A C₁ :=
    Module.FaithfullyFlat.of_flat_of_isLocalHom
  let : IsDomain C₁ :=
    finiteEtaleResidueLiftIsDomain_of_regularSystem hreg hgen
  let : Algebra C₁ Dlocal :=
    tensorChosenFactorRightAlgebra eResidueTensor
  let : IsScalarTower A C₁ Dlocal := by
    apply IsScalarTower.of_algebraMap_eq
    intro x
    calc
      algebraMap A Dlocal x =
          algebraMap Broot Dlocal (algebraMap A Broot x) :=
        IsScalarTower.algebraMap_apply A Broot Dlocal x
      _ = eResidueTensor
          (algebraMap Broot (Broot ⊗[A] C₁)
            (algebraMap A Broot x)) :=
        (eResidueTensor.commutes (algebraMap A Broot x)).symm
      _ = eResidueTensor
          (Algebra.TensorProduct.includeRight (algebraMap A C₁ x)) := by
        congr 1
        exact DFunLike.congr_fun
          Algebra.TensorProduct.includeLeftRingHom_comp_algebraMap x
      _ = algebraMap C₁ Dlocal (algebraMap A C₁ x) := rfl
  let yC := algebraMap A C₁ y
  let Rn := AdjoinRoot (X ^ N - Polynomial.C yC)
  let eRoot : Rn ≃ₐ[C₁] Dlocal :=
    oneRootChosenFactorAlgEquiv N y eResidueTensor
  let : IsDomain Rn := by
    simpa only [Rn, C₁, yC] using
      (finiteEtaleResidueLift_pair_adjoinRoot_isDomain_of_regularPair
        (l := l) y z hreg hgen N hN)
  let : IsDomain Dlocal := eRoot.symm.toMulEquiv.isDomain Rn
  let : Module.Free C₁ Rn :=
    (monic_X_pow_sub_C yC hN.ne').free_adjoinRoot
  let : FaithfulSMul C₁ Rn := Module.FaithfullyFlat.faithfulSMul
  let Pfield := FractionRing Dlocal
  let : IsScalarTower A Dlocal Pfield :=
    IsScalarTower.of_algebraMap_eq' rfl
  let : FaithfulSMul A Pfield := FaithfulSMul.trans A Dlocal Pfield
  let : Algebra (FractionRing A) Pfield :=
    FractionRing.liftAlgebra A Pfield
  let : IsScalarTower A (FractionRing A) Pfield :=
    FractionRing.isScalarTower_liftAlgebra A Pfield
  let eFinalA : OmegaFinal →ₐ[A] Pfield := fFinal
  let eFinalF : OmegaFinal →ₐ[FractionRing A] Pfield :=
    fractionFieldBaseAlgHomOfRestrictScalars
      (A := A) (F := FractionRing A) eFinalA
  let fPrefix : Omega →ₐ[FractionRing A] Pfield :=
    eFinalF.comp fTower
  let cPAlgebra : Algebra C₁ Pfield :=
    fractionRingTargetBaseAlgebraOfAlgEquiv eRoot
  let : SMul C₁ Pfield := cPAlgebra.toSMul
  let : @FaithfulSMul C₁ Pfield cPAlgebra.toSMul := by
    apply (@faithfulSMul_iff_algebraMap_injective
      C₁ Pfield _ _ cPAlgebra).mpr
    have hCDlocal : Function.Injective (algebraMap C₁ Dlocal) := by
      intro x x' hxx'
      apply FaithfulSMul.algebraMap_injective C₁ Rn
      apply eRoot.injective
      simpa only [eRoot.commutes] using hxx'
    change Function.Injective
      ((algebraMap Dlocal Pfield).comp (algebraMap C₁ Dlocal))
    exact (IsFractionRing.injective Dlocal Pfield).comp hCDlocal
  let : @IsScalarTower C₁ Dlocal Pfield
      (inferInstance : Algebra C₁ Dlocal).toSMul
      (inferInstance : Algebra Dlocal Pfield).toSMul
      cPAlgebra.toSMul := IsScalarTower.of_algebraMap_eq' rfl
  let : @IsScalarTower A C₁ Pfield
      (inferInstance : Algebra A C₁).toSMul
      cPAlgebra.toSMul
      (inferInstance : Algebra A Pfield).toSMul :=
    isScalarTower_of_algebra_tower_square
      (R := A) (S := C₁) (T := Dlocal) (U := Pfield)
  let KC := FractionRing C₁
  let kcPAlgebra : Algebra KC Pfield := fractionRingAlgebraOfAlgEquiv eRoot
  let : SMul KC Pfield := kcPAlgebra.toSMul
  let : @IsScalarTower C₁ KC Pfield
      (inferInstance : Algebra C₁ KC).toSMul
      kcPAlgebra.toSMul cPAlgebra.toSMul :=
    FractionRing.isScalarTower_liftAlgebra C₁ Pfield
  let aKCAlgebra : Algebra A KC :=
    ((algebraMap C₁ KC).comp (algebraMap A C₁)).toAlgebra
  let : SMul A KC := aKCAlgebra.toSMul
  let : @IsScalarTower A C₁ KC
      (inferInstance : Algebra A C₁).toSMul
      (inferInstance : Algebra C₁ KC).toSMul
      aKCAlgebra.toSMul := IsScalarTower.of_algebraMap_eq' rfl
  let : @FaithfulSMul A KC aKCAlgebra.toSMul := by
    apply (@faithfulSMul_iff_algebraMap_injective A KC _ _ aKCAlgebra).mpr
    change Function.Injective
      ((algebraMap C₁ KC).comp (algebraMap A C₁))
    exact (IsFractionRing.injective C₁ KC).comp
      (FaithfulSMul.algebraMap_injective A C₁)
  let : Algebra (FractionRing A) KC := FractionRing.liftAlgebra A KC
  let : IsScalarTower A (FractionRing A) KC :=
    FractionRing.isScalarTower_liftAlgebra A KC
  exact prefixEmbedding_exactPrimeBoundaryAway_terminal_isUnit
    (A := A) (C := C₁) (F := FractionRing A) (KC := KC)
    (M := Omega) (P := Pfield)
    y z hreg hgen hdim N fPrefix q hqPrime hqOver hqExact hAway hTerminal

theorem

selectedExponent_finish_after_final_root

L1442 ↗

EtaleFundamentalGroups.Kummer.selectedExponent_finish_after_final_root

Documentation

Finish the selected-exponent argument from the completed one-root factor. The retained construction supplies only the final component map; all local factor and residue-lift instances are confined to this declaration.

Source context 7 commands

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

noncomputable section
open scoped TensorProduct
namespace EtaleFundamentalGroups.Kummer
open IsLocalRing
open Polynomial
open RingTheory.Sequence
universe u

Lean source · full declaration

theorem selectedExponent_finish_after_final_root
    {A Omega OmegaFinal : Type u}
    [CommRing A] [IsDomain A] [IsRegularLocalRing A]
    [IsAdicComplete (maximalIdeal A) A]
    [Field Omega] [Algebra A Omega] [Algebra (FractionRing A) Omega]
    [IsScalarTower A (FractionRing A) Omega]
    [FiniteDimensional (FractionRing A) Omega]
    [IsGalois (FractionRing A) Omega]
    [Field OmegaFinal] [Algebra A OmegaFinal]
    [Algebra (FractionRing A) OmegaFinal]
    [IsScalarTower A (FractionRing A) OmegaFinal]
    (y z : A)
    (hreg : IsRegular A [y, z])
    (hgen : Ideal.ofList [y, z] = maximalIdeal A)
    (N : ℕ) (hN : 0 < N)
    (hChar : CharZero (A ⧸ Ideal.span ({y} : Set A)))
    (fTower : Omega →ₐ[FractionRing A] OmegaFinal)
    (q : Ideal (integralClosure A Omega))
    (hqPrime : q.IsPrime)
    (hqOver : q.LiesOver (Ideal.span ({y} : Set A)))
    (hqExact : q.ramificationIdx A = N)
    (hAway :
      (Localization.awayMap
        (algebraMap A (integralClosure A Omega)) y).Etale) :
    let n : Fin 1 → ℕ := fun _ ↦ N
    let a : Fin 1 → A := fun _ ↦ y
    let Broot := iteratedRadical A 1 n a
    let hymax : y ∈ maximalIdeal A := by
      rw [← hgen]
      exact Ideal.subset_span (by simp)
    let ha : ∀ i, a i ∈ maximalIdeal A := fun _ ↦ hymax
    letI : IsLocalRing Broot :=
      isLocalRing_iteratedRadical n a (fun _ ↦ hN) ha
    ∀ {T : Type u} [CommRing T] [Algebra A T] [Algebra Broot T]
      [IsScalarTower A Broot T] [Module.Finite Broot T]
      [Algebra.Etale Broot T],
      ∀ (P : Ideal T) [P.IsMaximal]
        [P.LiesOver (maximalIdeal Broot)],
        (∀ [IsDomain (Localization.AtPrime P)],
          OmegaFinal →ₐ[A] FractionRing (Localization.AtPrime P)) →
          IsUnit (N : A) := by
  classical
  dsimp only
  intro T _ _ _ _ _ _ P hPMax hPOver fFinal
  let n : Fin 1 → ℕ := fun _ ↦ N
  let a : Fin 1 → A := fun _ ↦ y
  let Broot := iteratedRadical A 1 n a
  have hymax : y ∈ maximalIdeal A := by
    rw [← hgen]
    exact Ideal.subset_span (by simp)
  have ha : ∀ i, a i ∈ maximalIdeal A := fun _ ↦ hymax
  let : IsLocalRing Broot :=
    isLocalRing_iteratedRadical n a (fun _ ↦ hN) ha
  let : HenselianLocalRing Broot :=
    henselianLocalRing_iteratedRadical_of_isAdicComplete
      n a (fun _ ↦ hN) ha
  let : P.IsPrime := hPMax.isPrime
  let Dp := Localization.AtPrime P
  let : Algebra T Dp := inferInstance
  let bRootDpAlgebra : Algebra Broot Dp := inferInstance
  let : SMul Broot Dp := bRootDpAlgebra.toSMul
  let : IsScalarTower Broot T Dp := inferInstance
  let : Module.Finite Broot Dp :=
    moduleFinite_localizationAtPrime_of_henselian_of_etale P
  let : Algebra.Etale Broot Dp :=
    etale_localizationAtPrime_of_henselian_of_etale P
  let : IsLocalHom (algebraMap Broot Dp) :=
    isLocalHom_algebraMap_localizationAtPrime_of_liesOver_maximalIdeal P
  have huniqueDp : ∀ Q : Ideal Dp, Q.IsPrime →
      Q.LiesOver (maximalIdeal Broot) → Q = maximalIdeal Dp := by
    intro Q hQPrime hQOver
    exact prime_eq_maximalIdeal_of_liesOver_of_finite
      (R := Broot) (S := Dp) Q hQPrime hQOver
  let aDpAlgebra : Algebra A Dp := inferInstance
  let : SMul A Dp := aDpAlgebra.toSMul
  let : IsScalarTower A Broot Dp :=
    isScalarTower_of_algebra_tower_square
      (R := A) (S := Broot) (T := T) (U := Dp)
  let : Module.FaithfullyFlat A Broot :=
    faithfullyFlat_iteratedRadical n a (fun _ ↦ hN)
  let : @Module.FaithfullyFlat Broot Dp _ _
      bRootDpAlgebra.toModule :=
    @Module.FaithfullyFlat.of_flat_of_isLocalHom
      Broot Dp _ _ bRootDpAlgebra _ _ _ _
  let : @FaithfulSMul A Dp aDpAlgebra.toSMul := by
    apply (@faithfulSMul_iff_algebraMap_injective
      A Dp _ _ aDpAlgebra).mpr
    intro x x' hxx'
    apply FaithfulSMul.algebraMap_injective A Broot
    apply FaithfulSMul.algebraMap_injective Broot Dp
    simpa only [IsScalarTower.algebraMap_apply A Broot Dp] using hxx'
  let qDp := maximalIdeal Dp
  let : qDp.IsPrime := (maximalIdeal.isMaximal Dp).isPrime
  let : qDp.LiesOver (maximalIdeal Broot) := by
    apply (Ideal.liesOver_iff _ _).mpr
    exact (IsLocalRing.maximalIdeal_comap (algebraMap Broot Dp)).symm
  exact selectedExponent_finish_local_factor
    (A := A) (Omega := Omega) (OmegaFinal := OmegaFinal)
    y z hreg hgen N hN hChar fTower q hqPrime hqOver hqExact hAway
    (Dlocal := Dp) qDp huniqueDp fFinal

theorem

selectedExponent_finish_completed_root_pushout

L1546 ↗

EtaleFundamentalGroups.Kummer.selectedExponent_finish_completed_root_pushout

Documentation

Transport the finite-etale model across the completed one-root pushout, then hand the resulting local factor to the terminal calculation.

Source context 7 commands

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

noncomputable section
open scoped TensorProduct
namespace EtaleFundamentalGroups.Kummer
open IsLocalRing
open Polynomial
open RingTheory.Sequence
universe u

Lean source · statement

theorem selectedExponent_finish_completed_root_pushout
    {B D E A Omega OmegaFinal : Type u}
    [CommRing B]
    [CommRing D] [Algebra B D]
    [CommRing E] [Algebra B E] [Algebra D E]
    [IsScalarTower B D E] [Module.Finite D E] [Algebra.Etale D E]
    [CommRing A] [IsDomain A] [IsRegularLocalRing A]
    [IsAdicComplete (maximalIdeal A) A] [Algebra B A]
    [Field Omega] [Algebra A Omega] [Algebra (FractionRing A) Omega]
    [IsScalarTower A (FractionRing A) Omega]
    [FiniteDimensional (FractionRing A) Omega]
    [IsGalois (FractionRing A) Omega]
    [Field OmegaFinal] [Algebra A OmegaFinal]
    [Algebra (FractionRing A) OmegaFinal]
    [IsScalarTower A (FractionRing A) OmegaFinal]
    (y z : A)
    (hreg : IsRegular A [y, z])
    (hgen : Ideal.ofList [y, z] = maximalIdeal A)
    (N : ℕ) (hN : 0 < N)
    (hyMax : y ∈ maximalIdeal A)
    (hChar : CharZero (A ⧸ Ideal.span ({y} : Set A)))
    (eBaseRoot :
      (A ⊗[B] D) ≃ₐ[A] AdjoinRoot (X ^ N - Polynomial.C y))
    (Pfinal : Ideal (A ⊗[B] E))
    (hPfinalMax : Pfinal.IsMaximal)
    (fFinal :
      ∀ [IsDomain (Localization.AtPrime Pfinal)],
        OmegaFinal →ₐ[A] FractionRing (Localization.AtPrime Pfinal))
    (fTower : Omega →ₐ[FractionRing A] OmegaFinal)
    (q : Ideal (integralClosure A Omega))
    (hqPrime : q.IsPrime)
    (hqOver : q.LiesOver (Ideal.span ({y} : Set A)))
    (hqExact : q.ramificationIdx A = N)
    (hAway :
      (Localization.awayMap
        (algebraMap A (integralClosure A Omega)) y).Etale) :
    IsUnit (N : A)

inductive

SelectedExponentRootReadyPackage

L1658 ↗

EtaleFundamentalGroups.Kummer.SelectedExponentRootReadyPackage

Source context 7 commands

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

noncomputable section
open scoped TensorProduct
namespace EtaleFundamentalGroups.Kummer
open IsLocalRing
open Polynomial
open RingTheory.Sequence
universe u

Lean source · full declaration

inductive SelectedExponentRootReadyPackage
    {B D : Type u} [CommRing B] [CommRing D] [Algebra B D]
    (N : ℕ) : Prop where
  | mk
      (E A Omega OmegaFinal : Type u)
      [CommRing E] [Algebra B E] [Algebra D E]
      [IsScalarTower B D E] [Module.Finite D E] [Algebra.Etale D E]
      [CommRing A] [IsDomain A] [IsRegularLocalRing A]
      [IsAdicComplete (maximalIdeal A) A] [Algebra B A]
      [Field Omega] [Algebra A Omega] [Algebra (FractionRing A) Omega]
      [IsScalarTower A (FractionRing A) Omega]
      [FiniteDimensional (FractionRing A) Omega]
      [IsGalois (FractionRing A) Omega]
      [Field OmegaFinal] [Algebra A OmegaFinal]
      [Algebra (FractionRing A) OmegaFinal]
      [IsScalarTower A (FractionRing A) OmegaFinal]
      (y z : A)
      (hreg : IsRegular A [y, z])
      (hgen : Ideal.ofList [y, z] = maximalIdeal A)
      (hN : 0 < N)
      (hyMax : y ∈ maximalIdeal A)
      (hChar : CharZero (A ⧸ Ideal.span ({y} : Set A)))
      (eBaseRoot : (A ⊗[B] D) ≃ₐ[A]
        AdjoinRoot (X ^ N - Polynomial.C y))
      (Pfinal : Ideal (A ⊗[B] E))
      (hPfinalMax : Pfinal.IsMaximal)
      (fFinal : ∀ [IsDomain (Localization.AtPrime Pfinal)],
        OmegaFinal →ₐ[A] FractionRing (Localization.AtPrime Pfinal))
      (fTower : Omega →ₐ[FractionRing A] OmegaFinal)
      (q : Ideal (integralClosure A Omega))
      (hqPrime : q.IsPrime)
      (hqOver : q.LiesOver (Ideal.span ({y} : Set A)))
      (hqExact : q.ramificationIdx A = N)
      (hAway : (Localization.awayMap
        (algebraMap A (integralClosure A Omega)) y).Etale)
      (reflectUnit : IsUnit (N : A) → IsUnit (N : B)) :
      SelectedExponentRootReadyPackage N

theorem

selectedExponent_root_ready_from_prefix_package

L1697 ↗

EtaleFundamentalGroups.Kummer.selectedExponent_root_ready_from_prefix_package

Source context 7 commands

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

noncomputable section
open scoped TensorProduct
namespace EtaleFundamentalGroups.Kummer
open IsLocalRing
open Polynomial
open RingTheory.Sequence
universe u

Lean source · statement

theorem selectedExponent_root_ready_from_prefix_package
    {B D KB M₀ M : Type u}
    [CommRing B] [IsDomain B] [IsRegularLocalRing B]
    [CommRing D] [IsDomain D] [Algebra B D]
    [Field KB] [Algebra B KB] [IsFractionRing B KB]
    [Field M₀] [Algebra B M₀] [Algebra KB M₀]
    [IsScalarTower B KB M₀] [FiniteDimensional KB M₀]
    [IsGalois KB M₀]
    [Field M] [Algebra D M] [Algebra B M] [IsScalarTower B D M]
    [Algebra KB M] [IsScalarTower B KB M]
    [IsScalarTower B (integralClosure B M₀) M₀]
    [Module.Finite B (integralClosure B M₀)]
    [IsFractionRing (integralClosure B M₀) M₀]
    [Algebra B (integralClosure D M)]
    [IsScalarTower B D (integralClosure D M)]
    [IsScalarTower B (integralClosure D M) M]
    [Module.Finite B (integralClosure D M)]
    [IsFractionRing (integralClosure D M) M]
    (yB zB : B) (N : ℕ) (hN : 0 < N)
    (hregB : IsRegular B [yB, zB])
    (hgenB : Ideal.ofList [yB, zB] = maximalIdeal B)
    (hCharB : CharZero (B ⧸ Ideal.span ({yB} : Set B)))
    (g : integralClosure B M₀ →ₐ[B] integralClosure D M)
    (p : Ideal (integralClosure D M))
    (hPrefixPackage : SelectedExponentPrefixPackage
      (B := B) (D := D) (KB := KB) (M₀ := M₀) (M := M)
      yB zB hregB hgenB N g p)
    (hfiniteFinal : Module.Finite D (integralClosure D M))
    (hEtaleFinal : Algebra.Etale D (integralClosure D M))
    (eBaseRoot :
      (AdicCompletion (maximalIdeal B) B ⊗[B] D) ≃ₐ[AdicCompletion (maximalIdeal B) B]
        AdjoinRoot
          (X ^ N - C (algebraMap B (AdicCompletion (maximalIdeal B) B) yB))) :
    SelectedExponentRootReadyPackage (B := B) (D := D) N

theorem

selectedExponent_finish_root_ready_package

L1891 ↗

EtaleFundamentalGroups.Kummer.selectedExponent_finish_root_ready_package

Documentation

Consume the typed terminal boundary in a fresh instance context.

Source context 7 commands

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

noncomputable section
open scoped TensorProduct
namespace EtaleFundamentalGroups.Kummer
open IsLocalRing
open Polynomial
open RingTheory.Sequence
universe u

Lean source · statement

theorem selectedExponent_finish_root_ready_package
    {B D : Type u} [CommRing B] [CommRing D] [Algebra B D]
    {N : ℕ}
    (data : SelectedExponentRootReadyPackage (B := B) (D := D) N) :
    IsUnit (N : B)

theorem

selectedExponent_completion_from_prefix_package

L1910 ↗

EtaleFundamentalGroups.Kummer.selectedExponent_completion_from_prefix_package

Documentation

Unpack the prefix once, then cross the typed terminal boundary.

Source context 7 commands

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

noncomputable section
open scoped TensorProduct
namespace EtaleFundamentalGroups.Kummer
open IsLocalRing
open Polynomial
open RingTheory.Sequence
universe u

Lean source · statement

theorem selectedExponent_completion_from_prefix_package
    {B D KB M₀ M : Type u}
    [CommRing B] [IsDomain B] [IsRegularLocalRing B]
    [CommRing D] [IsDomain D] [Algebra B D]
    [Field KB] [Algebra B KB] [IsFractionRing B KB]
    [Field M₀] [Algebra B M₀] [Algebra KB M₀]
    [IsScalarTower B KB M₀] [FiniteDimensional KB M₀]
    [IsGalois KB M₀]
    [Field M] [Algebra D M] [Algebra B M] [IsScalarTower B D M]
    [Algebra KB M] [IsScalarTower B KB M]
    [IsScalarTower B (integralClosure B M₀) M₀]
    [Module.Finite B (integralClosure B M₀)]
    [IsFractionRing (integralClosure B M₀) M₀]
    [Algebra B (integralClosure D M)]
    [IsScalarTower B D (integralClosure D M)]
    [IsScalarTower B (integralClosure D M) M]
    [Module.Finite B (integralClosure D M)]
    [IsFractionRing (integralClosure D M) M]
    (yB zB : B) (N : ℕ) (hN : 0 < N)
    (hregB : IsRegular B [yB, zB])
    (hgenB : Ideal.ofList [yB, zB] = maximalIdeal B)
    (hCharB : CharZero (B ⧸ Ideal.span ({yB} : Set B)))
    (g : integralClosure B M₀ →ₐ[B] integralClosure D M)
    (p : Ideal (integralClosure D M))
    (hPrefixPackage : SelectedExponentPrefixPackage
      (B := B) (D := D) (KB := KB) (M₀ := M₀) (M := M)
      yB zB hregB hgenB N g p)
    (hfiniteFinal : Module.Finite D (integralClosure D M))
    (hEtaleFinal : Algebra.Etale D (integralClosure D M))
    (eBaseRoot :
      (AdicCompletion (maximalIdeal B) B ⊗[B] D) ≃ₐ[AdicCompletion (maximalIdeal B) B]
        AdjoinRoot
          (X ^ N - C (algebraMap B (AdicCompletion (maximalIdeal B) B) yB))) :
    IsUnit (N : B)

theorem

selectedExponent_completion_core

L1952 ↗

EtaleFundamentalGroups.Kummer.selectedExponent_completion_core

Documentation

Assemble the prefix package separately so the long completed calculation is checked in an independent declaration.

Source context 7 commands

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

noncomputable section
open scoped TensorProduct
namespace EtaleFundamentalGroups.Kummer
open IsLocalRing
open Polynomial
open RingTheory.Sequence
universe u

Lean source · statement

theorem selectedExponent_completion_core
    {B D KB M₀ M : Type u}
    [CommRing B] [IsDomain B] [IsRegularLocalRing B]
    [CommRing D] [IsDomain D] [Algebra B D]
    [Module.Finite B D] [Module.Flat B D]
    [Field KB] [Algebra B KB] [IsFractionRing B KB]
    [Field M₀] [Algebra B M₀] [Algebra KB M₀]
    [IsScalarTower B KB M₀] [FiniteDimensional KB M₀]
    [IsGalois KB M₀]
    [Field M] [Algebra D M] [Algebra B M] [IsScalarTower B D M]
    [Algebra KB M] [IsScalarTower B KB M]
    [Algebra B (integralClosure D M)]
    [IsScalarTower B D (integralClosure D M)]
    (yB zB : B) (N : ℕ) (hN : 0 < N)
    (hregB : IsRegular B [yB, zB])
    (hgenB : Ideal.ofList [yB, zB] = maximalIdeal B)
    (hdimB : ringKrullDim B = ((2 : ℕ∞) : WithBot ℕ∞))
    (hyBPrime : Prime yB)
    (hCharB : CharZero (B ⧸ Ideal.span ({yB} : Set B)))
    (g : integralClosure B M₀ →ₐ[B] integralClosure D M)
    (qGlobal p : Ideal (integralClosure D M))
    (hqGlobalPrime : qGlobal.IsPrime)
    (hqGlobalOverB : qGlobal.LiesOver (Ideal.span ({yB} : Set B)))
    (hqGlobalLe : qGlobal ≤ p)
    (hpMax : p.IsMaximal)
    (hpOverB : p.LiesOver (maximalIdeal B))
    (qPrefix : Ideal (integralClosure B M₀))
    [hqPrefixPrime : qPrefix.IsPrime]
    [hqPrefixOverB : qPrefix.LiesOver (Ideal.span ({yB} : Set B))]
    (hqGlobalComap : qGlobal.comap g.toRingHom = qPrefix)
    (hqPrefixExact : qPrefix.ramificationIdx B = N)
    (hAwayPrefix :
      (Localization.awayMap (algebraMap B (integralClosure B M₀)) yB).Etale)
    (hfiniteFinal : Module.Finite D (integralClosure D M))
    (hEtaleFinal : Algebra.Etale D (integralClosure D M))
    (hFractionFinal : IsFractionRing (integralClosure D M) M)
    (eBaseRoot :
      (AdicCompletion (maximalIdeal B) B ⊗[B] D) ≃ₐ[AdicCompletion (maximalIdeal B) B]
        AdjoinRoot
          (X ^ N - C (algebraMap B (AdicCompletion (maximalIdeal B) B) yB))) :
    IsUnit (N : B)

theorem

maximalIdeal_liesOver_of_finite_local_extension

L2034 ↗

EtaleFundamentalGroups.Kummer.maximalIdeal_liesOver_of_finite_local_extension

Documentation

The maximal ideal of a finite faithful extension of local rings lies over the maximal ideal of the base.

Source context 7 commands

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

noncomputable section
open scoped TensorProduct
namespace EtaleFundamentalGroups.Kummer
open IsLocalRing
open Polynomial
open RingTheory.Sequence
universe u

Lean source · statement

theorem maximalIdeal_liesOver_of_finite_local_extension
    {R S : Type u}
    [CommRing R] [IsLocalRing R]
    [CommRing S] [IsLocalRing S] [Algebra R S] [FaithfulSMul R S]
    (hfinite : Module.Finite R S) :
    (maximalIdeal S).LiesOver (maximalIdeal R)

theorem

retained_primes_lieOver_base_of_finite_local_extension

L2048 ↗

EtaleFundamentalGroups.Kummer.retained_primes_lieOver_base_of_finite_local_extension

Documentation

Contract a retained branch and its retained closed point through one finite local intermediate ring.

Source context 7 commands

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

noncomputable section
open scoped TensorProduct
namespace EtaleFundamentalGroups.Kummer
open IsLocalRing
open Polynomial
open RingTheory.Sequence
universe u

Lean source · statement

theorem retained_primes_lieOver_base_of_finite_local_extension
    {B D E : Type u}
    [CommRing B] [IsLocalRing B]
    [CommRing D] [IsLocalRing D] [Algebra B D] [FaithfulSMul B D]
    [CommRing E] [Algebra D E] [Algebra B E] [IsScalarTower B D E]
    (hfinite : Module.Finite B D)
    (qB : Ideal B) (qD : Ideal D)
    (qGlobal p : Ideal E)
    (hqDOverB : qD.LiesOver qB)
    (hqGlobalOverD : qGlobal.LiesOver qD)
    (hpOverD : p.LiesOver (maximalIdeal D)) :
    qGlobal.LiesOver qB ∧ p.LiesOver (maximalIdeal B)

theorem

selectedExponent_completion_of_component_fields

L2071 ↗

EtaleFundamentalGroups.Kummer.selectedExponent_completion_of_component_fields

Documentation

Finish from fixed component fields after contracting the retained final primes and identifying the final normalization's fraction field.

Source context 7 commands

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

noncomputable section
open scoped TensorProduct
namespace EtaleFundamentalGroups.Kummer
open IsLocalRing
open Polynomial
open RingTheory.Sequence
universe u

Lean source · statement

theorem selectedExponent_completion_of_component_fields
    {B D KB KD M₀ M : Type u}
    [CommRing B] [IsDomain B] [IsRegularLocalRing B]
    [CommRing D] [IsDomain D] [IsRegularLocalRing D] [Algebra B D]
    [Module.Finite B D] [Module.Flat B D] [FaithfulSMul B D]
    [Field KB] [Algebra B KB] [IsFractionRing B KB]
    [Field KD] [Algebra D KD] [IsFractionRing D KD]
    [Field M₀] [bM₀Algebra : Algebra B M₀] [Algebra KB M₀]
    [IsScalarTower B KB M₀] [FiniteDimensional KB M₀]
    [IsGalois KB M₀]
    [Field M] [dMAlgebra : Algebra D M] [bMAlgebra : Algebra B M]
    [IsScalarTower B D M]
    [Algebra KD M] [IsScalarTower D KD M] [FiniteDimensional KD M]
    [kbMAlgebra : Algebra KB M] [IsScalarTower B KB M]
    [bEAlgebra : Algebra B (integralClosure D M)]
    [bDETower : IsScalarTower B D (integralClosure D M)]
    (yB zB : B) (N : ℕ) (hN : 0 < N)
    (hregB : IsRegular B [yB, zB])
    (hgenB : Ideal.ofList [yB, zB] = maximalIdeal B)
    (hdimB : ringKrullDim B = ((2 : ℕ∞) : WithBot ℕ∞))
    (hyBPrime : Prime yB)
    (hCharB : CharZero (B ⧸ Ideal.span ({yB} : Set B)))
    (g : integralClosure B M₀ →ₐ[B] integralClosure D M)
    (qD : Ideal D)
    (hqDOverB : qD.LiesOver (Ideal.span ({yB} : Set B)))
    (qGlobal p : Ideal (integralClosure D M))
    (hqGlobalPrime : qGlobal.IsPrime)
    (hqGlobalOverD : qGlobal.LiesOver qD)
    (hqGlobalLe : qGlobal ≤ p)
    (hpMax : p.IsMaximal)
    (hpOverD : p.LiesOver (maximalIdeal D))
    (qPrefix : Ideal (integralClosure B M₀))
    (hqGlobalComap : qGlobal.comap g.toRingHom = qPrefix)
    (hqPrefixPrime : qPrefix.IsPrime)
    (hqPrefixOverB : qPrefix.LiesOver (Ideal.span ({yB} : Set B)))
    (hqPrefixExact : qPrefix.ramificationIdx B = N)
    (hAwayPrefix :
      (Localization.awayMap
        (algebraMap B (integralClosure B M₀)) yB).Etale)
    (hfiniteFinal : Module.Finite D (integralClosure D M))
    (hEtaleFinal : Algebra.Etale D (integralClosure D M))
    (eBaseRoot :
      (AdicCompletion (maximalIdeal B) B ⊗[B] D) ≃ₐ[AdicCompletion (maximalIdeal B) B]
        AdjoinRoot
          (X ^ N - C (algebraMap B (AdicCompletion (maximalIdeal B) B) yB))) :
    IsUnit (N : B)

def

SelectedExponentComponentFieldsGoal

L2137 ↗

EtaleFundamentalGroups.Kummer.SelectedExponentComponentFieldsGoal

Documentation

The exact-prime goal after both component fields and their normalization map have been fixed.

Source context 7 commands

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

noncomputable section
open scoped TensorProduct
namespace EtaleFundamentalGroups.Kummer
open IsLocalRing
open Polynomial
open RingTheory.Sequence
universe u

Lean source · statement

def SelectedExponentComponentFieldsGoal
    {B D M₀ M : Type u}
    [CommRing B] [CommRing D] [IsLocalRing D] [Algebra B D]
    [Field M₀] [_bM₀Algebra : Algebra B M₀]
    [Field M] [_dMAlgebra : Algebra D M]
    [_bEAlgebra : Algebra B (integralClosure D M)]
    (yB : B) (N : ℕ) (qD : Ideal D) : Prop

theorem

selectedExponent_completion_of_component_fields_goal

L2162 ↗

EtaleFundamentalGroups.Kummer.selectedExponent_completion_of_component_fields_goal

Documentation

Prove the exact-prime goal once both component fields are fixed.

Source context 7 commands

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

noncomputable section
open scoped TensorProduct
namespace EtaleFundamentalGroups.Kummer
open IsLocalRing
open Polynomial
open RingTheory.Sequence
universe u

Lean source · statement

theorem selectedExponent_completion_of_component_fields_goal
    {B D KB KD M₀ M : Type u}
    [CommRing B] [IsDomain B] [IsRegularLocalRing B]
    [CommRing D] [IsDomain D] [IsRegularLocalRing D] [Algebra B D]
    [Module.Finite B D] [Module.Flat B D] [FaithfulSMul B D]
    [Field KB] [Algebra B KB] [IsFractionRing B KB]
    [Field KD] [Algebra D KD] [IsFractionRing D KD]
    [m₀Field : Field M₀] [bM₀Algebra : Algebra B M₀]
    [kbM₀Algebra : Algebra KB M₀]
    [bKBM₀Tower : IsScalarTower B KB M₀]
    [kbM₀Finite : FiniteDimensional KB M₀]
    [kbM₀Galois : IsGalois KB M₀]
    [Field M] [dMAlgebra : Algebra D M] [bMAlgebra : Algebra B M]
    [IsScalarTower B D M]
    [Algebra KD M] [IsScalarTower D KD M] [FiniteDimensional KD M]
    [kbMAlgebra : Algebra KB M] [IsScalarTower B KB M]
    [bEAlgebra : Algebra B (integralClosure D M)]
    [bDETower : IsScalarTower B D (integralClosure D M)]
    (yB zB : B) (N : ℕ) (hN : 0 < N)
    (hregB : IsRegular B [yB, zB])
    (hgenB : Ideal.ofList [yB, zB] = maximalIdeal B)
    (hdimB : ringKrullDim B = ((2 : ℕ∞) : WithBot ℕ∞))
    (hyBPrime : Prime yB)
    (hCharB : CharZero (B ⧸ Ideal.span ({yB} : Set B)))
    (qD : Ideal D)
    (hqDOverB : qD.LiesOver (Ideal.span ({yB} : Set B)))
    (eBaseRoot :
      (AdicCompletion (maximalIdeal B) B ⊗[B] D) ≃ₐ[AdicCompletion (maximalIdeal B) B]
        AdjoinRoot
          (X ^ N - C (algebraMap B (AdicCompletion (maximalIdeal B) B) yB))) :
    SelectedExponentComponentFieldsGoal
      (B := B) (D := D) (M₀ := M₀) (M := M)
      (_bM₀Algebra := bM₀Algebra) (_dMAlgebra := dMAlgebra)
      (_bEAlgebra := bEAlgebra) yB N qD

def

SelectedExponentFixedFinalGoal

L2213 ↗

EtaleFundamentalGroups.Kummer.SelectedExponentFixedFinalGoal

Documentation

The remaining selected-exponent goal after fixing the final generic tensor component, expressed through its actual intermediate contraction.

Source context 7 commands

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

noncomputable section
open scoped TensorProduct
namespace EtaleFundamentalGroups.Kummer
open IsLocalRing
open Polynomial
open RingTheory.Sequence
universe u

Lean source · statement

def SelectedExponentFixedFinalGoal
    {K L B D KB KD M : Type u}
    [Field K] [Field L] [Algebra K L]
    [FiniteDimensional K L] [IsGalois K L]
    [CommRing B] [IsDomain B] [IsRegularLocalRing B]
    [CommRing D] [IsDomain D] [IsRegularLocalRing D] [Algebra B D]
    [Module.Finite B D] [Module.Flat B D] [FaithfulSMul B D]
    [Field KB] [Algebra B KB] [IsFractionRing B KB]
    [Field KD] [Algebra D KD] [IsFractionRing D KD]
    [Algebra K KB] [Algebra K KD]
    [Algebra B KD] [IsScalarTower B D KD]
    [Algebra KB KD] [IsScalarTower B KB KD]
    [IsScalarTower K KB KD] [FiniteDimensional KB KD]
    (m : Ideal (KD ⊗[K] L)) [m.IsMaximal]
    [Field M]
    [dMAlgebra : Algebra D M] [_bMAlgebra : Algebra B M]
    [_bDMTower : IsScalarTower B D M]
    [_kdMAlgebra : Algebra KD M] [_dKDMTower : IsScalarTower D KD M]
    [FiniteDimensional KD M]
    [_kbMAlgebra : Algebra KB M] [_bKBMTower : IsScalarTower B KB M]
    [bEAlgebra : Algebra B (integralClosure D M)]
    [_bDETower : IsScalarTower B D (integralClosure D M)]
    (yB : B) (N : ℕ) (qD : Ideal D) : Prop

theorem

selectedExponent_completion_of_fixed_final_component

L2263 ↗

EtaleFundamentalGroups.Kummer.selectedExponent_completion_of_fixed_final_component

Documentation

Prove the intermediate-contraction goal for a fixed final component.

Source context 7 commands

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

noncomputable section
open scoped TensorProduct
namespace EtaleFundamentalGroups.Kummer
open IsLocalRing
open Polynomial
open RingTheory.Sequence
universe u

Lean source · statement

theorem selectedExponent_completion_of_fixed_final_component
    {K L B D KB KD M : Type u}
    [Field K] [Field L] [Algebra K L]
    [FiniteDimensional K L] [IsGalois K L]
    [CommRing B] [IsDomain B] [IsRegularLocalRing B]
    [CommRing D] [IsDomain D] [IsRegularLocalRing D] [Algebra B D]
    [Module.Finite B D] [Module.Flat B D] [FaithfulSMul B D]
    [Field KB] [Algebra B KB] [IsFractionRing B KB]
    [Field KD] [Algebra D KD] [IsFractionRing D KD]
    [Algebra K KB] [Algebra K KD]
    [Algebra B KD] [IsScalarTower B D KD]
    [Algebra KB KD] [IsScalarTower B KB KD]
    [IsScalarTower K KB KD] [FiniteDimensional KB KD]
    (m : Ideal (KD ⊗[K] L)) [m.IsMaximal]
    [Field M]
    [dMAlgebra : Algebra D M] [bMAlgebra : Algebra B M]
    [bDMTower : IsScalarTower B D M]
    [kdMAlgebra : Algebra KD M] [dKDMTower : IsScalarTower D KD M]
    [FiniteDimensional KD M]
    [kbMAlgebra : Algebra KB M] [bKBMTower : IsScalarTower B KB M]
    [bEAlgebra : Algebra B (integralClosure D M)]
    [bDETower : IsScalarTower B D (integralClosure D M)]
    (yB zB : B) (N : ℕ) (hN : 0 < N)
    (hregB : IsRegular B [yB, zB])
    (hgenB : Ideal.ofList [yB, zB] = maximalIdeal B)
    (hdimB : ringKrullDim B = ((2 : ℕ∞) : WithBot ℕ∞))
    (hyBPrime : Prime yB)
    (hCharB : CharZero (B ⧸ Ideal.span ({yB} : Set B)))
    (qD : Ideal D)
    (hqDOverB : qD.LiesOver (Ideal.span ({yB} : Set B)))
    (eBaseRoot :
      (AdicCompletion (maximalIdeal B) B ⊗[B] D) ≃ₐ[AdicCompletion (maximalIdeal B) B]
        AdjoinRoot
          (X ^ N - C (algebraMap B (AdicCompletion (maximalIdeal B) B) yB))) :
    SelectedExponentFixedFinalGoal
      (K := K) (L := L) (B := B) (D := D) (KB := KB) (KD := KD)
      (m := m) (M := M) (dMAlgebra := dMAlgebra)
      (_bMAlgebra := bMAlgebra) (_bDMTower := bDMTower)
      (_dKDMTower := dKDMTower) (_kbMAlgebra := kbMAlgebra)
      (_bKBMTower := bKBMTower) (bEAlgebra := bEAlgebra)
      (_bDETower := bDETower)
      yB N qD

def

SelectedExponentFixedFractionFieldsGoal

L2321 ↗

EtaleFundamentalGroups.Kummer.SelectedExponentFixedFractionFieldsGoal

Documentation

The selected-exponent goal after fixing the two fraction fields.

Source context 7 commands

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

noncomputable section
open scoped TensorProduct
namespace EtaleFundamentalGroups.Kummer
open IsLocalRing
open Polynomial
open RingTheory.Sequence
universe u

Lean source · statement

def SelectedExponentFixedFractionFieldsGoal
    {K L B D KB KD : Type u}
    [Field K] [Field L] [Algebra K L]
    [FiniteDimensional K L] [IsGalois K L]
    [CommRing B] [IsDomain B] [IsRegularLocalRing B]
    [CommRing D] [IsDomain D] [IsRegularLocalRing D] [Algebra B D]
    [Module.Finite B D] [Module.Flat B D] [FaithfulSMul B D]
    [Field KB] [Algebra B KB] [IsFractionRing B KB]
    [Field KD] [Algebra D KD] [IsFractionRing D KD]
    [Algebra K KB] [Algebra K KD]
    [Algebra B KD] [IsScalarTower B D KD]
    [Algebra KB KD] [IsScalarTower B KB KD]
    [IsScalarTower K KB KD] [FiniteDimensional KB KD]
    (yB : B) (N : ℕ) (qD : Ideal D) : Prop

theorem

selectedExponent_completion_of_fixed_fraction_fields

L2384 ↗

EtaleFundamentalGroups.Kummer.selectedExponent_completion_of_fixed_fraction_fields

Documentation

Select the final component and its intermediate contraction over the two fixed fraction fields.

Source context 7 commands

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

noncomputable section
open scoped TensorProduct
namespace EtaleFundamentalGroups.Kummer
open IsLocalRing
open Polynomial
open RingTheory.Sequence
universe u

Lean source · statement

theorem selectedExponent_completion_of_fixed_fraction_fields
    {K L B D KB KD : Type u}
    [Field K] [Field L] [Algebra K L]
    [FiniteDimensional K L] [IsGalois K L]
    [CommRing B] [IsDomain B] [IsRegularLocalRing B]
    [CommRing D] [IsDomain D] [IsRegularLocalRing D] [Algebra B D]
    [Module.Finite B D] [Module.Flat B D] [FaithfulSMul B D]
    [Field KB] [Algebra B KB] [IsFractionRing B KB]
    [Field KD] [Algebra D KD] [IsFractionRing D KD]
    [Algebra K KB] [Algebra K KD]
    [Algebra B KD] [IsScalarTower B D KD]
    [Algebra KB KD] [IsScalarTower B KB KD]
    [IsScalarTower K KB KD] [FiniteDimensional KB KD]
    (yB zB : B) (N : ℕ) (hN : 0 < N)
    (hregB : IsRegular B [yB, zB])
    (hgenB : Ideal.ofList [yB, zB] = maximalIdeal B)
    (hdimB : ringKrullDim B = ((2 : ℕ∞) : WithBot ℕ∞))
    (hyBPrime : Prime yB)
    (hCharB : CharZero (B ⧸ Ideal.span ({yB} : Set B)))
    (qD : Ideal D)
    (hqDOverB : qD.LiesOver (Ideal.span ({yB} : Set B)))
    (eBaseRoot :
      (AdicCompletion (maximalIdeal B) B ⊗[B] D) ≃ₐ[AdicCompletion (maximalIdeal B) B]
        AdjoinRoot
          (X ^ N - C (algebraMap B (AdicCompletion (maximalIdeal B) B) yB))) :
    SelectedExponentFixedFractionFieldsGoal
      (K := K) (L := L) (B := B) (D := D) (KB := KB) (KD := KD)
      yB N qD

theorem

isUnit_natCast_of_finite_local_extension

L2427 ↗

EtaleFundamentalGroups.Kummer.isUnit_natCast_of_finite_local_extension

Documentation

A natural-number unit descends along a finite map of local rings.

Source context 7 commands

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

noncomputable section
open scoped TensorProduct
namespace EtaleFundamentalGroups.Kummer
open IsLocalRing
open Polynomial
open RingTheory.Sequence
universe u

Lean source · statement

theorem isUnit_natCast_of_finite_local_extension
    {R S : Type u}
    [CommRing R] [IsLocalRing R]
    [CommRing S] [IsLocalRing S] [Algebra R S] [FaithfulSMul R S]
    (hfinite : Module.Finite R S) (N : ℕ)
    (hUnit : IsUnit (N : S)) :
    IsUnit (N : R)

theorem

splitStrictNormalCrossings_heightTwo_galoisFullRootCover_selectedExponent_isUnit

L2444 ↗

EtaleFundamentalGroups.Kummer.splitStrictNormalCrossings_heightTwo_galoisFullRootCover_selectedExponent_isUnit

Documentation

The exponent of the selected branch is a unit at every height-two point.

The proof uses the same retained completion prime for the final finite-etale normalization and for its canonical prefix normalization.

Source context 7 commands

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

noncomputable section
open scoped TensorProduct
namespace EtaleFundamentalGroups.Kummer
open IsLocalRing
open Polynomial
open RingTheory.Sequence
universe u

Lean source · statement

theorem
    splitStrictNormalCrossings_heightTwo_galoisFullRootCover_selectedExponent_isUnit
    {A K L : Type u}
    [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]
    [Module.Finite A (integralClosure A L)]
    {d r : ℕ} {f : A} {t : Fin (d + 1) → A}
    (hNC : IsSplitStrictNormalCrossingsAt f t r)
    (i : Fin (d + 1)) (hi : i.1 < r)
    (P : Ideal A) [P.IsPrime] (hP : P.height = 2)
    (htiP : t i ∈ P)
    (hCharZero : ∀ j, j.1 < r →
      CharZero (A ⧸ Ideal.span ({t j} : Set A)))
    (hAwayBase : (Localization.awayMap
      (algebraMap A (integralClosure A L)) f).Etale) :
    IsUnit
      ((heightTwoSelectedBranchGaloisRamificationIndex
          (K := K) (L := L) t hNC i : ℕ) :
        Localization.AtPrime P)

Module documentation

The selected exponent from the retained completed component

Declarations