NYLL
Module

OriginalFiniteNormalizationTameExactness.lean

Nyll.EtaleFundamentalGroups.Inertia.OriginalFiniteNormalizationTameExactness
5 declarations indexed from sourceView source ↗

Module documentation

Canonical tame exactness on the original normalization

Constructs the intrinsic canonical tame morphism and principal-unit wild subgroup from a finite Galois extension. Proves surjectivity onto the full roots group and identifies the wild subgroup as its kernel.

Imports13
Imported by7

Declarations

theorem

originalFiniteNormalizationPrime_ne_bot

L39 ↗
EtaleFundamentalGroups.Inertia.originalFiniteNormalizationPrime_ne_bot
Documentation

The chosen maximal prime of the original finite normalization is nonzero: its contraction is the nonzero maximal ideal of the original DVR.

Source context 4 commands

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

noncomputable section
namespace EtaleFundamentalGroups.Inertia
open SchemeTheory CategoryTheory
universe u v w
Lean source · statement
theorem originalFiniteNormalizationPrime_ne_bot
    (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]
    (Q : Ideal (normalizationCommAlgCat A F).carrier) [Q.IsMaximal] : Q ≠ ⊥
def

originalFiniteNormalizationTameRootsGroup

L60 ↗
EtaleFundamentalGroups.Inertia.originalFiniteNormalizationTameRootsGroup
Documentation

The full roots-of-unity group of the actual intrinsic tame order at the chosen original normalization prime.

Source context 4 commands

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

noncomputable section
namespace EtaleFundamentalGroups.Inertia
open SchemeTheory CategoryTheory
universe u v w
Lean source · statement
def originalFiniteNormalizationTameRootsGroup
    (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] : GrpCat.{w}
def

originalFiniteNormalizationTameMorphism

L74 ↗
EtaleFundamentalGroups.Inertia.originalFiniteNormalizationTameMorphism
Documentation

The existing intrinsic canonical tame morphism, on the actual original normalization and with all its arithmetic data supplied by the finite extension.

Source context 4 commands

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

noncomputable section
namespace EtaleFundamentalGroups.Inertia
open SchemeTheory CategoryTheory
universe u v w
Lean source · statement
def originalFiniteNormalizationTameMorphism
    (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] :
    commAlgIdealInertiaGroup A (normalizationCommAlgCat A F) Q ⟶
      originalFiniteNormalizationTameRootsGroup A K F Q
def

originalFiniteNormalizationWildSubgroup

L93 ↗
EtaleFundamentalGroups.Inertia.originalFiniteNormalizationWildSubgroup
Documentation

The independent principal-unit wild subgroup in intrinsic original normalization inertia. It is defined by the existing local wild subgroup.

Source context 4 commands

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

noncomputable section
namespace EtaleFundamentalGroups.Inertia
open SchemeTheory CategoryTheory
universe u v w
Lean source · statement
def originalFiniteNormalizationWildSubgroup
    (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 (commAlgIdealInertiaGroup A (normalizationCommAlgCat A F) Q)
theorem

originalFiniteNormalizationTameMorphism_exact

L111 ↗
EtaleFundamentalGroups.Inertia.originalFiniteNormalizationTameMorphism_exact
Documentation

From the original finite Galois extension alone, the same intrinsic canonical character is onto its full root group and has exactly the independently defined principal-unit wild kernel. The original field tower is closed before the finite inertia exactness theorem is applied.

Source context 4 commands

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

noncomputable section
namespace EtaleFundamentalGroups.Inertia
open SchemeTheory CategoryTheory
universe u v w
Lean source · statement
theorem originalFiniteNormalizationTameMorphism_exact
    (A : Type u) (K : Type v) (F : Type w)
    [rA : CommRing A] [dA : IsDomain A] [vA : IsDiscreteValuationRing A]
    [fK : Field K] [fF : Field F]
    [aAK : Algebra A K] [fAK : IsFractionRing A K]
    [aKF : Algebra K F] [aAF : Algebra A F] [tAKF : IsScalarTower A K F]
    [fKF : FiniteDimensional K F] [gKF : IsGalois K F] :
    ∀ (Q : Ideal (normalizationCommAlgCat A F)) [Q.IsMaximal],
      Function.Surjective (originalFiniteNormalizationTameMorphism A K F Q).hom'.toFun ∧
        (originalFiniteNormalizationTameMorphism A K F Q).hom'.ker =
          originalFiniteNormalizationWildSubgroup 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.