Module

NormalizationSeparableResidueSequence.lean

Nyll.EtaleFundamentalGroups.Inertia.NormalizationSeparableResidueSequence

8 declarations indexed from sourceView source ↗

Module documentation

Original decomposition and inertia over the separable residue field

Normality of the actual normalization residue extension gives the existing restriction equivalence with its relative separable closure. Composing this actual equivalence with the original residue action preserves its surjectivity and its literal kernel, the original inertia included in decomposition. No discrete valuation or algebraically closed residue hypothesis is used.

Imports6

Imported by2

def

separableResidueIsoOfNormal

L34 ↗

EtaleFundamentalGroups.Inertia.separableResidueIsoOfNormal

Source context 5 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

Lean source · full declaration

def separableResidueIsoOfNormal (k : Type u) [Field k] (E : Bundled Field.{w})
    (a : Algebra k E.α) (h : let := a; Normal k E.α) :
    nativeFieldAutomorphisms k E a ≅ nativeSeparableResidueGroup k E a := by
  let := a
  have : Normal k E.α := h
  exact (separableClosureAutEquiv k E.α).toGrpIso

theorem

separableResidueIsoOfNormal_commutes

L41 ↗

EtaleFundamentalGroups.Inertia.separableResidueIsoOfNormal_commutes

Source context 5 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

Lean source · full declaration

theorem separableResidueIsoOfNormal_commutes
    (k : Type u) [Field k] (E : Bundled Field.{w}) (a : Algebra k E.α)
    (h : let := a; Normal k E.α)
    (σ : (nativeFieldAutomorphisms k E a).carrier)
    (z : (nativeSeparableResidueField k E a).α) :
    nativeSeparableResidueActionScalar k E a
        ((separableResidueIsoOfNormal k E a h).hom.hom'.toFun σ) z =
      nativeFieldResidueActionScalar k E a σ (nativeSeparableResidueScalar k E a z) := by
  let := a
  have : Normal k E.α := h
  exact separableClosure_restrictNormal_coefficient k E.α (show E.α ≃ₐ[k] E.α from σ) z

def

normalizationSeparableResidueIso

L62 ↗

EtaleFundamentalGroups.Inertia.normalizationSeparableResidueIso

Documentation

Restriction identifies the original literal residue automorphism group with the Galois group of its actual separable part. The required normality is proved from the original normalization data.

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) (L : Type w)
  [CommRing A] [IsDomain A] [IsIntegrallyClosed A] [IsLocalRing 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).carrier) [Q.IsMaximal]

Lean source · statement

def normalizationSeparableResidueIso :
    normalizationResidueAutomorphisms A L Q ≅ normalizationResidueSeparableGroup A L Q

theorem

normalizationSeparableResidueIso_commutes

L70 ↗

EtaleFundamentalGroups.Inertia.normalizationSeparableResidueIso_commutes

Documentation

The residue restriction equivalence preserves the literal coefficient inclusion into the original normalization quotient.

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) (L : Type w)
  [CommRing A] [IsDomain A] [IsIntegrallyClosed A] [IsLocalRing 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).carrier) [Q.IsMaximal]

Lean source · statement

theorem normalizationSeparableResidueIso_commutes
    (σ : (normalizationResidueAutomorphisms A L Q).carrier)
    (z : (nativeSeparableResidueField (IsLocalRing.ResidueField A)
      (normalizationResidueFieldObject A L Q) (normalizationResidueFieldAlgebra A L Q)).α) :
    nativeSeparableResidueActionScalar (IsLocalRing.ResidueField A)
        (normalizationResidueFieldObject A L Q) (normalizationResidueFieldAlgebra A L Q)
        ((normalizationSeparableResidueIso A K L Q).hom.hom'.toFun σ) z =
      normalizationResidueActionScalar A L Q σ
        (nativeSeparableResidueScalar (IsLocalRing.ResidueField A)
          (normalizationResidueFieldObject A L Q) (normalizationResidueFieldAlgebra A L Q) z)

def

normalizationSeparableResidueMorphism

L90 ↗

EtaleFundamentalGroups.Inertia.normalizationSeparableResidueMorphism

Documentation

The original decomposition action restricted to the actual separable residue field.

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) (L : Type w)
  [CommRing A] [IsDomain A] [IsIntegrallyClosed A] [IsLocalRing 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).carrier) [Q.IsMaximal]

Lean source · statement

def normalizationSeparableResidueMorphism :
    GrpCat.Hom (normalizationDecompositionGroup A K L Q)
      (normalizationResidueSeparableGroup A L Q)

theorem

normalizationSeparableResidueMorphism_surjective

L97 ↗

EtaleFundamentalGroups.Inertia.normalizationSeparableResidueMorphism_surjective

Documentation

Every automorphism of the actual separable residue field is induced by an element of the original decomposition subgroup.

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) (L : Type w)
  [CommRing A] [IsDomain A] [IsIntegrallyClosed A] [IsLocalRing 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).carrier) [Q.IsMaximal]

Lean source · statement

theorem normalizationSeparableResidueMorphism_surjective :
    Function.Surjective (normalizationSeparableResidueMorphism A K L Q).hom'.toFun

theorem

normalizationSeparableResidueMorphism_ker

L104 ↗

EtaleFundamentalGroups.Inertia.normalizationSeparableResidueMorphism_ker

Documentation

The actual separable-residue map has the same literal kernel in D as the original full residue action.

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) (L : Type w)
  [CommRing A] [IsDomain A] [IsIntegrallyClosed A] [IsLocalRing 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).carrier) [Q.IsMaximal]

Lean source · statement

theorem normalizationSeparableResidueMorphism_ker :
    (normalizationSeparableResidueMorphism A K L Q).hom'.ker =
      (actualNormalizationInertiaToDecomposition A K L Q).range

theorem

normalizationSeparableResidue_exact

L113 ↗

EtaleFundamentalGroups.Inertia.normalizationSeparableResidue_exact

Documentation

The exact original I-to-D-to-separable-residue sequence over an arbitrary normal local domain, with the same original inclusion and residue action.

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) (L : Type w)
  [CommRing A] [IsDomain A] [IsIntegrallyClosed A] [IsLocalRing 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).carrier) [Q.IsMaximal]

Lean source · statement

theorem normalizationSeparableResidue_exact :
    Function.Injective (actualNormalizationInertiaToDecomposition A K L Q).toFun ∧
      Function.Surjective (normalizationSeparableResidueMorphism A K L Q).hom'.toFun ∧
        (normalizationSeparableResidueMorphism A K L Q).hom'.ker =
          (actualNormalizationInertiaToDecomposition A K L Q).range

Module documentation

Original decomposition and inertia over the separable residue field

Declarations