Module

TopologicallyCharacteristicSubgroups.lean

Nyll.ProCGroups.Topologies.TopologicallyCharacteristicSubgroups

38 declarations indexed from sourceView source ↗

Module documentation

Topologically characteristic subgroups

This file studies subgroups invariant under continuous automorphisms. It proves invariance of the closed commutator subgroup, gives equivalent map and comap formulations, and establishes closure of topologically characteristic subgroups under lattice operations and topological closure.

Imports4

Mathlib.Topology.Algebra.ContinuousMonoidHom
Mathlib.Topology.Algebra.Group.Quotient
Mathlib.GroupTheory.Commutator.Basic
Nyll.ProCGroups.Topologies.QuotientMaps

Imported by9

lemma

image_subtype_eq_map

L25 ↗

TopologicalGroup.image_subtype_eq_map

Documentation

Identify the image of a subgroup with its Subgroup.map.

Source context 2 commands

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

universe u
namespace TopologicalGroup

Lean source · full declaration

lemma image_subtype_eq_map
    {G : Type u} [Group G]
    {H : Type _} [Group H]
    (f : G →* H) (K : Subgroup G) :
    (fun x : G => f x) '' (K : Set G) = ((K.map f : Subgroup H) : Set H) := by
  ext y
  constructor
  · rintro ⟨x, hx, rfl⟩
    exact ⟨x, hx, rfl⟩
  · rintro ⟨x, hx, rfl⟩
    exact ⟨x, hx, rfl⟩

lemma

map_symm_toMonoidHom_eq_comap

L41 ↗

TopologicalGroup.map_symm_toMonoidHom_eq_comap

Documentation

Mapping a subgroup by the inverse of an automorphism agrees with comapping along the automorphism itself.

Source context 2 commands

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

universe u
namespace TopologicalGroup

Lean source · statement

lemma map_symm_toMonoidHom_eq_comap
    {G : Type u} [Group G] (K : Subgroup G) (e : G ≃* G) :
    K.map e.symm.toMonoidHom = K.comap e.toMonoidHom

theorem

map_topologicalClosure_le_of_map_le

L66 ↗

Subgroup.map_topologicalClosure_le_of_map_le

Documentation

Continuous maps send the topological closure of a subgroup into a closed subgroup whenever they send the subgroup itself into that closed subgroup.

Source context 4 commands

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

universe u
namespace Subgroup
variable {G : Type u} [TopologicalSpace G] [Group G] [IsTopologicalGroup G]
variable {H K : Subgroup G}

Lean source · statement

theorem map_topologicalClosure_le_of_map_le
    {G H : Type*} [TopologicalSpace G] [Group G] [IsTopologicalGroup G]
    [TopologicalSpace H] [Group H]
    {A : Subgroup G} {B : Subgroup H} {f : G →* H}
    (hf : Continuous f) (hAB : A.map f ≤ B) (hB : IsClosed (B : Set H)) :
    A.topologicalClosure.map f ≤ B

theorem

map_topologicalClosure_eq_of_continuousMulEquiv

L82 ↗

Subgroup.map_topologicalClosure_eq_of_continuousMulEquiv

Documentation

Homeomorphic group equivalences commute with topological closure of subgroups.

Source context 4 commands

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

universe u
namespace Subgroup
variable {G : Type u} [TopologicalSpace G] [Group G] [IsTopologicalGroup G]
variable {H K : Subgroup G}

Lean source · statement

theorem map_topologicalClosure_eq_of_continuousMulEquiv
    {G H : Type*} [TopologicalSpace G] [Group G] [IsTopologicalGroup G]
    [TopologicalSpace H] [Group H] [IsTopologicalGroup H]
    (e : G ≃ₜ* H) (A : Subgroup G) :
    A.topologicalClosure.map e.toMulEquiv.toMonoidHom =
      (A.map e.toMulEquiv.toMonoidHom).topologicalClosure

