Module

ActualTameCharacterEquivariance.lean

Nyll.EtaleFundamentalGroups.Inertia.ActualTameCharacterEquivariance

1 declaration indexed from sourceView source ↗

Module documentation

The SAME canonical global tame character is D-equivariant

The existing character and root limit retain their native group owners. Their proved scalar evaluation and action laws reduce this equality to the actual canonical finite coordinate equivariance, with no comparison premise.

Imports3

Imported by3

theorem

actualTameCharacter_conjugate

L25 ↗

EtaleFundamentalGroups.Inertia.actualTameCharacter_conjugate

Source context 3 commands

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

namespace EtaleFundamentalGroups.Inertia
open SchemeTheory
universe u v w

Lean source · statement

theorem actualTameCharacter_conjugate
    (A : Type u) (K : Type v) (L : Type w)
    [CommRing A] [IsDomain A] [IsDiscreteValuationRing 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]
    (d : (normalizationDecompositionGroup A K L Q).carrier)
    (σ : (actualNormalizationInertiaGroup A K L Q).carrier) :
    (actualTameCharacterMorphism A K L Q).hom'.toFun
        (originalFiniteNormalizationInertiaConjugate A K L Q d σ) =
      actualTameRootsAction_apply A K L Q d
        ((actualTameCharacterMorphism A K L Q).hom'.toFun σ)

Module documentation

The SAME canonical global tame character is D-equivariant

Declarations

actualTameCharacter_conjugate