Module

AbelianModPower.lean

Nyll.ProCGroups.Abelian.AbelianModPower

10 declarations indexed from sourceView source ↗

Module documentation

Abelianization modulo a power

For a topological group G, first quotient by the closed commutator subgroup, then by the subgroup of q-th powers. Continuous homomorphisms descend to this quotient, and maps to commutative groups of exponent dividing q factor through it.

Imports4

Nyll.ProCGroups.Abelian.TopologicalAbelianization
Nyll.ProCGroups.Topologies.QuotientMaps
Mathlib.GroupTheory.QuotientGroup.Basic
Mathlib.Topology.Algebra.Group.Quotient

Imported by11

abbrev

abelianModPower

L26 ↗

ProCGroups.Abelian.abelianModPower

Documentation

The abelianization of a topological group modulo its q-th powers.

Source context 2 commands

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

namespace ProCGroups.Abelian
universe u v

Lean source · statement

abbrev abelianModPower
    (G : Type u) [TopologicalSpace G] [Group G] [IsTopologicalGroup G]
    (q : ℕ) : Type u

def

abelianModPowerMap

L34 ↗

ProCGroups.Abelian.abelianModPowerMap

Documentation

A continuous homomorphism induces a homomorphism of abelianizations modulo q-th powers.

Source context 2 commands

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

namespace ProCGroups.Abelian
universe u v

Lean source · statement

def abelianModPowerMap
    {G : Type u} [TopologicalSpace G] [Group G] [IsTopologicalGroup G]
    {H : Type v} [TopologicalSpace H] [Group H] [IsTopologicalGroup H]
    (q : ℕ) (f : G →ₜ* H) :
    abelianModPower G q →ₜ* abelianModPower H q

theorem

abelianModPowerMap_mk

L59 ↗

ProCGroups.Abelian.abelianModPowerMap_mk

Documentation

The induced map on abelianizations modulo powers sends the class of a representative to the class of its image.

Source context 2 commands

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

namespace ProCGroups.Abelian
universe u v

Lean source · statement

theorem abelianModPowerMap_mk
    {G : Type u} [TopologicalSpace G] [Group G] [IsTopologicalGroup G]
    {H : Type v} [TopologicalSpace H] [Group H] [IsTopologicalGroup H]
    (q : ℕ) (f : G →ₜ* H) (g : G) :
    abelianModPowerMap q f
      (QuotientGroup.mk' (powMonoidHom (α := TopologicalAbelianization G) q).range
        (TopologicalAbelianization.mk G g)) =
      QuotientGroup.mk' (powMonoidHom (α := TopologicalAbelianization H) q).range
        (TopologicalAbelianization.mk H (f g))

def

abelianModPowerLift

L72 ↗

ProCGroups.Abelian.abelianModPowerLift

Documentation

A continuous homomorphism to a commutative group of exponent dividing q factors through the topological abelianization modulo q-th powers.

Source context 2 commands

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

namespace ProCGroups.Abelian
universe u v

Lean source · statement

def abelianModPowerLift
    {G : Type u} [TopologicalSpace G] [Group G] [IsTopologicalGroup G]
    {A : Type v} [TopologicalSpace A] [CommGroup A] [T1Space A]
    (q : ℕ) (f : G →ₜ* A) (hpow : ∀ a : A, a ^ q = 1) :
    abelianModPower G q →ₜ* A

theorem

abelianModPowerLift_mk

L87 ↗

ProCGroups.Abelian.abelianModPowerLift_mk

Documentation

The factorization through Gᵃᵇ/q evaluates to the original map on representatives.

Source context 2 commands

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

namespace ProCGroups.Abelian
universe u v

Lean source · statement

theorem abelianModPowerLift_mk
    {G : Type u} [TopologicalSpace G] [Group G] [IsTopologicalGroup G]
    {A : Type v} [TopologicalSpace A] [CommGroup A] [T1Space A]
    (q : ℕ) (f : G →ₜ* A) (hpow : ∀ a : A, a ^ q = 1) (g : G) :
    abelianModPowerLift q f hpow
      (QuotientGroup.mk' (powMonoidHom (α := TopologicalAbelianization G) q).range
        (TopologicalAbelianization.mk G g)) = f g