abbrev

closedCommutator

L110 ↗

Subgroup.closedCommutator

Documentation

The closed commutator subgroup of a topological group.

Source context 4 commands

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

universe u
namespace Subgroup
variable {G : Type u} [TopologicalSpace G] [Group G] [IsTopologicalGroup G]
variable {H K : Subgroup G}

Lean source · statement

abbrev closedCommutator (G : Type*) [TopologicalSpace G] [Group G]
    [IsTopologicalGroup G] : Subgroup G

theorem

isClosed_closedCommutator

L115 ↗

Subgroup.isClosed_closedCommutator

Documentation

The closed commutator subgroup is closed.

Source context 4 commands

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

universe u
namespace Subgroup
variable {G : Type u} [TopologicalSpace G] [Group G] [IsTopologicalGroup G]
variable {H K : Subgroup G}

Lean source · statement

theorem isClosed_closedCommutator
    (G : Type*) [TopologicalSpace G] [Group G] [IsTopologicalGroup G] :
    IsClosed (closedCommutator G : Set G)

theorem

commutator_le_closedCommutator

L121 ↗

Subgroup.commutator_le_closedCommutator

Documentation

The abstract commutator subgroup is contained in the closed commutator subgroup.

Source context 4 commands

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

universe u
namespace Subgroup
variable {G : Type u} [TopologicalSpace G] [Group G] [IsTopologicalGroup G]
variable {H K : Subgroup G}

Lean source · statement

theorem commutator_le_closedCommutator
    (G : Type*) [TopologicalSpace G] [Group G] [IsTopologicalGroup G] :
    _root_.commutator G ≤ closedCommutator G

theorem

topologicalClosure_eq_self_of_discrete

L129 ↗

Subgroup.topologicalClosure_eq_self_of_discrete

Documentation

In a discrete topological group, the topological closure of a subgroup is the subgroup itself.

Source context 4 commands

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

universe u
namespace Subgroup
variable {G : Type u} [TopologicalSpace G] [Group G] [IsTopologicalGroup G]
variable {H K : Subgroup G}

Lean source · statement

theorem topologicalClosure_eq_self_of_discrete
    (H : Subgroup G) [DiscreteTopology G] :
    H.topologicalClosure = H

theorem

closedCommutator_eq_commutator_of_discrete

L139 ↗

Subgroup.closedCommutator_eq_commutator_of_discrete

Documentation

For a discrete group, the closed commutator subgroup agrees with the ordinary commutator subgroup.

Source context 4 commands

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

universe u
namespace Subgroup
variable {G : Type u} [TopologicalSpace G] [Group G] [IsTopologicalGroup G]
variable {H K : Subgroup G}

Lean source · statement

theorem closedCommutator_eq_commutator_of_discrete
    (G : Type*) [TopologicalSpace G] [Group G] [IsTopologicalGroup G]
    [DiscreteTopology G] :
    closedCommutator G = _root_.commutator G

theorem

closedCommutator_map_le

L146 ↗

Subgroup.closedCommutator_map_le

Documentation

Continuous homomorphisms send closed commutator subgroups into closed commutator subgroups.

Source context 4 commands

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

universe u
namespace Subgroup
variable {G : Type u} [TopologicalSpace G] [Group G] [IsTopologicalGroup G]
variable {H K : Subgroup G}

Lean source · statement

theorem closedCommutator_map_le
    {G H : Type*} [TopologicalSpace G] [Group G] [IsTopologicalGroup G]
    [TopologicalSpace H] [Group H] [IsTopologicalGroup H]
    (f : G →ₜ* H) :
    (closedCommutator G).map f.toMonoidHom ≤ closedCommutator H

theorem

closedCommutator_map_eq_of_equiv

L163 ↗

Subgroup.closedCommutator_map_eq_of_equiv

Documentation

Continuous group equivalences map the closed commutator subgroup onto the closed commutator subgroup.

