Nyll.EtaleFundamentalGroups.Inertia.OriginalFiniteFieldCanonicalTameEquivariance

theorem

originalFiniteFieldCanonicalTameMorphism_conjugate_stabilizer

EtaleFundamentalGroups.Inertia.originalFiniteFieldCanonicalTameMorphism_conjugate_stabilizer

Documentation

The original canonical character intertwines literal original conjugation with the root map of its actual intrinsic D-image. The original residue-automorphism group remains closed during this character comparison.

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 originalFiniteFieldCanonicalTameMorphism_conjugate_stabilizer
    (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)
    (σ : actualNormalizationInertiaGroup A K F Q) :
    let : IsDedekindDomain (normalizationCommAlgCat A F) :=
      integralClosure.isDedekindDomain A K F
    (originalFiniteFieldCanonicalTameMorphism A K F Q).hom'.toFun
        (originalFiniteNormalizationInertiaConjugate A K F Q d σ) =
      (commAlgStabilizerCanonicalRootsMap A (normalizationCommAlgCat A F) Q
        (originalFiniteNormalizationPrime_ne_bot A K F Q)
        ((originalFiniteNormalizationDecompositionMorphism A K F Q).hom'.toFun d)).hom'.toFun
          ((originalFiniteFieldCanonicalTameMorphism A K F Q).hom'.toFun σ) := by
  intro normalizationDedekind
  have : Finite (normalizationCommAlgCat A F ≃ₐ[A] normalizationCommAlgCat A F) :=
    nativeNormalization_aut_finite A K (CommAlgCat.of A F) (Field.toIsField F)
  have himage := originalFiniteNormalizationInertiaConjugate_map A K F Q d σ
  have hcharacter := commAlgCanonicalTameCharacter_conjugate A
    (normalizationCommAlgCat A F) Q (originalFiniteNormalizationPrime_ne_bot A K F Q)
    ((originalFiniteNormalizationDecompositionMorphism A K F Q).hom'.toFun d)
    ((originalFiniteNormalizationInertiaMorphism A K F Q).hom'.toFun σ)
  exact (originalFiniteFieldCanonicalTameMorphism_apply A K F Q
    (originalFiniteNormalizationInertiaConjugate A K F Q d σ)).trans
    ((congrArg
      (commAlgCanonicalTameCharacter A (normalizationCommAlgCat A F) Q
        (originalFiniteNormalizationPrime_ne_bot A K F Q)).toFun himage).trans
      (hcharacter.trans
        (congrArg
          (commAlgStabilizerCanonicalRootsMap A (normalizationCommAlgCat A F) Q
            (originalFiniteNormalizationPrime_ne_bot A K F Q)
            ((originalFiniteNormalizationDecompositionMorphism A K F Q).hom'.toFun d)).hom'.toFun
          (originalFiniteFieldCanonicalTameMorphism_apply A K F Q σ).symm)))

theorem

originalFiniteFieldCanonicalTameMorphism_decomposition_equivariant

L74 ↗

EtaleFundamentalGroups.Inertia.originalFiniteFieldCanonicalTameMorphism_decomposition_equivariant

Documentation

At the original finite Galois stage, the SAME canonical character satisfies χ(dσd⁻¹) = d̄(χ(σ)), where d̄ is the image under the SAME original normalizationResidueMorphism and acts by the fixed existing rootsGroupMap. No residue-action comparison or conjugation compatibility is an input.

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

theorem originalFiniteFieldCanonicalTameMorphism_decomposition_equivariant
    (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)
    (σ : actualNormalizationInertiaGroup A K F Q) :
    (originalFiniteFieldCanonicalTameMorphism A K F Q).hom'.toFun
        (originalFiniteNormalizationInertiaConjugate A K F Q d σ) =
      (originalFiniteNormalizationResidueRootsMap A K F Q
        ((normalizationResidueMorphism A K F Q).hom'.toFun d)).hom'.toFun
          ((originalFiniteFieldCanonicalTameMorphism A K F Q).hom'.toFun σ)

OriginalFiniteFieldCanonicalTameEquivariance.lean

Module documentation

Equivariance of original finite-field tame characters

originalFiniteFieldCanonicalTameMorphism_conjugate_stabilizer

originalFiniteFieldCanonicalTameMorphism_decomposition_equivariant

Module documentation

Equivariance of original finite-field tame characters

Declarations

originalFiniteFieldCanonicalTameMorphism_conjugate_stabilizer

originalFiniteFieldCanonicalTameMorphism_decomposition_equivariant