theorem

abelianModPowerLift_surjective

L98 ↗

ProCGroups.Abelian.abelianModPowerLift_surjective

Documentation

Surjectivity is preserved by the factorization through Gᵃᵇ/q.

Source context 2 commands

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

namespace ProCGroups.Abelian
universe u v

Lean source · statement

theorem abelianModPowerLift_surjective
    {G : Type u} [TopologicalSpace G] [Group G] [IsTopologicalGroup G]
    {A : Type v} [TopologicalSpace A] [CommGroup A] [T1Space A]
    (q : ℕ) (f : G →ₜ* A) (hpow : ∀ a : A, a ^ q = 1)
    (hf : Function.Surjective f) :
    Function.Surjective (abelianModPowerLift q f hpow)

def

abelianModPowerMk

L116 ↗

ProCGroups.Abelian.abelianModPowerMk

Documentation

The canonical continuous quotient map to abelianization modulo powers.

Source context 3 commands

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

namespace ProCGroups.Abelian
universe u v
variable {G H J : Type*}
  [TopologicalSpace G] [Group G] [IsTopologicalGroup G]
  [TopologicalSpace H] [Group H] [IsTopologicalGroup H]
  [TopologicalSpace J] [Group J] [IsTopologicalGroup J]

Lean source · statement

def abelianModPowerMk (G : Type*) [TopologicalSpace G] [Group G]
    [IsTopologicalGroup G] (q : ℕ) : G →ₜ* abelianModPower G q

theorem

abelianModPowerMk_surjective

L125 ↗

ProCGroups.Abelian.abelianModPowerMk_surjective

Documentation

Every class modulo commutators and powers has a group representative.

Source context 3 commands

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

namespace ProCGroups.Abelian
universe u v
variable {G H J : Type*}
  [TopologicalSpace G] [Group G] [IsTopologicalGroup G]
  [TopologicalSpace H] [Group H] [IsTopologicalGroup H]
  [TopologicalSpace J] [Group J] [IsTopologicalGroup J]

Lean source · statement

theorem abelianModPowerMk_surjective (q : ℕ) :
    Function.Surjective (abelianModPowerMk G q)

theorem

abelianModPowerMap_comp

L130 ↗

ProCGroups.Abelian.abelianModPowerMap_comp

Documentation

Passage to abelianizations modulo powers respects composition.

Source context 3 commands

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

namespace ProCGroups.Abelian
universe u v
variable {G H J : Type*}
  [TopologicalSpace G] [Group G] [IsTopologicalGroup G]
  [TopologicalSpace H] [Group H] [IsTopologicalGroup H]
  [TopologicalSpace J] [Group J] [IsTopologicalGroup J]

Lean source · statement

theorem abelianModPowerMap_comp (q : ℕ) (f : G →ₜ* H) (g : H →ₜ* J) :
    abelianModPowerMap q (g.comp f) =
      (abelianModPowerMap q g).comp (abelianModPowerMap q f)

theorem

abelianModPowerMap_mk_apply

L138 ↗

ProCGroups.Abelian.abelianModPowerMap_mk_apply

Documentation

The induced map carries the class of an element to the class of its image.

Source context 3 commands

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

namespace ProCGroups.Abelian
universe u v
variable {G H J : Type*}
  [TopologicalSpace G] [Group G] [IsTopologicalGroup G]
  [TopologicalSpace H] [Group H] [IsTopologicalGroup H]
  [TopologicalSpace J] [Group J] [IsTopologicalGroup J]

Lean source · statement

theorem abelianModPowerMap_mk_apply (q : ℕ) (f : G →ₜ* H) (a : G) :
    abelianModPowerMap q f (abelianModPowerMk G q a) =
      abelianModPowerMk H q (f a)

Module documentation

Abelianization modulo a power

Declarations