Nyll.EtaleFundamentalGroups.Kummer.AdjoinRoot.Global.FiniteEtaleExponentUnit

Module documentation

Exact-root completion terminal without a public closed prime

A finite algebra over the local exact-root cover has a maximal ideal over the closed point by lying over. This file chooses that ideal internally and feeds the resulting literal prime to the global-Away same-prime completion terminal.

Thus a caller which has produced one global finite-etale normalization factor and its primitive Away map need not expose a comparison with an independently chosen completed factor or a closed-prime parameter.

theorem

exponent_isUnit_of_adjoinRoot_global_finiteEtale_boundaryAway

L35 ↗

EtaleFundamentalGroups.Kummer.exponent_isUnit_of_adjoinRoot_global_finiteEtale_boundaryAway

Documentation

A global finite-etale factor of the one-root cover, together with its literal primitive Away map, forces the root exponent to be a unit.

The closed prime is produced from module-finiteness and is then tracked by the same-prime completion theorem. No prime comparison, component bijection, or degree equality is a public hypothesis.

Source context 4 commands

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

noncomputable section
namespace EtaleFundamentalGroups.Kummer
open IsLocalRing
universe uA uE

Lean source · statement

theorem
    exponent_isUnit_of_adjoinRoot_global_finiteEtale_boundaryAway
    {A : Type uA} [CommRing A] [IsDomain A] [IsRegularLocalRing A]
    {N : ℕ} (hN : 0 < N) {y : A} (hy : Prime y)
    (hyQuot : IsRegularLocalRing (A ⧸ Ideal.span ({y} : Set A)))
    (hdim : ringKrullDim A = ((2 : ℕ∞) : WithBot ℕ∞))
    (hCharZero : CharZero (A ⧸ Ideal.span ({y} : Set A)))
    {E : Type uE} [CommRing E] [Nontrivial E]
    [Algebra
      (AdjoinRoot (Polynomial.X ^ N - Polynomial.C y)) E]
    [Algebra A E]
    [IsScalarTower A
      (AdjoinRoot (Polynomial.X ^ N - Polynomial.C y)) E]
    [Module.Finite
      (AdjoinRoot (Polynomial.X ^ N - Polynomial.C y)) E]
    [Algebra.Etale
      (AdjoinRoot (Polynomial.X ^ N - Polynomial.C y)) E]
    [IsLocalRing
      (AdjoinRoot (Polynomial.X ^ N - Polynomial.C y))]
    (hAway : (Localization.awayMap (algebraMap A E) y).Etale) :
    IsUnit (N : A)

Module documentation

Exact-root completion terminal without a public closed prime

Declarations

exponent_isUnit_of_adjoinRoot_global_finiteEtale_boundaryAway