Module

NormalizationResidueSequence.lean

Nyll.SchemeTheory.RingTheory.Ramification.NormalizationResidueSequence

9 declarations indexed from sourceView source ↗

Module documentation

The actual normalization residue sequence

The groups and homomorphism below are the native stabilizer and the literal quotient-algebra automorphism group of the actual integral closure. The possibly infinite Galois action has the prescribed normalization action. Normality supplies coefficient descent and the Krull topology supplies the open stabilizers; the compact residue construction proves surjectivity. The kernel included into the original Galois group is exactly inertia.

Imports5

Imported by15

def

normalizationDecompositionGroup

L35 ↗

EtaleFundamentalGroups.Inertia.normalizationDecompositionGroup

Documentation

The actual decomposition group of the prime of the normalization.

Source context 5 commands

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

noncomputable section
namespace EtaleFundamentalGroups.Inertia
open SchemeTheory CategoryTheory
universe u v w
attribute [local instance] normalizationCommAlgGaloisAction

Lean source · statement

def normalizationDecompositionGroup
    (A : Type u) (K : Type v) (L : Type w)
    [CommRing A] [Field K] [Field L]
    [Algebra A K] [IsFractionRing A K] [Algebra K L] [Algebra A L]
    [IsScalarTower A K L] [Algebra.IsAlgebraic K L]
    (Q : Ideal (normalizationCommAlgCat A L)) : GrpCat.{w}

def

normalizationResidueAutomorphisms

L44 ↗

EtaleFundamentalGroups.Inertia.normalizationResidueAutomorphisms

Documentation

The literal residue automorphism group over the contracted base prime.

Source context 5 commands

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

noncomputable section
namespace EtaleFundamentalGroups.Inertia
open SchemeTheory CategoryTheory
universe u v w
attribute [local instance] normalizationCommAlgGaloisAction

Lean source · statement

def normalizationResidueAutomorphisms
    (A : Type u) (L : Type w) [CommRing A] [CommRing L] [Algebra A L]
    (Q : Ideal (normalizationCommAlgCat A L)) : GrpCat.{w}

def

normalizationDecompositionInclusion

L50 ↗

EtaleFundamentalGroups.Inertia.normalizationDecompositionInclusion

Documentation

The actual decomposition-group inclusion in the original Galois group.

Source context 5 commands

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

noncomputable section
namespace EtaleFundamentalGroups.Inertia
open SchemeTheory CategoryTheory
universe u v w
attribute [local instance] normalizationCommAlgGaloisAction

Lean source · statement

def normalizationDecompositionInclusion
    (A : Type u) (K : Type v) (L : Type w)
    [CommRing A] [Field K] [Field L]
    [Algebra A K] [IsFractionRing A K] [Algebra K L] [Algebra A L]
    [IsScalarTower A K L] [Algebra.IsAlgebraic K L]
    (Q : Ideal (normalizationCommAlgCat A L)) :
    normalizationDecompositionGroup A K L Q →* Gal(L/K)

def

normalizationResidueMorphism

L60 ↗

EtaleFundamentalGroups.Inertia.normalizationResidueMorphism

Documentation

The actual native stabilizer homomorphism for the original normalization.

Source context 5 commands

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

noncomputable section
namespace EtaleFundamentalGroups.Inertia
open SchemeTheory CategoryTheory
universe u v w
attribute [local instance] normalizationCommAlgGaloisAction

Lean source · statement

def normalizationResidueMorphism
    (A : Type u) (K : Type v) (L : Type w)
    [CommRing A] [Field K] [Field L]
    [Algebra A K] [IsFractionRing A K] [Algebra K L] [Algebra A L]
    [IsScalarTower A K L] [IsGalois K L]
    (Q : Ideal (normalizationCommAlgCat A L)) :
    GrpCat.Hom (normalizationDecompositionGroup A K L Q)
      (normalizationResidueAutomorphisms A L Q)

theorem

normalizationResidueMorphism_epi

L72 ↗

EtaleFundamentalGroups.Inertia.normalizationResidueMorphism_epi

Documentation

Normality and the actual infinite Galois action prove the residue map epic.

Source context 5 commands

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

noncomputable section
namespace EtaleFundamentalGroups.Inertia
open SchemeTheory CategoryTheory
universe u v w
attribute [local instance] normalizationCommAlgGaloisAction

Lean source · statement