Source context 4 commands

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

universe u
namespace Subgroup
variable {G : Type u} [TopologicalSpace G] [Group G] [IsTopologicalGroup G]
variable {H K : Subgroup G}

Lean source · statement

theorem closedCommutator_map_eq_of_equiv
    {G H : Type*} [TopologicalSpace G] [Group G] [IsTopologicalGroup G]
    [TopologicalSpace H] [Group H] [IsTopologicalGroup H]
    (e : G ≃ₜ* H) :
    (closedCommutator G).map e.toMulEquiv.toMonoidHom = closedCommutator H

theorem

closedCommutator_characteristic

L184 ↗

Subgroup.closedCommutator_characteristic

Documentation

The closed commutator subgroup is invariant under continuous automorphisms.

Source context 4 commands

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

universe u
namespace Subgroup
variable {G : Type u} [TopologicalSpace G] [Group G] [IsTopologicalGroup G]
variable {H K : Subgroup G}

Lean source · statement

theorem closedCommutator_characteristic
    {G : Type*} [TopologicalSpace G] [Group G] [IsTopologicalGroup G] :
    ∀ e : G ≃ₜ* G,
      (closedCommutator G).map e.toMulEquiv.toMonoidHom = closedCommutator G

structure

TopologicallyCharacteristic

L191 ↗

Subgroup.TopologicallyCharacteristic

Documentation

A subgroup is topologically characteristic if every continuous automorphism preserves it.

Source context 4 commands

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

universe u
namespace Subgroup
variable {G : Type u} [TopologicalSpace G] [Group G] [IsTopologicalGroup G]
variable {H K : Subgroup G}

Lean source · full declaration

structure TopologicallyCharacteristic
    (H : Subgroup G) : Prop where
  /-- Pulling back \(H\) along any continuous automorphism of \(G\) leaves \(H\) unchanged. -/
  comap_eq : ∀ e : G ≃ₜ* G, H.comap e.toMulEquiv.toMonoidHom = H

instance

topologicallyCharacteristic_of_characteristic

L199 ↗

Subgroup.topologicallyCharacteristic_of_characteristic

Documentation

Every abstractly characteristic subgroup is invariant under continuous automorphisms.

Source context 5 commands

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

universe u
namespace Subgroup
variable {G : Type u} [TopologicalSpace G] [Group G] [IsTopologicalGroup G]
variable {H K : Subgroup G}
attribute [class] TopologicallyCharacteristic

Lean source · statement

instance topologicallyCharacteristic_of_characteristic
    [H.Characteristic] :
    H.TopologicallyCharacteristic

theorem

topologicallyCharacteristic_iff_comap_eq

L213 ↗

Subgroup.topologicallyCharacteristic_iff_comap_eq

Documentation

Topological characteristicity is equivalent to invariance under comap by every continuous automorphism.

Source context 6 commands

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

universe u
namespace Subgroup
variable {G : Type u} [TopologicalSpace G] [Group G] [IsTopologicalGroup G]
variable {H K : Subgroup G}
attribute [class] TopologicallyCharacteristic
omit [IsTopologicalGroup G] in

Lean source · statement

theorem topologicallyCharacteristic_iff_comap_eq :
    H.TopologicallyCharacteristic ↔
      ∀ e : G ≃ₜ* G, H.comap e.toMulEquiv.toMonoidHom = H

theorem

topologicallyCharacteristic_iff_comap_le

L223 ↗

Subgroup.topologicallyCharacteristic_iff_comap_le

Documentation

A subgroup is topologically characteristic exactly when every automorphism comap is contained in it.

Source context 6 commands

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

universe u
namespace Subgroup
variable {G : Type u} [TopologicalSpace G] [Group G] [IsTopologicalGroup G]
variable {H K : Subgroup G}
attribute [class] TopologicallyCharacteristic
omit [IsTopologicalGroup G] in

