NYLL
Module

NormalizationAbsoluteResidueSequence.lean

Nyll.EtaleFundamentalGroups.Inertia.NormalizationAbsoluteResidueSequence
7 declarations indexed from sourceView source ↗

Module documentation

The absolute separable-residue exact sequence

Constructs the decomposition-group morphism to the separable residue Galois group and proves surjectivity. Identifies its kernel image with original ideal inertia to obtain the absolute residue exact sequence.

Imports2
Imported by4

Declarations

def

normalizationAbsoluteResidueMorphism

L36 ↗
EtaleFundamentalGroups.Inertia.normalizationAbsoluteResidueMorphism
Documentation

The original decomposition residue map, followed by its actual restriction to the separable residue closure.

Source context 6 commands

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

noncomputable section
namespace EtaleFundamentalGroups.Inertia
open CategoryTheory SchemeTheory
universe u v w
attribute [local instance] normalizationCommAlgGaloisAction
variable (A : Type u) (K : Type v) (Ω : Type w)
  [CommRing A] [IsDomain A] [IsDiscreteValuationRing A]
  [Field K] [Field Ω] [Algebra A K] [IsFractionRing A K]
  [Algebra K Ω] [Algebra A Ω] [IsScalarTower A K Ω] [IsSepClosure K Ω]
  (Q : Ideal (normalizationCommAlgCat A Ω)) [Q.IsMaximal]
Lean source · statement
def normalizationAbsoluteResidueMorphism :
    GrpCat.Hom (normalizationDecompositionGroup A K Ω Q)
      (normalizationResidueSeparableGroup A Ω Q)
theorem

normalizationAbsoluteResidueMorphism_surjective

L43 ↗
EtaleFundamentalGroups.Inertia.normalizationAbsoluteResidueMorphism_surjective
Documentation

The actual original residue map onto the separable residue Galois group is surjective, including inseparable residue extensions.

Source context 6 commands

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

noncomputable section
namespace EtaleFundamentalGroups.Inertia
open CategoryTheory SchemeTheory
universe u v w
attribute [local instance] normalizationCommAlgGaloisAction
variable (A : Type u) (K : Type v) (Ω : Type w)
  [CommRing A] [IsDomain A] [IsDiscreteValuationRing A]
  [Field K] [Field Ω] [Algebra A K] [IsFractionRing A K]
  [Algebra K Ω] [Algebra A Ω] [IsScalarTower A K Ω] [IsSepClosure K Ω]
  (Q : Ideal (normalizationCommAlgCat A Ω)) [Q.IsMaximal]
Lean source · statement
theorem normalizationAbsoluteResidueMorphism_surjective :
    Function.Surjective (normalizationAbsoluteResidueMorphism A K Ω Q).hom'.toFun
theorem

normalizationAbsoluteResidueMorphism_ker

L50 ↗
EtaleFundamentalGroups.Inertia.normalizationAbsoluteResidueMorphism_ker
Documentation

The actual separable-residue map has exactly the same subgroup kernel inside the original decomposition group.

Source context 6 commands

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

noncomputable section
namespace EtaleFundamentalGroups.Inertia
open CategoryTheory SchemeTheory
universe u v w
attribute [local instance] normalizationCommAlgGaloisAction
variable (A : Type u) (K : Type v) (Ω : Type w)
  [CommRing A] [IsDomain A] [IsDiscreteValuationRing A]
  [Field K] [Field Ω] [Algebra A K] [IsFractionRing A K]
  [Algebra K Ω] [Algebra A Ω] [IsScalarTower A K Ω] [IsSepClosure K Ω]
  (Q : Ideal (normalizationCommAlgCat A Ω)) [Q.IsMaximal]
Lean source · statement
theorem normalizationAbsoluteResidueMorphism_ker :
    (normalizationAbsoluteResidueMorphism A K Ω Q).hom'.ker =
      (normalizationResidueMorphism A K Ω Q).hom'.ker
def

normalizationAbsoluteResidueKernelImage

L58 ↗
EtaleFundamentalGroups.Inertia.normalizationAbsoluteResidueKernelImage
Documentation

The actual kernel image in the original absolute Galois group, computed before its identification with ideal inertia.

Source context 6 commands

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

