Closed subgroups of topological groups

This file collects constructions on closed subgroups of a topological group.

An isomorphism of topological groups carries closed subgroups to closed subgroups. This is packaged as an order isomorphism, together with its compatibility with normality: the transport of a normal closed subgroup is normal. An isomorphism carrying one normal subgroup onto another also induces an isomorphism of the quotient topological groups, so a normal closed subgroup can be transported without changing the topological quotient it defines.

A closed subgroup H of A × G projecting onto G, that is with ∀ g, ∃ a, (a, g) ∈ H, is a closed relation from G to A defined everywhere. When A is compact, the fibre {a | (a, g) ∈ H} over each g is compact, so along a chain of such subgroups the fibres of the intersection are nonempty, and Zorn's lemma supplies a minimal such subgroup below any given one.

Main definitions

• ContinuousMulEquiv.closedSubgroupOrderIso: transport of closed subgroups along an isomorphism of topological groups.
• ContinuousMulEquiv.subgroupMap: a subgroup is topologically isomorphic to its image under an isomorphism of topological groups.
• ContinuousMulEquiv.quotientCongr: the induced isomorphism of quotient topological groups.

Main results

• Subgroup.forall_exists_mem_sInf_of_isChain: the intersection of a chain of closed subgroups of A × G projecting onto G still projects onto G.
• Subgroup.exists_minimal_isClosed_le: a closed subgroup of A × G projecting onto G contains a minimal closed subgroup projecting onto G.

def ContinuousMulEquiv.closedSubgroupOrderIso {G : Type u} {H : Type v} [Group G] [Group H] [TopologicalSpace G] [TopologicalSpace H] (e : G ≃ₜ* H) : ClosedSubgroup G ≃o ClosedSubgroup H

A topological group isomorphism transports closed subgroups, preserving inclusion.

Equations

• One or more equations did not get rendered due to their size.

@[simp]

theorem ContinuousMulEquiv.closedSubgroupOrderIso_apply_toSubgroup {G : Type u} {H : Type v} [Group G] [Group H] [TopologicalSpace G] [TopologicalSpace H] (e : G ≃ₜ* H) (K : ClosedSubgroup G) : ↑(e.closedSubgroupOrderIso K) = Subgroup.map e.toMonoidHom ↑K

The underlying subgroup transported by ContinuousMulEquiv.closedSubgroupOrderIso is the image of the original subgroup.

@[simp]

theorem ContinuousMulEquiv.closedSubgroupOrderIso_symm_apply_toSubgroup {G : Type u} {H : Type v} [Group G] [Group H] [TopologicalSpace G] [TopologicalSpace H] (e : G ≃ₜ* H) (L : ClosedSubgroup H) : ↑(e.closedSubgroupOrderIso.symm L) = Subgroup.map e.symm.toMonoidHom ↑L

The inverse transport of a closed subgroup is its image under the inverse topological group isomorphism.

@[simp]

theorem ContinuousMulEquiv.mem_closedSubgroupOrderIso {G : Type u} {H : Type v} [Group G] [Group H] [TopologicalSpace G] [TopologicalSpace H] (e : G ≃ₜ* H) (K : ClosedSubgroup G) {h : H} : h ∈ e.closedSubgroupOrderIso K ↔ e.symm h ∈ K

An element lies in a transported closed subgroup exactly when its inverse image lies in the original one.

@[simp]

theorem ContinuousMulEquiv.mem_closedSubgroupOrderIso_symm {G : Type u} {H : Type v} [Group G] [Group H] [TopologicalSpace G] [TopologicalSpace H] (e : G ≃ₜ* H) (L : ClosedSubgroup H) {g : G} : g ∈ e.closedSubgroupOrderIso.symm L ↔ e g ∈ L

An element lies in an inversely transported closed subgroup exactly when its image lies in the original one.

theorem ContinuousMulEquiv.apply_mem_closedSubgroupOrderIso {G : Type u} {H : Type v} [Group G] [Group H] [TopologicalSpace G] [TopologicalSpace H] (e : G ≃ₜ* H) (K : ClosedSubgroup G) {g : G} : e g ∈ e.closedSubgroupOrderIso K ↔ g ∈ K

The image of an element lies in a transported closed subgroup exactly when the element lies in the original one. This is not marked @[simp]: simp already reaches g ∈ K through ContinuousMulEquiv.mem_closedSubgroupOrderIso and ContinuousMulEquiv.symm_apply_apply.

instance ContinuousMulEquiv.instNormalClosedSubgroupOrderIso {G : Type u} {H : Type v} [Group G] [Group H] [TopologicalSpace G] [TopologicalSpace H] (e : G ≃ₜ* H) (K : ClosedSubgroup G) [(↑K).Normal] : (↑(e.closedSubgroupOrderIso K)).Normal

Normality is preserved when a closed subgroup is transported along a topological group isomorphism.

def ContinuousMulEquiv.subgroupMap {G : Type u} {H : Type v} [Group G] [Group H] [TopologicalSpace G] [TopologicalSpace H] (e : G ≃ₜ* H) (K : Subgroup G) : ↥K ≃ₜ* ↥(Subgroup.map (↑↑e) K)