Lean source · statement

theorem topologicallyCharacteristic_iff_comap_le :
    H.TopologicallyCharacteristic ↔
      ∀ e : G ≃ₜ* G, H.comap e.toMulEquiv.toMonoidHom ≤ H

theorem

topologicallyCharacteristic_iff_le_comap

L236 ↗

Subgroup.topologicallyCharacteristic_iff_le_comap

Documentation

A subgroup is topologically characteristic exactly when it is contained in every automorphism comap.

Source context 6 commands

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

universe u
namespace Subgroup
variable {G : Type u} [TopologicalSpace G] [Group G] [IsTopologicalGroup G]
variable {H K : Subgroup G}
attribute [class] TopologicallyCharacteristic
omit [IsTopologicalGroup G] in

Lean source · statement

theorem topologicallyCharacteristic_iff_le_comap :
    H.TopologicallyCharacteristic ↔
      ∀ e : G ≃ₜ* G, H ≤ H.comap e.toMulEquiv.toMonoidHom

theorem

topologicallyCharacteristic_iff_map_eq

L251 ↗

Subgroup.topologicallyCharacteristic_iff_map_eq

Documentation

Topological characteristicity is equivalent to invariance under image by every continuous automorphism.

Source context 6 commands

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

universe u
namespace Subgroup
variable {G : Type u} [TopologicalSpace G] [Group G] [IsTopologicalGroup G]
variable {H K : Subgroup G}
attribute [class] TopologicallyCharacteristic
omit [IsTopologicalGroup G] in

Lean source · statement

theorem topologicallyCharacteristic_iff_map_eq :
    H.TopologicallyCharacteristic ↔
      ∀ e : G ≃ₜ* G, H.map e.toMulEquiv.toMonoidHom = H

theorem

closedCommutator_topologicallyCharacteristic

L259 ↗

Subgroup.closedCommutator_topologicallyCharacteristic

Documentation

The closed commutator subgroup is topologically characteristic.

Source context 5 commands

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

universe u
namespace Subgroup
variable {G : Type u} [TopologicalSpace G] [Group G] [IsTopologicalGroup G]
variable {H K : Subgroup G}
attribute [class] TopologicallyCharacteristic

Lean source · statement

theorem closedCommutator_topologicallyCharacteristic
    {G : Type*} [TopologicalSpace G] [Group G] [IsTopologicalGroup G] :
    (closedCommutator G).TopologicallyCharacteristic

theorem

topologicallyCharacteristic_iff_le_map

L270 ↗

Subgroup.topologicallyCharacteristic_iff_le_map

Documentation

A subgroup is topologically characteristic exactly when it is contained in every automorphism image.

Source context 6 commands

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

universe u
namespace Subgroup
variable {G : Type u} [TopologicalSpace G] [Group G] [IsTopologicalGroup G]
variable {H K : Subgroup G}
attribute [class] TopologicallyCharacteristic
omit [IsTopologicalGroup G] in

Lean source · statement

theorem topologicallyCharacteristic_iff_le_map :
    H.TopologicallyCharacteristic ↔
      ∀ e : G ≃ₜ* G, H ≤ H.map e.toMulEquiv.toMonoidHom

lemma

map_eq

L283 ↗

Subgroup.TopologicallyCharacteristic.map_eq

Documentation

A topologically characteristic subgroup is fixed by the image of every continuous automorphism.

Source context 7 commands

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

universe u
namespace Subgroup
variable {G : Type u} [TopologicalSpace G] [Group G] [IsTopologicalGroup G]
variable {H K : Subgroup G}
attribute [class] TopologicallyCharacteristic
namespace TopologicallyCharacteristic
omit [IsTopologicalGroup G] in

Lean source · statement

lemma map_eq
    (hH : H.TopologicallyCharacteristic) (e : G ≃ₜ* G) :
    H.map (e.toMulEquiv.toMonoidHom) = H

