NYLL
Module

OriginalFiniteFieldCanonicalTameExactness.lean

Nyll.EtaleFundamentalGroups.Inertia.OriginalFiniteFieldCanonicalTameExactness
3 declarations indexed from sourceView source ↗

Module documentation

Exactness of finite-field tame characters

Constructs the original finite-field canonical tame morphism and an independent principal-unit wild subgroup. Proves surjectivity and identifies that subgroup as the kernel.

Imports6
Imported by5

Declarations

def

originalFiniteFieldCanonicalTameMorphism

L31 ↗
EtaleFundamentalGroups.Inertia.originalFiniteFieldCanonicalTameMorphism
Documentation

The same intrinsic canonical character, evaluated on the actual normalization action of the original finite field inertia.

Source context 4 commands

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

noncomputable section
namespace EtaleFundamentalGroups.Inertia
open CategoryTheory SchemeTheory
universe u v w
Lean source · statement
def originalFiniteFieldCanonicalTameMorphism
    (A : Type u) (K : Type v) (F : Type w)
    [CommRing A] [IsDomain A] [IsDiscreteValuationRing A]
    [Field K] [Field F] [Algebra A K] [IsFractionRing A K]
    [Algebra K F] [Algebra A F] [IsScalarTower A K F]
    [FiniteDimensional K F] [IsGalois K F]
    (Q : Ideal (normalizationCommAlgCat A F)) [Q.IsMaximal] :
    actualNormalizationInertiaGroup A K F Q ⟶
      originalFiniteNormalizationTameRootsGroup A K F Q
def

originalFiniteFieldWildSubgroup

L46 ↗
EtaleFundamentalGroups.Inertia.originalFiniteFieldWildSubgroup
Documentation

The actual principal-unit wild subgroup, pulled back through the prescribed normalization restriction. This definition is independent of the canonical character.

Source context 4 commands

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

noncomputable section
namespace EtaleFundamentalGroups.Inertia
open CategoryTheory SchemeTheory
universe u v w
Lean source · statement
def originalFiniteFieldWildSubgroup
    (A : Type u) (K : Type v) (F : Type w)
    [CommRing A] [IsDomain A] [IsDiscreteValuationRing A]
    [Field K] [Field F] [Algebra A K] [IsFractionRing A K]
    [Algebra K F] [Algebra A F] [IsScalarTower A K F]
    [FiniteDimensional K F] [IsGalois K F]
    (Q : Ideal (normalizationCommAlgCat A F)) [Q.IsMaximal] :
    Subgroup (actualNormalizationInertiaGroup A K F Q)
theorem

originalFiniteFieldCanonicalTameMorphism_exact

L60 ↗
EtaleFundamentalGroups.Inertia.originalFiniteFieldCanonicalTameMorphism_exact
Documentation

At one actual finite Galois stage, the original inertia maps onto the full canonical residue-root group and has precisely the independently defined principal-unit wild kernel. All comparison data are constructed.

Source context 4 commands

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

noncomputable section
namespace EtaleFundamentalGroups.Inertia
open CategoryTheory SchemeTheory
universe u v w
Lean source · statement
theorem originalFiniteFieldCanonicalTameMorphism_exact
    (A : Type u) (K : Type v) (F : Type w)
    [CommRing A] [IsDomain A] [IsDiscreteValuationRing A]
    [Field K] [Field F] [Algebra A K] [IsFractionRing A K]
    [Algebra K F] [Algebra A F] [IsScalarTower A K F]
    [FiniteDimensional K F] [IsGalois K F]
    (Q : Ideal (normalizationCommAlgCat A F)) [Q.IsMaximal] :
    Function.Surjective (originalFiniteFieldCanonicalTameMorphism A K F Q).hom.toFun ∧
      (originalFiniteFieldCanonicalTameMorphism A K F Q).hom.ker =
        originalFiniteFieldWildSubgroup A K F Q

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