Module

CommAlgResidueRootsMap.lean

Nyll.EtaleFundamentalGroups.Inertia.CommAlgResidueRootsMap

3 declarations indexed from sourceView source ↗

Module documentation

Native residue actions on roots

Constructs local residue-root group objects and maps induced by quotient automorphisms. Identifies the native residue morphism with the localization roots action.

Imports8

Imported by2

def

commAlgResidueRootsGroup

EtaleFundamentalGroups.Inertia.commAlgResidueRootsGroup

Documentation

Roots in the actual local residue field, with their native group object.

Source context 5 commands

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

noncomputable section
namespace EtaleFundamentalGroups.Inertia
open SchemeTheory RamificationTheory.HilbertRamification
open scoped Pointwise
universe u v

Lean source · statement

def commAlgResidueRootsGroup
    {A : Type u} [CommRing A] (R : CommAlgCat.{v} A)
    (Q : Ideal R) [Q.IsMaximal] (n : ℕ) : GrpCat.{v}

def

commAlgResidueRootsMap

EtaleFundamentalGroups.Inertia.commAlgResidueRootsMap

Documentation

The given native quotient automorphism acts on roots through the fixed canonical quotient-to-local-residue equivalence.

Source context 5 commands

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

noncomputable section
namespace EtaleFundamentalGroups.Inertia
open SchemeTheory RamificationTheory.HilbertRamification
open scoped Pointwise
universe u v

Lean source · statement

def commAlgResidueRootsMap
    {A : Type u} [CommRing A] (R : CommAlgCat.{v} A)
    (Q : Ideal R) [Q.IsMaximal] (n : ℕ)
    (ρ : nativeAlgebraResidueAutomorphisms R Q) :
    GrpCat.Hom (commAlgResidueRootsGroup R Q n) (commAlgResidueRootsGroup R Q n)

theorem

nativeAlgebraResidueMorphism_rootsMap

EtaleFundamentalGroups.Inertia.nativeAlgebraResidueMorphism_rootsMap

Documentation

The standard localization action on roots is induced by the SAME native residue morphism. The equality uses its proved actual coefficient square.

Source context 5 commands

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

noncomputable section
namespace EtaleFundamentalGroups.Inertia
open SchemeTheory RamificationTheory.HilbertRamification
open scoped Pointwise
universe u v

Lean source · statement

theorem nativeAlgebraResidueMorphism_rootsMap
    {A : Type u} [CommRing A] (R : CommAlgCat.{v} A)
    (G : Type v) [Group G] [MulSemiringAction G R]
    (Q : Ideal R) [Q.IsMaximal]
    (hbase : ∀ g : G, (MulSemiringAction.toRingHom G R g).comp
      (commAlgCoefficientMap R) = commAlgCoefficientMap R)
    (n : ℕ) (d : nativeResidueStabilizer R G Q) :
    rootsGroupMap
        (MulSemiringAction.toRingHom (MulAction.stabilizer G Q) Q.ResidueField d) n =
      commAlgResidueRootsMap R Q n
        ((nativeAlgebraResidueMorphism R G Q hbase).hom'.toFun d)