lemma

apply_mem_iff

L304 ↗

Subgroup.TopologicallyCharacteristic.apply_mem_iff

Documentation

Membership in a topologically characteristic subgroup is invariant under applying a continuous automorphism.

Source context 7 commands

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

universe u
namespace Subgroup
variable {G : Type u} [TopologicalSpace G] [Group G] [IsTopologicalGroup G]
variable {H K : Subgroup G}
attribute [class] TopologicallyCharacteristic
namespace TopologicallyCharacteristic
omit [IsTopologicalGroup G] in

Lean source · statement

lemma apply_mem_iff
    (hH : H.TopologicallyCharacteristic) (e : G ≃ₜ* G) {g : G} :
    e g ∈ H ↔ g ∈ H

theorem

inf

L312 ↗

Subgroup.TopologicallyCharacteristic.inf

Documentation

Intersections of topologically characteristic subgroups are topologically characteristic.

Source context 7 commands

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

universe u
namespace Subgroup
variable {G : Type u} [TopologicalSpace G] [Group G] [IsTopologicalGroup G]
variable {H K : Subgroup G}
attribute [class] TopologicallyCharacteristic
namespace TopologicallyCharacteristic
omit [IsTopologicalGroup G] in

Lean source · statement

theorem inf
    (hH : H.TopologicallyCharacteristic) (hK : K.TopologicallyCharacteristic) :
    (H ⊓ K).TopologicallyCharacteristic

theorem

sup

L325 ↗

Subgroup.TopologicallyCharacteristic.sup

Documentation

Supremums of topologically characteristic subgroups are topologically characteristic.

Source context 7 commands

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

universe u
namespace Subgroup
variable {G : Type u} [TopologicalSpace G] [Group G] [IsTopologicalGroup G]
variable {H K : Subgroup G}
attribute [class] TopologicallyCharacteristic
namespace TopologicallyCharacteristic
omit [IsTopologicalGroup G] in

Lean source · statement

theorem sup
    (hH : H.TopologicallyCharacteristic) (hK : K.TopologicallyCharacteristic) :
    (H ⊔ K).TopologicallyCharacteristic

theorem

sInf

L341 ↗

Subgroup.TopologicallyCharacteristic.sInf

Documentation

Arbitrary intersections of topologically characteristic subgroups are topologically characteristic.

Source context 7 commands

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

universe u
namespace Subgroup
variable {G : Type u} [TopologicalSpace G] [Group G] [IsTopologicalGroup G]
variable {H K : Subgroup G}
attribute [class] TopologicallyCharacteristic
namespace TopologicallyCharacteristic
omit [IsTopologicalGroup G] in

Lean source · statement

theorem sInf
    {S : Set (Subgroup G)}
    (hS : ∀ L ∈ S, L.TopologicallyCharacteristic) :
    (sInf S).TopologicallyCharacteristic

theorem

iInf

L360 ↗

Subgroup.TopologicallyCharacteristic.iInf

Documentation

Indexed intersections of topologically characteristic subgroups are topologically characteristic.

Source context 7 commands

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

universe u
namespace Subgroup
variable {G : Type u} [TopologicalSpace G] [Group G] [IsTopologicalGroup G]
variable {H K : Subgroup G}
attribute [class] TopologicallyCharacteristic
namespace TopologicallyCharacteristic
omit [IsTopologicalGroup G] in

Lean source · statement

theorem iInf
    {ι : Sort*} {S : ι → Subgroup G}
    (hS : ∀ i, (S i).TopologicallyCharacteristic) :
    (⨅ i, S i).TopologicallyCharacteristic

theorem

iSup

L376 ↗

Subgroup.TopologicallyCharacteristic.iSup

Documentation

Indexed supremums of topologically characteristic subgroups are topologically characteristic.

Source context 7 commands

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

