Module

ClosedNormal.lean

Nyll.ProCGroups.ProC.Quotients.ClosedNormal

10 declarations indexed from sourceView source ↗

Module documentation

Quotients by closed normal subgroups

This file supplies the profinite topology and normalized continuous sections for closed-normal quotients, identifies iterated quotients, proves closedness of quotient images, and transfers topological generation between a group, its kernel, and its quotient.

Imports2

Imported by20

theorem

totallyDisconnectedSpace_quotient_closedNormal

L27 ↗

ProCGroups.totallyDisconnectedSpace_quotient_closedNormal

Documentation

A quotient by a closed normal subgroup of a compact Hausdorff totally disconnected topological group is totally disconnected.

Source context 4 commands

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

open Set
open scoped Topology Pointwise
namespace ProCGroups
universe u v

Lean source · statement

theorem totallyDisconnectedSpace_quotient_closedNormal
    {G : Type*} [Group G] [TopologicalSpace G] [IsTopologicalGroup G]
    [CompactSpace G] [T2Space G] [TotallyDisconnectedSpace G]
    (N : Subgroup G) [N.Normal] (hN : IsClosed (N : Set G)) :
    TotallyDisconnectedSpace (G ⧸ N)

def

closedNormalQuotientSection

L114 ↗

ProCGroups.Generation.closedNormalQuotientSection

Documentation

A chosen continuous section of the quotient map by a closed normal subgroup of a profinite group.

Source context 6 commands

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

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

Lean source · statement

def closedNormalQuotientSection
    {N : Subgroup G} (hNclosed : IsClosed (N : Set G)) :
    G ⧸ N → G

theorem

closedNormalQuotientSection_continuous

L120 ↗

ProCGroups.Generation.closedNormalQuotientSection_continuous

Documentation

The chosen closed-normal quotient section is continuous.

Source context 6 commands

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

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

Lean source · statement

theorem closedNormalQuotientSection_continuous
    {N : Subgroup G} (hNclosed : IsClosed (N : Set G)) :
    Continuous (closedNormalQuotientSection (G := G) (N := N) hNclosed)

theorem

closedNormalQuotientSection_rightInverse

L127 ↗

ProCGroups.Generation.closedNormalQuotientSection_rightInverse

Documentation

The chosen closed-normal quotient section is a right inverse to the quotient map.

Source context 6 commands

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

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

Lean source · statement

theorem closedNormalQuotientSection_rightInverse
    {N : Subgroup G} (hNclosed : IsClosed (N : Set G)) :
    Function.RightInverse
      (closedNormalQuotientSection (G := G) (N := N) hNclosed)
      (QuotientGroup.mk (s := N))

theorem

closedNormalQuotientSection_one

L136 ↗

ProCGroups.Generation.closedNormalQuotientSection_one

Documentation

The chosen closed-normal quotient section sends the identity coset to \(1\).

Source context 6 commands

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

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

Lean source · statement

theorem closedNormalQuotientSection_one
    {N : Subgroup G} (hNclosed : IsClosed (N : Set G)) :
    closedNormalQuotientSection (G := G) (N := N) hNclosed
      (QuotientGroup.mk (s := N) (1 : G)) = 1

def

quotientBotContinuousMulEquiv

L147 ↗

ProCGroups.Generation.quotientBotContinuousMulEquiv

Documentation

The quotient by the bottom subgroup is continuously multiplicatively equivalent to the original profinite group.

Source context 6 commands

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

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

Lean source · statement

def quotientBotContinuousMulEquiv :
    G ≃ₜ* G ⧸ (⊥ : Subgroup G)

theorem

topologicallyGenerates_union_closedNormal_iff_quotient

L158 ↗

ProCGroups.Generation.topologicallyGenerates_union_closedNormal_iff_quotient

Documentation

Adding a closed normal subgroup to a generating set is equivalent to generating the quotient from the image of the set.

Source context 7 commands

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

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

Lean source · statement

theorem topologicallyGenerates_union_closedNormal_iff_quotient
    {N : Subgroup G} [N.Normal]
    (hNclosed : IsClosed (N : Set G)) {X : Set G} :
    TopologicallyGenerates (G := G) (X ∪ (N : Set G)) ↔
      TopologicallyGenerates (G := G ⧸ N) ((QuotientGroup.mk' N) '' X)

theorem

isClosed_image_closedNormal_quotient

L258 ↗

ProCGroups.Generation.isClosed_image_closedNormal_quotient

Documentation

The image of a closed subgroup in a quotient by a closed normal subgroup is closed.

Source context 7 commands

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

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

Lean source · statement

theorem isClosed_image_closedNormal_quotient
    {N N' : Subgroup G} [N'.Normal]
    (hNclosed : IsClosed (N : Set G)) (hN'closed : IsClosed (N' : Set G)) :
    IsClosed ((N.map (QuotientGroup.mk' N') : Subgroup (G ⧸ N')) : Set (G ⧸ N'))

def

quotientQuotientContinuousMulEquiv

L281 ↗

ProCGroups.Generation.quotientQuotientContinuousMulEquiv

Documentation

The quotient-of-quotient isomorphism for closed normal subgroups as a continuous multiplicative equivalence.

Source context 6 commands

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

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

Lean source · statement

def quotientQuotientContinuousMulEquiv
    {N N' : Subgroup G} [N.Normal] [N'.Normal]
    (hNclosed : IsClosed (N : Set G))
    (hN'N : N' ≤ N) :
    ((G ⧸ N') ⧸ N.map (QuotientGroup.mk' N')) ≃ₜ* G ⧸ N

theorem

topologicallyGenerates_of_quotient_section_union_kernel

L301 ↗

ProCGroups.Generation.topologicallyGenerates_of_quotient_section_union_kernel

Documentation

A quotient section together with generators for the kernel generates the intermediate quotient.

Source context 7 commands

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

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

Lean source · statement

theorem topologicallyGenerates_of_quotient_section_union_kernel
    {N N' : Subgroup G} [N.Normal] [N'.Normal]
    (hNclosed : IsClosed (N : Set G)) (hN'closed : IsClosed (N' : Set G))
    (hN'N : N' ≤ N)
    {Y : Set (G ⧸ N)}
    (hYgen : TopologicallyGenerates (G := G ⧸ N) Y)
    {σ : (G ⧸ N) → (G ⧸ N')}
    (hσright : Function.RightInverse σ (leftQuotientProjection N' N hN'N))
    {T : Set G}
    (hTgen : N ≤ Subgroup.closure (T ∪ (N' : Set G))) :
    TopologicallyGenerates (G := G ⧸ N')
      (σ '' Y ∪ ((QuotientGroup.mk' N') '' T))

Module documentation

Quotients by closed normal subgroups

Declarations