NYLL
Module

OriginalFiniteCanonicalRootsAction.lean

Nyll.EtaleFundamentalGroups.Inertia.OriginalFiniteCanonicalRootsAction
2 declarations indexed from sourceView source ↗

Module documentation

Original residue actions on finite tame roots

Constructs the root map induced by an original residue automorphism and identifies it with the action of the corresponding normalization stabilizer image.

Imports6
Imported by2

Declarations

def

originalFiniteNormalizationResidueRootsMap

L31 ↗
EtaleFundamentalGroups.Inertia.originalFiniteNormalizationResidueRootsMap
Documentation

The given element of the original residue target acts on the full finite tame roots through the fixed native residue roots map.

Source context 4 commands

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

noncomputable section
namespace EtaleFundamentalGroups.Inertia
open SchemeTheory
universe u v w
Lean source · statement
def originalFiniteNormalizationResidueRootsMap
    (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]
    (ρ : normalizationResidueAutomorphisms A F Q) :
    GrpCat.Hom (originalFiniteNormalizationTameRootsGroup A K F Q)
      (originalFiniteNormalizationTameRootsGroup A K F Q)
theorem

originalFiniteNormalizationStabilizerRootsMap_eq_residue

L49 ↗
EtaleFundamentalGroups.Inertia.originalFiniteNormalizationStabilizerRootsMap_eq_residue
Documentation

The actual normalization D-image and the SAME original residue morphism induce identical root maps. The equality is supplied by the proved coefficient comparison, before an original inertia element is introduced.

Source context 4 commands

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

noncomputable section
namespace EtaleFundamentalGroups.Inertia
open SchemeTheory
universe u v w
Lean source · full declaration
theorem originalFiniteNormalizationStabilizerRootsMap_eq_residue
    (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]
    (d : normalizationDecompositionGroup A K F Q) :
    let : IsDedekindDomain (normalizationCommAlgCat A F) :=
      integralClosure.isDedekindDomain A K F
    commAlgStabilizerCanonicalRootsMap A (normalizationCommAlgCat A F) Q
        (originalFiniteNormalizationPrime_ne_bot A K F Q)
        ((originalFiniteNormalizationDecompositionMorphism A K F Q).hom'.toFun d) =
      originalFiniteNormalizationResidueRootsMap A K F Q
        ((normalizationResidueMorphism A K F Q).hom'.toFun d) := by
  intro normalizationDedekind
  exact congrArg
    (commAlgCanonicalResidueRootsMap A (normalizationCommAlgCat A F) Q
      (originalFiniteNormalizationPrime_ne_bot A K F Q))
    (originalFiniteNormalizationDecompositionMorphism_residue A K F Q d).symm

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