NYLL
Module

ResidualCharacterDetection.lean

Nyll.GaloisCohomology.ProP.ResidualCharacterDetection
2 declarations indexed from sourceView source ↗

Module documentation

Finite p-power characters detect residual abelianized conjugation

A changed continuous cyclic p-power character factors through the actual maximal pro-p residual quotient. Its change therefore detects conjugation on the topological abelianization of that quotient.

Imports11
Imported by2

Declarations

theorem

cyclicPrimePower_hasOpenNormalBasis

L33 ↗
ClassFieldTower.ProP.cyclicPrimePower_hasOpenNormalBasis
Source context 3 commands

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

namespace ClassFieldTower.ProP
open ProCGroups ProCGroups.ProC ProCGroups.Abelian
universe u
Lean source · statement
theorem cyclicPrimePower_hasOpenNormalBasis (p s : ℕ) [Fact p.Prime] :
    HasOpenNormalBasisInClass (FiniteGroupClass.pGroup p)
      (ULift.{u} (Multiplicative (ZMod (p ^ s))))
theorem

residualAbelianization_conjugation_ne_one_of_cyclicCharacter_ne

L48 ↗
ClassFieldTower.ProP.residualAbelianization_conjugation_ne_one_of_cyclicCharacter_ne
Documentation

A changed p-power character detects the actual conjugation automorphism of the abelianized pro-p residual quotient of a closed normal subgroup.

Source context 3 commands

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

namespace ClassFieldTower.ProP
open ProCGroups ProCGroups.ProC ProCGroups.Abelian
universe u
Lean source · statement
theorem residualAbelianization_conjugation_ne_one_of_cyclicCharacter_ne
    {G : Type u} [Group G] [TopologicalSpace G] [IsTopologicalGroup G]
    [CompactSpace G] [T2Space G] [TotallyDisconnectedSpace G]
    (p s : ℕ) [Fact p.Prime]
    (N : Subgroup G) [N.Normal] (hN : IsClosed (N : Set G)) (g : G)
    (χ : N →ₜ* Multiplicative (ZMod (p ^ s))) (x : N)
    (hχ : χ (MulAut.conjNormal g x) ≠ χ x) :
    (TopologicalAbelianization.congr
      (residualQuotientConjugationContinuousMulEquiv
        (FiniteGroupClass.pGroup_fullFormation p) N hN g)).toMulEquiv ≠ 1

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