The topological first isomorphism theorem

A surjective strict homomorphism of topological groups f : G →* H induces an isomorphism of topological groups G ⧸ f.ker ≃ₜ* H: the kernel lift of a strict homomorphism is an embedding (Mathlib's MonoidHom.isStrictMap_iff_isEmbedding_kerLift), and a surjective embedding is a homeomorphism. This is Mathlib's ContinuousMulEquiv.quotientKerEquivRange with the range replaced by the whole target.

A continuous surjection from a compact group to a Hausdorff group is a closed map, hence strict, so it is a special case; that case permits changing the quotient model in profinite extensions.

Main definitions

• ContinuousMulEquiv.quotientKerEquivOfSurjective and ContinuousAddEquiv.quotientKerEquivOfSurjective: the isomorphism G ⧸ f.ker ≃ₜ* H induced by a surjective strict homomorphism f, with the evaluation lemmas quotientKerEquivOfSurjective_apply_mk and quotientKerEquivOfSurjective_symm_apply.
• ContinuousMonoidHom.quotientKerEquivOfSurjective: the case of a continuous surjection from a compact group to a Hausdorff group.

References

• N. Bourbaki, General Topology, Chapters 1–4, Springer (1989), Chapter III (Topological groups), § 2 (Subgroups, quotient groups, homomorphisms of topological groups).

noncomputable def ContinuousMulEquiv.quotientKerEquivOfSurjective {G : Type u_1} {H : Type u_2} [Group G] [Group H] [TopologicalSpace G] [TopologicalSpace H] (f : G →* H) (hf : Topology.IsStrictMap ⇑f) (hs : Function.Surjective ⇑f) : G ⧸ f.ker ≃ₜ* H

The first isomorphism theorem for a surjective strict homomorphism of topological groups: G ⧸ f.ker ≃ₜ* H.

noncomputable def ContinuousAddEquiv.quotientKerEquivOfSurjective {G : Type u_1} {H : Type u_2} [AddGroup G] [AddGroup H] [TopologicalSpace G] [TopologicalSpace H] (f : G →+ H) (hf : Topology.IsStrictMap ⇑f) (hs : Function.Surjective ⇑f) : G ⧸ f.ker ≃ₜ+ H

The first isomorphism theorem for a surjective strict homomorphism of topological additive groups: G ⧸ f.ker ≃ₜ+ H.

@[simp]

theorem ContinuousMulEquiv.quotientKerEquivOfSurjective_apply_mk {G : Type u_1} {H : Type u_2} [Group G] [Group H] [TopologicalSpace G] [TopologicalSpace H] (f : G →* H) (hf : Topology.IsStrictMap ⇑f) (hs : Function.Surjective ⇑f) (x : G) : (quotientKerEquivOfSurjective f hf hs) ↑x = f x

The quotient isomorphism evaluates on the class of x as f x.

@[simp]

theorem ContinuousAddEquiv.quotientKerEquivOfSurjective_apply_mk {G : Type u_1} {H : Type u_2} [AddGroup G] [AddGroup H] [TopologicalSpace G] [TopologicalSpace H] (f : G →+ H) (hf : Topology.IsStrictMap ⇑f) (hs : Function.Surjective ⇑f) (x : G) : (quotientKerEquivOfSurjective f hf hs) ↑x = f x

The quotient isomorphism evaluates on the class of x as f x.

@[simp]

theorem ContinuousMulEquiv.quotientKerEquivOfSurjective_symm_apply {G : Type u_1} {H : Type u_2} [Group G] [Group H] [TopologicalSpace G] [TopologicalSpace H] (f : G →* H) (hf : Topology.IsStrictMap ⇑f) (hs : Function.Surjective ⇑f) (x : G) : (quotientKerEquivOfSurjective f hf hs).symm (f x) = ↑x

The inverse of the quotient isomorphism sends f x to the class of x.

@[simp]

theorem ContinuousAddEquiv.quotientKerEquivOfSurjective_symm_apply {G : Type u_1} {H : Type u_2} [AddGroup G] [AddGroup H] [TopologicalSpace G] [TopologicalSpace H] (f : G →+ H) (hf : Topology.IsStrictMap ⇑f) (hs : Function.Surjective ⇑f) (x : G) : (quotientKerEquivOfSurjective f hf hs).symm (f x) = ↑x

The inverse of the quotient isomorphism sends f x to the class of x.

noncomputable def ContinuousMonoidHom.quotientKerEquivOfSurjective {G : Type u_1} {H : Type u_2} [Group G] [TopologicalSpace G] [CompactSpace G] [Group H] [TopologicalSpace H] [T2Space H] (f : G →ₜ* H) (hf : Function.Surjective ⇑f) : G ⧸ (↑f).ker ≃ₜ* H

The first isomorphism theorem for a continuous surjection from a compact group to a Hausdorff group, with the quotient topology on the source.

@[simp]

theorem ContinuousMonoidHom.quotientKerEquivOfSurjective_apply_mk {G : Type u_1} {H : Type u_2} [Group G] [TopologicalSpace G] [CompactSpace G] [Group H] [TopologicalSpace H] [T2Space H] (f : G →ₜ* H) (hf : Function.Surjective ⇑f) (x : G) : (f.quotientKerEquivOfSurjective hf) ↑x = f x

The topological first isomorphism theorem sends the class of x to f x.

@[simp]

theorem ContinuousMonoidHom.quotientKerEquivOfSurjective_symm_apply {G : Type u_1} {H : Type u_2} [Group G] [TopologicalSpace G] [CompactSpace G] [Group H] [TopologicalSpace H] [T2Space H] (f : G →ₜ* H) (hf : Function.Surjective ⇑f) (x : G) : (f.quotientKerEquivOfSurjective hf).symm (f x) = ↑x

The inverse of the topological first isomorphism theorem sends f x to the class of x.