Module

Conjugation.lean

Nyll.ProCGroups.Topologies.Conjugation

4 declarations indexed from sourceView source ↗

Module documentation

Continuous conjugation actions

This file bundles conjugation by a normalizing element as a continuous multiplicative equivalence. It also descends conjugation to quotients by topologically characteristic subgroups and records the formula on quotient representatives.

Imports2

Imported by5

def

conjNormalContinuousMulEquiv

L27 ↗

ProCGroups.Subgroup.conjNormalContinuousMulEquiv

Documentation

Conjugation by an ambient element as a continuous automorphism of a normal subgroup.

Source context 4 commands

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

open scoped Topology
namespace ProCGroups
namespace Subgroup
universe u

Lean source · statement

def conjNormalContinuousMulEquiv
    {G : Type u} [TopologicalSpace G] [Group G] [IsTopologicalGroup G]
    (N : Subgroup G) [N.Normal] (g : G) : N ≃ₜ* N

theorem

conjNormalContinuousMulEquiv_apply

L45 ↗

ProCGroups.Subgroup.conjNormalContinuousMulEquiv_apply

Documentation

The conjugation equivalence is evaluated by conjugating representatives.

Source context 4 commands

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

open scoped Topology
namespace ProCGroups
namespace Subgroup
universe u

Lean source · statement

theorem conjNormalContinuousMulEquiv_apply
    {G : Type u} [TopologicalSpace G] [Group G] [IsTopologicalGroup G]
    (N : Subgroup G) [N.Normal] (g : G) (x : N) :
    conjNormalContinuousMulEquiv N g x = MulAut.conjNormal g x

def

quotientConjugationOnTopologicallyCharacteristicQuotient

L65 ↗

ProCGroups.Topologies.quotientConjugationOnTopologicallyCharacteristicQuotient

Documentation

Topological variant of \(\mathrm{ProCGroups.GroupTheory.quotientConjugationOnCharacteristicQuotient}\). It only needs \(K\) to be preserved by continuous automorphisms, since the conjugation maps used to define the action are continuous.

Source context 3 commands

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

open scoped Topology
namespace ProCGroups.Topologies
universe u

Lean source · statement

def quotientConjugationOnTopologicallyCharacteristicQuotient
    {G : Type u} [TopologicalSpace G] [Group G] [IsTopologicalGroup G]
    (N : Subgroup G) [N.Normal] (K : Subgroup N) [K.TopologicallyCharacteristic]
    (hNactsTrivially :
      ∀ n x : N, (((MulAut.conjNormal (n : G)) x) * x⁻¹ : N) ∈ K) :
    (G ⧸ N) →* MulAut (N ⧸ K)

theorem

quotientConjugationOnTopologicallyCharacteristicQuotient_mk_apply_mk

L104 ↗

ProCGroups.Topologies.quotientConjugationOnTopologicallyCharacteristicQuotient_mk_apply_mk

Documentation

The topological conjugation action sends representatives to conjugates.

Source context 3 commands

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

open scoped Topology
namespace ProCGroups.Topologies
universe u

Lean source · statement

theorem quotientConjugationOnTopologicallyCharacteristicQuotient_mk_apply_mk
    {G : Type u} [TopologicalSpace G] [Group G] [IsTopologicalGroup G]
    (N : Subgroup G) [N.Normal] (K : Subgroup N) [K.TopologicallyCharacteristic]
    (hNactsTrivially :
      ∀ n x : N, (((MulAut.conjNormal (n : G)) x) * x⁻¹ : N) ∈ K)
    (g : G) (n : N) :
    quotientConjugationOnTopologicallyCharacteristicQuotient
      (G := G) N K hNactsTrivially
      (QuotientGroup.mk' N g) (QuotientGroup.mk' K n) =
        QuotientGroup.mk' K ((MulAut.conjNormal g) n)

Module documentation

Continuous conjugation actions

Declarations

conjNormalContinuousMulEquiv

conjNormalContinuousMulEquiv_apply

quotientConjugationOnTopologicallyCharacteristicQuotient

quotientConjugationOnTopologicallyCharacteristicQuotient_mk_apply_mk