Module

CommAlgCanonicalTameEquivariance.lean

Nyll.EtaleFundamentalGroups.Inertia.CommAlgCanonicalTameEquivariance

4 declarations indexed from sourceView source ↗

Module documentation

Equivariance of intrinsic canonical tame characters

Constructs the native residue action on canonical tame roots and identifies it with the localization action. Proves equivariance under stabilizer conjugation.

Imports8

Imported by4

def

commAlgCanonicalResidueRootsMap

L34 ↗

EtaleFundamentalGroups.Inertia.commAlgCanonicalResidueRootsMap

Documentation

The same quotient residue automorphism acts on the full intrinsic tame roots group through the fixed canonical quotient-residue equivalence.

Source context 5 commands

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

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

Lean source · statement

def commAlgCanonicalResidueRootsMap
    (A : Type u) [CommRing A] (B : CommAlgCat.{v} A) [IsDedekindDomain B]
    (Q : Ideal B) [Q.IsMaximal] (hQ : Q ≠ ⊥)
    (ρ : nativeAlgebraResidueAutomorphisms B Q) :
    GrpCat.Hom (commAlgIdealTameRootsGroup A B Q hQ)
      (commAlgIdealTameRootsGroup A B Q hQ)

def

commAlgStabilizerCanonicalRootsMap

L44 ↗

EtaleFundamentalGroups.Inertia.commAlgStabilizerCanonicalRootsMap

Documentation

The actual intrinsic stabilizer acts through its existing native residue morphism. No localized action is retained by this native map's interface.

Source context 5 commands

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

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

Lean source · statement

def commAlgStabilizerCanonicalRootsMap
    (A : Type u) [CommRing A] (B : CommAlgCat.{v} A) [IsDedekindDomain B]
    (Q : Ideal B) [Q.IsMaximal] (hQ : Q ≠ ⊥)
    (d : nativeResidueStabilizer B (B ≃ₐ[A] B) Q) :
    GrpCat.Hom (commAlgIdealTameRootsGroup A B Q hQ)
      (commAlgIdealTameRootsGroup A B Q hQ)

theorem

commAlgStabilizerCanonicalRootsMap_eq_standard

L55 ↗

EtaleFundamentalGroups.Inertia.commAlgStabilizerCanonicalRootsMap_eq_standard

Documentation

Its coefficient action is exactly the standard localization-residue action, by the proved square for the same native residue morphism.

Source context 5 commands

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

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

Lean source · statement

theorem commAlgStabilizerCanonicalRootsMap_eq_standard
    (A : Type u) [CommRing A] (B : CommAlgCat.{v} A) [IsDedekindDomain B]
    (Q : Ideal B) [Q.IsMaximal] (hQ : Q ≠ ⊥)
    (d : nativeResidueStabilizer B (B ≃ₐ[A] B) Q) :
    commAlgStabilizerCanonicalRootsMap A B Q hQ d =
      rootsGroupMap
        (MulSemiringAction.toRingHom (MulAction.stabilizer (B ≃ₐ[A] B) Q)
          Q.ResidueField d)
        (finiteIdealTameOrder B (B ≃ₐ[A] B) Q hQ)

theorem

commAlgCanonicalTameCharacter_conjugate

L70 ↗

EtaleFundamentalGroups.Inertia.commAlgCanonicalTameCharacter_conjugate

Documentation

The existing canonical character intertwines actual intrinsic conjugation with the same native stabilizer residue action on its roots.

Source context 5 commands

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

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

Lean source · statement

theorem commAlgCanonicalTameCharacter_conjugate
    (A : Type u) [CommRing A] (B : CommAlgCat.{v} A)
    [IsDedekindDomain B] [Finite (B ≃ₐ[A] B)]
    (Q : Ideal B) [Q.IsMaximal] (hQ : Q ≠ ⊥)
    (d : nativeResidueStabilizer B (B ≃ₐ[A] B) Q)
    (σ : commAlgIdealInertiaGroup A B Q) :
    (commAlgCanonicalTameCharacter A B Q hQ).toFun
        (commAlgIdealInertiaConjugate A B Q d σ) =
      (commAlgStabilizerCanonicalRootsMap A B Q hQ d).hom'.toFun
        ((commAlgCanonicalTameCharacter A B Q hQ).toFun σ)

Module documentation

Equivariance of intrinsic canonical tame characters

Declarations

commAlgCanonicalResidueRootsMap

commAlgStabilizerCanonicalRootsMap

commAlgStabilizerCanonicalRootsMap_eq_standard

commAlgCanonicalTameCharacter_conjugate