Module

PadicPrimaryQuotient.lean

Nyll.GaloisCohomology.ProfiniteIntegers.PadicPrimaryQuotient

4 declarations indexed from sourceView source ↗

Module documentation

P-adic characters factor through the maximal pro-p quotient

Imports3

Imported by3

theorem

finite_pGroup_basis

L17 ↗

ProCGroups.ProC.finite_pGroup_basis

Source context 2 commands

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

namespace ProCGroups.ProC
universe u

Lean source · statement

theorem finite_pGroup_basis
    {p : ℕ} [Fact p.Prime]
    {B : Type u} [Group B] [TopologicalSpace B] [IsTopologicalGroup B]
    [Finite B] [DiscreteTopology B] (hB : IsPGroup p B) :
    HasOpenNormalBasisInClass (FiniteGroupClass.pGroup p) B

theorem

proPResidualCore_le_ker_padicCharacter

L28 ↗

ProCGroups.ProC.proPResidualCore_le_ker_padicCharacter

Documentation

Every continuous p-adic character kills the pro-p residual core.

Source context 2 commands

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

namespace ProCGroups.ProC
universe u

Lean source · statement

theorem proPResidualCore_le_ker_padicCharacter
    {p : ℕ} [Fact p.Prime]
    {A : Type u} [Group A] [TopologicalSpace A] [IsTopologicalGroup A]
    [CompactSpace A] (f : A →ₜ* Multiplicative (PadicInt p)) :
    proCResidualCore (FiniteGroupClass.pGroup p) A ≤ f.toMonoidHom.ker

def

liftPadicCharacter

L68 ↗

ProCGroups.ProC.liftPadicCharacter

Documentation

The induced p-adic character on the maximal pro-p quotient.

Source context 2 commands

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

namespace ProCGroups.ProC
universe u

Lean source · statement

def liftPadicCharacter
    {p : ℕ} [Fact p.Prime]
    {A : Type u} [Group A] [TopologicalSpace A] [IsTopologicalGroup A]
    [CompactSpace A] (f : A →ₜ* Multiplicative (PadicInt p)) :
    A ⧸ proCResidualCore (FiniteGroupClass.pGroup p) A →ₜ* Multiplicative (PadicInt p)

theorem

liftPadicCharacter_mk

L75 ↗

ProCGroups.ProC.liftPadicCharacter_mk

Source context 2 commands

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

namespace ProCGroups.ProC
universe u

Lean source · statement

theorem liftPadicCharacter_mk
    {p : ℕ} [Fact p.Prime]
    {A : Type u} [Group A] [TopologicalSpace A] [IsTopologicalGroup A]
    [CompactSpace A] (f : A →ₜ* Multiplicative (PadicInt p)) (a : A) :
    liftPadicCharacter f (QuotientGroup.mk' _ a) = f a

Module documentation

P-adic characters factor through the maximal pro-p quotient

Declarations

finite_pGroup_basis

proPResidualCore_le_ker_padicCharacter

liftPadicCharacter

liftPadicCharacter_mk