Module

Abelian.lean

Nyll.ProCGroups.ProC.GroupPredicates.Abelian

1 declaration indexed from sourceView source ↗

Module documentation

Abelian open-normal quotient bases

This file proves that a profinite group with an abelian open-normal quotient basis is itself abelian. The proof tests commutators in all open normal quotients and then uses profinite separation.

Imports1

Nyll.ProCGroups.ProC.InverseLimits.Predicates

Imported by3

theorem

isAbelian

L35 ↗

ProCGroups.ProC.HasAbelianOpenNormalBasis.isAbelian

Documentation

A profinite group with an abelian open-normal quotient basis is abelian.

Source context 9 commands

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

open Set
open scoped Topology Pointwise
namespace ProCGroups.ProC
universe u v
open InverseSystems
section
variable {G : Type u} [Group G] [TopologicalSpace G] [IsTopologicalGroup G]
  [CompactSpace G] [T2Space G] [TotallyDisconnectedSpace G]
namespace HasAbelianOpenNormalBasis
omit [T2Space G] in

Lean source · statement

theorem isAbelian (hG : HasAbelianOpenNormalBasis G) : ∀ a b : G, a * b = b * a

Module documentation

Abelian open-normal quotient bases

Declarations

isAbelian