Module

DivisorialCanonicalSourceConjugacy.lean

Nyll.EtaleFundamentalGroups.Inertia.DivisorialCanonicalSourceConjugacy

3 declarations indexed from sourceView source ↗

Module documentation

Canonical field sources for divisorial cyclotomic conjugacy

At every finite Galois cover, normalization-prime inertia has an actual canonical source: the fundamental group of the inertia fixed field. This file expresses a profinite element by compatible finite-level source lifts and proves that these lifts imply the finite-quotient inertia-membership condition used by divisorial cyclotomic conjugacy.

The fixed field and its separable closure depend on the finite cover. No single strict-henselization object is postulated here.

Imports2

Imported by1

Nyll.EtaleFundamentalGroups.Inertia.All

def

IsCanonicalNormalizationPrimeInertiaSourceElement

L42 ↗

EtaleFundamentalGroups.Inertia.IsCanonicalNormalizationPrimeInertiaSourceElement

Documentation

A fundamental-group element is represented by the actual canonical normalization-prime inertia-field source in every pointed connected finite Galois quotient. The witness is a source element whose image is exactly the finite deck image of the given profinite element.

This definition uses source maps, rather than assuming ideal-inertia membership or cyclotomic conjugacy as a conclusion.

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 IsCanonicalNormalizationPrimeInertiaSourceElement
    {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

normalizationPrimeInertiaInFiniteQuotients_of_canonicalSource

L92 ↗

EtaleFundamentalGroups.Inertia.normalizationPrimeInertiaInFiniteQuotients_of_canonicalSource

Documentation

Actual canonical inertia-field source lifts land in normalization-prime ideal inertia at every finite quotient.

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

theorem
    normalizationPrimeInertiaInFiniteQuotients_of_canonicalSource
    {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))
    (hgamma : IsCanonicalNormalizationPrimeInertiaSourceElement
      xi P gamma) :
    IsNormalizationPrimeInertiaElementInFiniteQuotients xi P gamma

theorem

isConj_inv_of_isCanonicalNormalizationPrimeInertiaSourceElement_of_geometricallyIntegral_divisor

L146 ↗

EtaleFundamentalGroups.Inertia.isConj_inv_of_isCanonicalNormalizationPrimeInertiaSourceElement_of_geometricallyIntegral_divisor

Documentation

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

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

theorem
    isConj_inv_of_isCanonicalNormalizationPrimeInertiaSourceElement_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 : IsCanonicalNormalizationPrimeInertiaSourceElement
      xi P gamma) :
    IsConj gamma gamma⁻¹

Module documentation

Canonical field sources for divisorial cyclotomic conjugacy

Declarations

IsCanonicalNormalizationPrimeInertiaSourceElement

normalizationPrimeInertiaInFiniteQuotients_of_canonicalSource

isConj_inv_of_isCanonicalNormalizationPrimeInertiaSourceElement_of_geometricallyIntegral_divisor