NYLL
Module

DivisorialCyclotomicConjugacy.lean

Nyll.EtaleFundamentalGroups.Inertia.DivisorialCyclotomicConjugacy
2 declarations indexed from sourceView source ↗

Module documentation

Divisorial cyclotomic conjugacy from finite quotients

Membership in a divisorial inertia group can be expressed without constructing a strict henselization: in every pointed connected finite Galois cover, the image of the element belongs to normalization-prime inertia above the fixed height-one boundary prime. Cyclotomic inversion in each actual deck group, together with finite-quotient detection of conjugacy in a profinite group, then gives conjugacy in the etale fundamental group itself.

Imports3
Imported by4

Declarations

def

IsNormalizationPrimeInertiaElementInFiniteQuotients

L42 ↗
EtaleFundamentalGroups.Inertia.IsNormalizationPrimeInertiaElementInFiniteQuotients
Documentation

The finite-quotient characterization of membership in divisorial inertia above a fixed boundary prime. For every actual pointed connected finite Galois cover, a normalization prime above the boundary prime is chosen at that finite level and the image of the element is required to lie in its ideal-inertia subgroup.

This is an inertia-membership condition; it does not assume conjugacy with the inverse or any other conclusion of the cyclotomic theorem.

Source context 7 commands

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

noncomputable section
open AlgebraicGeometry CategoryTheory
open AlgebraicGeometry.FiniteEtale
open CategoryTheory.PreGaloisCategory
open RamificationTheory.HilbertRamification
namespace EtaleFundamentalGroups.Inertia
universe u
Lean source · statement
def IsNormalizationPrimeInertiaElementInFiniteQuotients
    {U : Scheme.{u}} [IsIntegral U] [IsNormalIntegral U]
    [IsLocallyNoetherian U]
    {Omega : Type u} [Field Omega] [IsSepClosed Omega]
    (xi : Spec (.of Omega) ⟶ U)
    {A : Type u} [CommRing A] [IsDomain A] [IsIntegrallyClosed A]
    [Algebra A U.functionField] [IsFractionRing A U.functionField]
    (P : Ideal A) [P.IsPrime]
    (gamma : π₁ᵉᵗ(xi)) : Prop
theorem

isConj_inv_of_isNormalizationPrimeInertiaElementInFiniteQuotients_of_geometricallyIntegral_divisor

L85 ↗
EtaleFundamentalGroups.Inertia.isConj_inv_of_isNormalizationPrimeInertiaElementInFiniteQuotients_of_geometricallyIntegral_divisor
Documentation

A finite-quotient divisorial inertia element at a geometrically integral height-one boundary prime is conjugate to its inverse in the full etale fundamental group.

Source context 8 commands

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

noncomputable section
open AlgebraicGeometry CategoryTheory
open AlgebraicGeometry.FiniteEtale
open CategoryTheory.PreGaloisCategory
open RamificationTheory.HilbertRamification
namespace EtaleFundamentalGroups.Inertia
universe u
open _root_.EtaleFundamentalGroups.Kummer
  (finiteEtaleGaloisCover_heightOneIdealInertia_isConj_inv_of_geometricallyIntegral_divisor) in
Lean source · statement
theorem
  isConj_inv_of_isNormalizationPrimeInertiaElementInFiniteQuotients_of_geometricallyIntegral_divisor
    (k : Type u) [Field k] (ek : k ≃+* ℚ)
    {U : Scheme.{u}} [IsIntegral U] [IsNormalIntegral U]
    [IsLocallyNoetherian U]
    {Omega : Type u} [Field Omega] [IsSepClosed Omega]
    (xi : Spec (.of Omega) ⟶ U)
    {A : Type u} [CommRing A] [IsDomain A] [IsRegularRing A]
    [IsIntegrallyClosed A]
    [Algebra A U.functionField] [IsFractionRing A U.functionField]
    (P : Ideal A) [P.IsPrime] (hP : P.height = 1)
    [Algebra k (A ⧸ P)]
    (hgeo : GeometricallyIntegral
      (Spec.map (CommRingCat.ofHom (algebraMap k (A ⧸ P)))))
    (gamma : π₁ᵉᵗ(xi))
    (hgamma :
      IsNormalizationPrimeInertiaElementInFiniteQuotients xi P gamma) :
    IsConj gamma gamma⁻¹

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