universe u
namespace Subgroup
variable {G : Type u} [TopologicalSpace G] [Group G] [IsTopologicalGroup G]
variable {H K : Subgroup G}
attribute [class] TopologicallyCharacteristic
namespace TopologicallyCharacteristic
omit [IsTopologicalGroup G] in

Lean source · statement

theorem iSup
    {ι : Sort*} {S : ι → Subgroup G}
    (hS : ∀ i, (S i).TopologicallyCharacteristic) :
    (⨆ i, S i).TopologicallyCharacteristic

theorem

topologicalClosure

L392 ↗

Subgroup.TopologicallyCharacteristic.topologicalClosure

Documentation

The topological closure of a topologically characteristic subgroup is topologically characteristic.

Source context 6 commands

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

universe u
namespace Subgroup
variable {G : Type u} [TopologicalSpace G] [Group G] [IsTopologicalGroup G]
variable {H K : Subgroup G}
attribute [class] TopologicallyCharacteristic
namespace TopologicallyCharacteristic

Lean source · statement

theorem topologicalClosure
    (hH : H.TopologicallyCharacteristic) :
    H.topologicalClosure.TopologicallyCharacteristic

instance

botTopologicallyCharacteristic

L423 ↗

Subgroup.botTopologicallyCharacteristic

Documentation

The bottom subgroup is topologically characteristic.

Source context 5 commands

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

universe u
namespace Subgroup
variable {G : Type u} [TopologicalSpace G] [Group G] [IsTopologicalGroup G]
variable {H K : Subgroup G}
attribute [class] TopologicallyCharacteristic

Lean source · statement

instance botTopologicallyCharacteristic :
    (⊥ : Subgroup G).TopologicallyCharacteristic

instance

topTopologicallyCharacteristic

L427 ↗

Subgroup.topTopologicallyCharacteristic

Documentation

The top subgroup is topologically characteristic.

Source context 5 commands

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

universe u
namespace Subgroup
variable {G : Type u} [TopologicalSpace G] [Group G] [IsTopologicalGroup G]
variable {H K : Subgroup G}
attribute [class] TopologicallyCharacteristic

Lean source · statement

instance topTopologicallyCharacteristic :
    (⊤ : Subgroup G).TopologicallyCharacteristic

instance

commutatorTopologicallyCharacteristic

L431 ↗

Subgroup.commutatorTopologicallyCharacteristic

Documentation

Commutators of topologically characteristic subgroups are topologically characteristic.

Source context 5 commands

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

universe u
namespace Subgroup
variable {G : Type u} [TopologicalSpace G] [Group G] [IsTopologicalGroup G]
variable {H K : Subgroup G}
attribute [class] TopologicallyCharacteristic

Lean source · statement

instance commutatorTopologicallyCharacteristic
    [H.TopologicallyCharacteristic] [K.TopologicallyCharacteristic] :
    (⁅H, K⁆).TopologicallyCharacteristic

instance

centerTopologicallyCharacteristic

L448 ↗

Subgroup.centerTopologicallyCharacteristic

Documentation

The center is topologically characteristic.

Source context 5 commands

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

universe u
namespace Subgroup
variable {G : Type u} [TopologicalSpace G] [Group G] [IsTopologicalGroup G]
variable {H K : Subgroup G}
attribute [class] TopologicallyCharacteristic

Lean source · statement

instance centerTopologicallyCharacteristic :
    (center G).TopologicallyCharacteristic

instance

topologicallyCharacteristic_centralizerInst

L455 ↗

Subgroup.topologicallyCharacteristic_centralizerInst

Documentation

The centralizer of a topologically characteristic subgroup is again topologically characteristic.

Source context 5 commands

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

universe u
namespace Subgroup
variable {G : Type u} [TopologicalSpace G] [Group G] [IsTopologicalGroup G]
variable {H K : Subgroup G}
attribute [class] TopologicallyCharacteristic

Lean source · statement