theorem normalizationResidueMorphism_epi
    (A : Type u) (K : Type v) (L : Type w)
    [CommRing A] [IsIntegrallyClosed A] [Field K] [Field L]
    [Algebra A K] [IsFractionRing A K] [Algebra K L] [Algebra A L]
    [IsScalarTower A K L] [IsGalois K L]
    (Q : Ideal (normalizationCommAlgCat A L)) [Q.IsPrime] :
    Epi (C := GrpCat.{w}) (X := normalizationDecompositionGroup A K L Q)
      (Y := normalizationResidueAutomorphisms A L Q)
      (normalizationResidueMorphism A K L Q)

theorem

normalizationResidueMorphism_surjective

L88 ↗

EtaleFundamentalGroups.Inertia.normalizationResidueMorphism_surjective

Documentation

The original decomposition group surjects onto the actual residue algebra automorphisms, with no finite-extension or Henselian hypothesis.

Source context 5 commands

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

noncomputable section
namespace EtaleFundamentalGroups.Inertia
open SchemeTheory CategoryTheory
universe u v w
attribute [local instance] normalizationCommAlgGaloisAction

Lean source · statement

theorem normalizationResidueMorphism_surjective
    (A : Type u) (K : Type v) (L : Type w)
    [CommRing A] [IsIntegrallyClosed A] [Field K] [Field L]
    [Algebra A K] [IsFractionRing A K] [Algebra K L] [Algebra A L]
    [IsScalarTower A K L] [IsGalois K L]
    (Q : Ideal (normalizationCommAlgCat A L)) [Q.IsPrime] :
    Function.Surjective (normalizationResidueMorphism A K L Q).hom'.toFun

def

normalizationResidueKernelImage

L102 ↗

EtaleFundamentalGroups.Inertia.normalizationResidueKernelImage

Documentation

The actual residue-map kernel, mapped into the original Galois group.

Source context 5 commands

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

noncomputable section
namespace EtaleFundamentalGroups.Inertia
open SchemeTheory CategoryTheory
universe u v w
attribute [local instance] normalizationCommAlgGaloisAction

Lean source · statement

def normalizationResidueKernelImage
    (A : Type u) (K : Type v) (L : Type w)
    [CommRing A] [Field K] [Field L]
    [Algebra A K] [IsFractionRing A K] [Algebra K L] [Algebra A L]
    [IsScalarTower A K L] [IsGalois K L]
    (Q : Ideal (normalizationCommAlgCat A L)) : Subgroup Gal(L/K)

theorem

normalizationResidueKernelImage_eq_inertia

L112 ↗

EtaleFundamentalGroups.Inertia.normalizationResidueKernelImage_eq_inertia

Documentation

The computed kernel image is the native inertia group at the original prime.

Source context 5 commands

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

noncomputable section
namespace EtaleFundamentalGroups.Inertia
open SchemeTheory CategoryTheory
universe u v w
attribute [local instance] normalizationCommAlgGaloisAction

Lean source · statement

theorem normalizationResidueKernelImage_eq_inertia
    (A : Type u) (K : Type v) (L : Type w)
    [CommRing A] [Field K] [Field L]
    [Algebra A K] [IsFractionRing A K] [Algebra K L] [Algebra A L]
    [IsScalarTower A K L] [IsGalois K L]
    (Q : Ideal (normalizationCommAlgCat A L)) :
    normalizationResidueKernelImage A K L Q = Q.inertia Gal(L/K)

theorem

normalizationResidueMorphism_map_ker

L124 ↗

EtaleFundamentalGroups.Inertia.normalizationResidueMorphism_map_ker

Documentation

The kernel of the literal residue map, included into the original Galois group, is exactly the original inertia subgroup.

Source context 5 commands

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

noncomputable section
namespace EtaleFundamentalGroups.Inertia
open SchemeTheory CategoryTheory
universe u v w
attribute [local instance] normalizationCommAlgGaloisAction

Lean source · statement

theorem normalizationResidueMorphism_map_ker
    (A : Type u) (K : Type v) (L : Type w)
    [CommRing A] [Field K] [Field L]
    [Algebra A K] [IsFractionRing A K] [Algebra K L] [Algebra A L]
    [IsScalarTower A K L] [IsGalois K L]
    (Q : Ideal (normalizationCommAlgCat A L)) :
    (normalizationResidueMorphism A K L Q).hom'.ker.map
      (normalizationDecompositionInclusion A K L Q) = Q.inertia Gal(L/K)

Module documentation

The actual normalization residue sequence

Declarations