noncomputable section
namespace EtaleFundamentalGroups.Inertia
open CategoryTheory SchemeTheory
universe u v w
attribute [local instance] normalizationCommAlgGaloisAction
variable (A : Type u) (K : Type v) (Ω : Type w)
  [CommRing A] [IsDomain A] [IsDiscreteValuationRing A]
  [Field K] [Field Ω] [Algebra A K] [IsFractionRing A K]
  [Algebra K Ω] [Algebra A Ω] [IsScalarTower A K Ω] [IsSepClosure K Ω]
  (Q : Ideal (normalizationCommAlgCat A Ω)) [Q.IsMaximal]
Lean source · statement
def normalizationAbsoluteResidueKernelImage : Subgroup Gal(Ω/K)
theorem

normalizationAbsoluteResidueKernelImage_eq

L64 ↗
EtaleFundamentalGroups.Inertia.normalizationAbsoluteResidueKernelImage_eq
Documentation

Restricting the actual residue automorphisms changes neither this computed kernel image nor its embedding into the original Galois group.

Source context 6 commands

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

noncomputable section
namespace EtaleFundamentalGroups.Inertia
open CategoryTheory SchemeTheory
universe u v w
attribute [local instance] normalizationCommAlgGaloisAction
variable (A : Type u) (K : Type v) (Ω : Type w)
  [CommRing A] [IsDomain A] [IsDiscreteValuationRing A]
  [Field K] [Field Ω] [Algebra A K] [IsFractionRing A K]
  [Algebra K Ω] [Algebra A Ω] [IsScalarTower A K Ω] [IsSepClosure K Ω]
  (Q : Ideal (normalizationCommAlgCat A Ω)) [Q.IsMaximal]
Lean source · statement
theorem normalizationAbsoluteResidueKernelImage_eq :
    normalizationAbsoluteResidueKernelImage A K Ω Q = normalizationResidueKernelImage A K Ω Q
theorem

normalizationAbsoluteResidueMorphism_map_ker

L74 ↗
EtaleFundamentalGroups.Inertia.normalizationAbsoluteResidueMorphism_map_ker
Documentation

The original separable-residue kernel, included in the actual absolute Galois group, is the original ideal inertia group.

Source context 6 commands

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

noncomputable section
namespace EtaleFundamentalGroups.Inertia
open CategoryTheory SchemeTheory
universe u v w
attribute [local instance] normalizationCommAlgGaloisAction
variable (A : Type u) (K : Type v) (Ω : Type w)
  [CommRing A] [IsDomain A] [IsDiscreteValuationRing A]
  [Field K] [Field Ω] [Algebra A K] [IsFractionRing A K]
  [Algebra K Ω] [Algebra A Ω] [IsScalarTower A K Ω] [IsSepClosure K Ω]
  (Q : Ideal (normalizationCommAlgCat A Ω)) [Q.IsMaximal]
Lean source · statement
theorem normalizationAbsoluteResidueMorphism_map_ker :
    (normalizationAbsoluteResidueMorphism A K Ω Q).hom'.ker.map
        (normalizationDecompositionInclusion A K Ω Q) = Q.inertia Gal(Ω/K)
theorem

normalizationAbsoluteResidue_exact

L84 ↗
EtaleFundamentalGroups.Inertia.normalizationAbsoluteResidue_exact
Documentation

The original absolute residue exact sequence has the same D, I and residue action as the constructed normalization sequence. Its target is the actual Galois group of the separable residue closure.

Source context 6 commands

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

noncomputable section
namespace EtaleFundamentalGroups.Inertia
open CategoryTheory SchemeTheory
universe u v w
attribute [local instance] normalizationCommAlgGaloisAction
variable (A : Type u) (K : Type v) (Ω : Type w)
  [CommRing A] [IsDomain A] [IsDiscreteValuationRing A]
  [Field K] [Field Ω] [Algebra A K] [IsFractionRing A K]
  [Algebra K Ω] [Algebra A Ω] [IsScalarTower A K Ω] [IsSepClosure K Ω]
  (Q : Ideal (normalizationCommAlgCat A Ω)) [Q.IsMaximal]
Lean source · statement
theorem normalizationAbsoluteResidue_exact :
    Function.Surjective (normalizationAbsoluteResidueMorphism A K Ω Q).hom'.toFun ∧
      (normalizationAbsoluteResidueMorphism A K Ω Q).hom'.ker.map
        (normalizationDecompositionInclusion A K Ω Q) = Q.inertia Gal(Ω/K)

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