Module

FiniteQuotients.lean

Nyll.ProCGroups.ProC.InverseLimits.FiniteQuotients

5 declarations indexed from sourceView source ↗

Module documentation

Finite quotient objects for pro-\(C\) inverse limits

This file bundles finite discrete groups and quotients by open normal subgroups as profinite objects. It records the induced pro-\(C\) structures and the corresponding product construction.

Imports1

Nyll.ProCGroups.ProC.OpenNormalSubgroups.ProCGroup

Imported by11

theorem

of_finite_discrete

L33 ↗

ProCGroups.ProC.HasOpenNormalBasisInClass.of_finite_discrete

Documentation

Any finite discrete group already lying in the class \(C\) is pro-\(C\).

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 {C : FiniteGroupClass.{u}}
variable {G : Type u} [Group G] [TopologicalSpace G] [IsTopologicalGroup G]
namespace HasOpenNormalBasisInClass

Lean source · statement

theorem of_finite_discrete (hquot : FiniteGroupClass.QuotientClosed C)
    [Finite G] [DiscreteTopology G] (hCG : C G) : HasOpenNormalBasisInClass C G

theorem

quotient_openNormalSubgroup

L43 ↗

ProCGroups.ProC.HasOpenNormalBasisInClass.quotient_openNormalSubgroup

Documentation

If \(G\) is pro-\(C\) and \(C\) is closed under quotients, then every quotient of \(G\) by an open normal subgroup is again pro-\(C\).

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 {C : FiniteGroupClass.{u}}
variable {G : Type u} [Group G] [TopologicalSpace G] [IsTopologicalGroup G]
namespace HasOpenNormalBasisInClass

Lean source · statement

theorem quotient_openNormalSubgroup
    (hForm : FiniteGroupClass.Formation C)
    [CompactSpace G] [T2Space G]
    (hG : HasOpenNormalBasisInClass C G) (U : OpenNormalSubgroup G) :
    HasOpenNormalBasisInClass C (G ⧸ (U : Subgroup G))

theorem

quotient_openNormalSubgroupInClass

L52 ↗

ProCGroups.ProC.HasOpenNormalBasisInClass.quotient_openNormalSubgroupInClass

Documentation

Quotients by open normal subgroups in the class-indexing family are pro-\(C\).

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 {C : FiniteGroupClass.{u}}
variable {G : Type u} [Group G] [TopologicalSpace G] [IsTopologicalGroup G]
namespace HasOpenNormalBasisInClass

Lean source · statement

theorem quotient_openNormalSubgroupInClass
    (hquot : FiniteGroupClass.QuotientClosed C)
    (U : OpenNormalSubgroupInClass C G) :
    HasOpenNormalBasisInClass C (G ⧸ (U.1 : Subgroup G))

theorem

pi

L64 ↗

ProCGroups.ProC.HasOpenNormalBasisInClass.pi

Documentation

Arbitrary products of pro-\(C\) groups remain pro-\(C\) when \(C\) is a formation.

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 {C : FiniteGroupClass.{u}}
variable {G : Type u} [Group G] [TopologicalSpace G] [IsTopologicalGroup G]
namespace HasOpenNormalBasisInClass

Lean source · statement

theorem pi {α : Type u} {β : α → Type u}
    [∀ a, Group (β a)] [∀ a, TopologicalSpace (β a)] [∀ a, IsTopologicalGroup (β a)]
    [∀ a, CompactSpace (β a)] [∀ a, T2Space (β a)]
    [∀ a, TotallyDisconnectedSpace (β a)]
    (hForm : FiniteGroupClass.Formation C)
    (hβ : ∀ a, HasOpenNormalBasisInClass C (β a)) :
    HasOpenNormalBasisInClass C ((a : α) → β a)

theorem

hasOpenNormalBasisInClass_allFinite

L177 ↗

ProCGroups.ProC.hasOpenNormalBasisInClass_allFinite

Documentation

Every profinite group has an open-normal basis with finite quotients.

Source context 8 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 {C : FiniteGroupClass.{u}}
variable {G : Type u} [Group G] [TopologicalSpace G] [IsTopologicalGroup G]

Lean source · statement

theorem hasOpenNormalBasisInClass_allFinite
    {G : Type u} [Group G] [TopologicalSpace G] [IsTopologicalGroup G]
    [CompactSpace G] [T2Space G] [TotallyDisconnectedSpace G] :
    HasOpenNormalBasisInClass FiniteGroupClass.allFinite G

Module documentation

Finite quotient objects for pro-\(C\) inverse limits

Declarations

of_finite_discrete

quotient_openNormalSubgroup

quotient_openNormalSubgroupInClass

pi

hasOpenNormalBasisInClass_allFinite