A subgroup is topologically isomorphic to its image under a topological group isomorphism, for the subspace topologies. This is MulEquiv.subgroupMap together with the continuity of both directions.

Equations

• e.subgroupMap K = { toMulEquiv := (↑e).subgroupMap K, continuous_toFun := ⋯, continuous_invFun := ⋯ }

@[simp]

theorem ContinuousMulEquiv.coe_subgroupMap_apply {G : Type u} {H : Type v} [Group G] [Group H] [TopologicalSpace G] [TopologicalSpace H] (e : G ≃ₜ* H) (K : Subgroup G) (g : ↥K) : ↑((e.subgroupMap K) g) = e ↑g

ContinuousMulEquiv.subgroupMap applies the isomorphism.

@[simp]

theorem ContinuousMulEquiv.coe_subgroupMap_symm_apply {G : Type u} {H : Type v} [Group G] [Group H] [TopologicalSpace G] [TopologicalSpace H] (e : G ≃ₜ* H) (K : Subgroup G) (h : ↥(Subgroup.map (↑↑e) K)) : ↑((e.subgroupMap K).symm h) = e.symm ↑h

The inverse of ContinuousMulEquiv.subgroupMap applies the inverse isomorphism.

def ContinuousMulEquiv.quotientCongr {G : Type u} {H : Type v} [Group G] [Group H] [TopologicalSpace G] [TopologicalSpace H] (e : G ≃ₜ* H) (N : Subgroup G) (M : Subgroup H) [N.Normal] [M.Normal] (he : Subgroup.map e.toMonoidHom N = M) : G ⧸ N ≃ₜ* H ⧸ M

A topological group isomorphism carrying a normal subgroup onto a normal subgroup induces an isomorphism of the quotient topological groups. This is QuotientGroup.congr together with the continuity of both directions, which follows from the quotient-map property of the two projections.

For a normal closed subgroup N : ClosedSubgroup G the hypothesis holds by rfl on the transported subgroup, so e.quotientCongr N (e.closedSubgroupOrderIso N) rfl is the induced isomorphism G ⧸ N.toSubgroup ≃ₜ* H ⧸ (e.closedSubgroupOrderIso N).toSubgroup.

Equations

• e.quotientCongr N M he = { toMulEquiv := QuotientGroup.congr N M e.toMulEquiv he, continuous_toFun := ⋯, continuous_invFun := ⋯ }

@[simp]

theorem ContinuousMulEquiv.quotientCongr_mk {G : Type u} {H : Type v} [Group G] [Group H] [TopologicalSpace G] [TopologicalSpace H] (e : G ≃ₜ* H) (N : Subgroup G) (M : Subgroup H) [N.Normal] [M.Normal] (he : Subgroup.map e.toMonoidHom N = M) (g : G) : (e.quotientCongr N M he) ↑g = ↑(e g)

The quotient isomorphism sends the class of an element to the class of its image.

@[simp]

theorem ContinuousMulEquiv.quotientCongr_symm_mk {G : Type u} {H : Type v} [Group G] [Group H] [TopologicalSpace G] [TopologicalSpace H] (e : G ≃ₜ* H) (N : Subgroup G) (M : Subgroup H) [N.Normal] [M.Normal] (he : Subgroup.map e.toMonoidHom N = M) (h : H) : (e.quotientCongr N M he).symm ↑h = ↑(e.symm h)

The inverse quotient isomorphism sends the class of an element to the class of its inverse image.

theorem Subgroup.forall_exists_mem_sInf_of_isChain {A : Type u_1} [Group A] [TopologicalSpace A] [CompactSpace A] {G : Type u_2} [Group G] [TopologicalSpace G] {c : Set (Subgroup (A × G))} (hne : c.Nonempty) (hchain : IsChain (fun (x1 x2 : Subgroup (A × G)) => x1 ≤ x2) c) (hclosed : ∀ K ∈ c, IsClosed ↑K) (hsurj : ∀ K ∈ c, ∀ (g : G), ∃ (a : A), (a, g) ∈ K) (g : G) : ∃ (a : A), (a, g) ∈ sInf c

The intersection of a nonempty chain of closed subgroups of A × G, each projecting onto G, projects onto G when A is compact: the fibre over g is a directed intersection of nonempty compact sets.

theorem Subgroup.exists_minimal_isClosed_le {A : Type u_1} [Group A] [TopologicalSpace A] [CompactSpace A] {G : Type u_2} [Group G] [TopologicalSpace G] (R : Subgroup (A × G)) (hclosed : IsClosed ↑R) (hsurj : ∀ (g : G), ∃ (a : A), (a, g) ∈ R) : ∃ (H : Subgroup (A × G)), Minimal (fun (H : Subgroup (A × G)) => H ≤ R ∧ IsClosed ↑H ∧ ∀ (g : G), ∃ (a : A), (a, g) ∈ H) H

A closed subgroup of A × G projecting onto G, with A compact, contains a minimal closed subgroup projecting onto G.