Module

SigmaEquivalence.lean

Nyll.Yamaguchi26AbfaithfulGalois.GroupTheory.SigmaEquivalence

1 declaration indexed from sourceView source ↗

Module documentation

Transport of Sigma-ab-faithfulness

A topological group equivalence identifies every open layer and its normal quotient action on the actual residual abelianization.

Imports3

Imported by3

theorem

of_continuousMulEquiv

L24 ↗

ProCGroups.FiniteStepSolvableQuotients.IsSigmaAbFaithful.of_continuousMulEquiv

Documentation

Sigma-ab-faithfulness is invariant under topological group equivalences.

Source context 3 commands

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

namespace ProCGroups.FiniteStepSolvableQuotients
open ProCGroups.ProC
universe u

Lean source · statement

theorem IsSigmaAbFaithful.of_continuousMulEquiv
    {G H : Type u} [Group G] [Group H]
    [TopologicalSpace G] [TopologicalSpace H]
    [IsTopologicalGroup G] [IsTopologicalGroup H]
    [CompactSpace G] [T2Space G] [TotallyDisconnectedSpace G]
    [CompactSpace H] [T2Space H] [TotallyDisconnectedSpace H]
    {sigma : Set ℕ} (e : G ≃ₜ* H) (hH : IsSigmaAbFaithful sigma H) :
    IsSigmaAbFaithful sigma G

Module documentation

Transport of Sigma-ab-faithfulness

Declarations

of_continuousMulEquiv