Short exact sequences of topological groups

In this file, we define a short exact sequence of topological groups to be a closed embedding φ followed by an open quotient map ψ satisfying φ.range = ψ.ker.

Main definitions

• TopologicalGroup.IsSES φ ψ: A predicate stating that φ is a closed embedding, ψ is an open quotient map, and φ.range = ψ.ker.

structure TopologicalGroup.IsSES {A : Type u_1} {B : Type u_2} {C : Type u_3} [Group A] [Group B] [Group C] [TopologicalSpace A] [TopologicalSpace B] [TopologicalSpace C] (φ : A →* B) (ψ : B →* C) : Prop

A predicate stating that φ and ψ define a short exact sequence of topological groups.

• isClosedEmbedding : Topology.IsClosedEmbedding ⇑φ
• isOpenQuotientMap : IsOpenQuotientMap ⇑ψ
• mulExact : Function.MulExact ⇑φ ⇑ψ

structure TopologicalAddGroup.IsSES {A : Type u_1} {B : Type u_2} {C : Type u_3} [AddGroup A] [AddGroup B] [AddGroup C] [TopologicalSpace A] [TopologicalSpace B] [TopologicalSpace C] (φ : A →+ B) (ψ : B →+ C) : Prop

A predicate stating that φ and ψ define a short exact sequence of topological groups.

• isClosedEmbedding : Topology.IsClosedEmbedding ⇑φ
• isOpenQuotientMap : IsOpenQuotientMap ⇑ψ
• exact : Function.Exact ⇑φ ⇑ψ

theorem TopologicalGroup.IsSES.ofClosedSubgroup {G : Type u_1} [Group G] [TopologicalSpace G] [IsTopologicalGroup G] (H : Subgroup G) [H.Normal] (hH : IsClosed ↑H) : IsSES H.subtype (QuotientGroup.mk' H)

Construct a short exact sequence of topological groups from a closed normal subgroup.

theorem TopologicalAddGroup.IsSES.ofClosedAddSubgroup {G : Type u_1} [AddGroup G] [TopologicalSpace G] [IsTopologicalAddGroup G] (H : AddSubgroup G) [H.Normal] (hH : IsClosed ↑H) : IsSES H.subtype (QuotientAddGroup.mk' H)

Construct a short exact sequence of topological groups from a closed normal subgroup.