instance topologicallyCharacteristic_centralizerInst
    [hH : H.TopologicallyCharacteristic] :
    (centralizer (H : Set G)).TopologicallyCharacteristic

instance

topologicallyCharacteristic_normalInst

L469 ↗

Subgroup.topologicallyCharacteristic_normalInst

Documentation

Topologically characteristic subgroups are normal.

Source context 5 commands

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

universe u
namespace Subgroup
variable {G : Type u} [TopologicalSpace G] [Group G] [IsTopologicalGroup G]
variable {H K : Subgroup G}
attribute [class] TopologicallyCharacteristic

Lean source · statement

instance topologicallyCharacteristic_normalInst
    [H.TopologicallyCharacteristic] :
    H.Normal

def

quotientMulEquiv

L494 ↗

Subgroup.TopologicallyCharacteristic.quotientMulEquiv

Documentation

A continuous automorphism descends to the quotient by a topologically characteristic subgroup.

Source context 6 commands

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

universe u
namespace Subgroup
variable {G : Type u} [TopologicalSpace G] [Group G] [IsTopologicalGroup G]
variable {H K : Subgroup G}
attribute [class] TopologicallyCharacteristic
namespace TopologicallyCharacteristic

Lean source · statement

def quotientMulEquiv
    (hH : H.TopologicallyCharacteristic) (e : G ≃ₜ* G) :
    G ⧸ H ≃* G ⧸ H

theorem

quotientMulEquiv_mk

L504 ↗

Subgroup.TopologicallyCharacteristic.quotientMulEquiv_mk

Documentation

The quotient equivalence induced by a topologically characteristic subgroup sends representatives to representatives.

Source context 6 commands

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

universe u
namespace Subgroup
variable {G : Type u} [TopologicalSpace G] [Group G] [IsTopologicalGroup G]
variable {H K : Subgroup G}
attribute [class] TopologicallyCharacteristic
namespace TopologicallyCharacteristic

Lean source · statement

theorem quotientMulEquiv_mk
    (hH : H.TopologicallyCharacteristic) (e : G ≃ₜ* G) (g : G) :
    hH.quotientMulEquiv e (QuotientGroup.mk' H g) =
      QuotientGroup.mk' H (e g)

def

quotientContinuousMulEquiv

L514 ↗

Subgroup.TopologicallyCharacteristic.quotientContinuousMulEquiv

Documentation

A topologically characteristic subgroup induces the corresponding continuous multiplicative equivalence on quotients.

Source context 6 commands

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

universe u
namespace Subgroup
variable {G : Type u} [TopologicalSpace G] [Group G] [IsTopologicalGroup G]
variable {H K : Subgroup G}
attribute [class] TopologicallyCharacteristic
namespace TopologicallyCharacteristic

Lean source · statement

def quotientContinuousMulEquiv
    (hH : H.TopologicallyCharacteristic) (e : G ≃ₜ* G) :
    G ⧸ H ≃ₜ* G ⧸ H

theorem

quotientContinuousMulEquiv_mk

L524 ↗

Subgroup.TopologicallyCharacteristic.quotientContinuousMulEquiv_mk

Documentation

The continuous quotient equivalence induced by a topologically characteristic subgroup sends representatives to representatives.

Source context 6 commands

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

universe u
namespace Subgroup
variable {G : Type u} [TopologicalSpace G] [Group G] [IsTopologicalGroup G]
variable {H K : Subgroup G}
attribute [class] TopologicallyCharacteristic
namespace TopologicallyCharacteristic

Lean source · statement

theorem quotientContinuousMulEquiv_mk
    (hH : H.TopologicallyCharacteristic) (e : G ≃ₜ* G) (g : G) :
    hH.quotientContinuousMulEquiv e (QuotientGroup.mk' H g) =
      QuotientGroup.mk' H (e g)

Module documentation

Topologically characteristic subgroups

Declarations