NYLL
Module

Closed.lean

Nyll.ProCGroups.ProC.Subgroups.Closed
7 declarations indexed from sourceView source ↗

Module documentation

Closed subgroups, ranges, and extensions of pro-\(C\) groups

The pro-\(C\) basis passes to closed subgroups when \(C\) is subgroup-closed, to Hausdorff continuous quotients when \(C\) is a formation, and across a closed normal extension when \(C\) is extension-closed.

Imports1
Imported by13

Declarations

theorem

of_closedSubgroup

L33 ↗
ProCGroups.ProC.HasOpenNormalBasisInClass.of_closedSubgroup
Documentation

A closed subgroup of a pro-\(C\) group 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
section
variable {C : FiniteGroupClass.{u}}
variable {G : Type u} [Group G] [TopologicalSpace G] [IsTopologicalGroup G]
namespace HasOpenNormalBasisInClass
omit [IsTopologicalGroup G] in
Lean source · statement
theorem of_closedSubgroup
    (hIso : FiniteGroupClass.IsomClosed C)
    (hSub : FiniteGroupClass.SubgroupClosed C)
    (hG : HasOpenNormalBasisInClass C G) (H : ClosedSubgroup G) :
    HasOpenNormalBasisInClass C ↥(H : Subgroup G)
theorem

of_isClosed_subgroup

L78 ↗
ProCGroups.ProC.HasOpenNormalBasisInClass.of_isClosed_subgroup
Documentation

A closed ordinary subgroup of a pro-\(C\) group is pro-\(C\) with the induced topology.

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
section
variable {C : FiniteGroupClass.{u}}
variable {G : Type u} [Group G] [TopologicalSpace G] [IsTopologicalGroup G]
namespace HasOpenNormalBasisInClass
omit [IsTopologicalGroup G] in
Lean source · statement
theorem of_isClosed_subgroup
    (hIso : FiniteGroupClass.IsomClosed C)
    (hSub : FiniteGroupClass.SubgroupClosed C)
    (hG : HasOpenNormalBasisInClass C G) (H : Subgroup G) (hH : IsClosed (H : Set G)) :
    HasOpenNormalBasisInClass C H
theorem

of_closedSubgroup_of_fullFormation

L88 ↗
ProCGroups.ProC.HasOpenNormalBasisInClass.of_closedSubgroup_of_fullFormation
Documentation

Closed-subgroup permanence for pro-\(C\) groups from a full formation package.

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
section
variable {C : FiniteGroupClass.{u}}
variable {G : Type u} [Group G] [TopologicalSpace G] [IsTopologicalGroup G]
namespace HasOpenNormalBasisInClass
omit [IsTopologicalGroup G] in
Lean source · statement
theorem of_closedSubgroup_of_fullFormation
    (hC : FiniteGroupClass.FullFormation C)
    (hG : HasOpenNormalBasisInClass C G) (H : ClosedSubgroup G) :
    HasOpenNormalBasisInClass C ↥(H : Subgroup G)
theorem

of_isClosed_subgroup_of_fullFormation

L96 ↗
ProCGroups.ProC.HasOpenNormalBasisInClass.of_isClosed_subgroup_of_fullFormation
Documentation

Closed-subgroup permanence in ordinary subgroup form from a full formation package.

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
section
variable {C : FiniteGroupClass.{u}}
variable {G : Type u} [Group G] [TopologicalSpace G] [IsTopologicalGroup G]
namespace HasOpenNormalBasisInClass
omit [IsTopologicalGroup G] in
Lean source · statement
theorem of_isClosed_subgroup_of_fullFormation
    (hC : FiniteGroupClass.FullFormation C)
    (hG : HasOpenNormalBasisInClass C G) (H : Subgroup G) (hH : IsClosed (H : Set G)) :
    HasOpenNormalBasisInClass C H
theorem

range

L106 ↗
ProCGroups.ProC.HasOpenNormalBasisInClass.range
Documentation

The range of a continuous homomorphism from a pro-\(C\) group to a Hausdorff topological group is again pro-\(C\), with the induced subtype topology.

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
section
variable {C : FiniteGroupClass.{u}}
variable {G : Type u} [Group G] [TopologicalSpace G] [IsTopologicalGroup G]
namespace HasOpenNormalBasisInClass
Lean source · statement
theorem range
    (hIso : FiniteGroupClass.IsomClosed C)
    (hQuot : FiniteGroupClass.QuotientClosed C)
    [CompactSpace G] [T2Space G] [TotallyDisconnectedSpace G]
    (hG : HasOpenNormalBasisInClass C G)
    {H : Type u} [Group H] [TopologicalSpace H] [IsTopologicalGroup H] [T2Space H]
    (f : G →ₜ* H) :
    HasOpenNormalBasisInClass C f.toMonoidHom.range
theorem

of_surjective

L127 ↗
ProCGroups.ProC.HasOpenNormalBasisInClass.of_surjective
Documentation

A Hausdorff continuous quotient of a group with an open-normal \(C\)-basis again has such a basis.

Source context 7 commands

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

open Set
open scoped Topology Pointwise
namespace ProCGroups.ProC
universe u
section
variable {C : FiniteGroupClass.{u}}
variable {G : Type u} [Group G] [TopologicalSpace G] [IsTopologicalGroup G]
Lean source · statement
theorem HasOpenNormalBasisInClass.of_surjective
    (hForm : FiniteGroupClass.Formation C)
    [CompactSpace G] [T2Space G] [TotallyDisconnectedSpace G]
    (hG : HasOpenNormalBasisInClass C G)
    {H : Type u} [Group H] [TopologicalSpace H] [IsTopologicalGroup H] [T2Space H]
    (f : G →ₜ* H) (hf : Function.Surjective f) :
    HasOpenNormalBasisInClass C H
theorem

extension

L161 ↗
ProCGroups.ProC.HasOpenNormalBasisInClass.extension
Documentation

If E is profinite, K is a normal pro-\(C\) subgroup of E, and E/K is pro-\(C\), then E 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
section
variable {C : FiniteGroupClass.{u}}
variable {G : Type u} [Group G] [TopologicalSpace G] [IsTopologicalGroup G]
namespace HasOpenNormalBasisInClass
variable {E : Type u} [Group E] [TopologicalSpace E] [IsTopologicalGroup E]
Lean source · statement
theorem extension
    (hIso : FiniteGroupClass.IsomClosed C)
    (hQuot : FiniteGroupClass.QuotientClosed C)
    (hExt : FiniteGroupClass.ExtensionClosed C)
    [CompactSpace E] [T2Space E] [TotallyDisconnectedSpace E]
    (K : Subgroup E) [K.Normal] (hKclosed : IsClosed (K : Set E))
    (hK : HasOpenNormalBasisInClass C K) (hQ : HasOpenNormalBasisInClass C (E ⧸ K)) :
    HasOpenNormalBasisInClass C E

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