Strict Group Homomorphisms

In this file, we study homomorphisms of topological groups which are strict in the sense of Topology.IsStrictMap.

We provide specialized variations of general facts about IsStrictMap for convenience. But we also show that strict group homomorphisms enjoy some extra properties compared to general strict maps. Namely, we provide:

• isStrictMap_iff_isOpenQuotientMap_rangeRestrict: f is a strict group homomorphism if and only if the rangeRestrict of f is an open quotient map. This ultimately relies on MonoidHom.isOpenQuotientMap_of_isQuotientMap.
• isStrictMap_prodMap: The product (in the sense of MonoidHom.prodMap) of strict group homomorphisms is strict. Note that this result is false for general maps; what makes things work in our context is that, unlike IsQuotientMap, IsOpenQuotientMap is stable under product.

theorem MonoidHom.isStrictMap_iff_isEmbedding_kerLift {G : Type u_1} {H : Type u_2} [Group G] [Group H] {f : G →* H} [TopologicalSpace G] [TopologicalSpace H] : Topology.IsStrictMap ⇑f ↔ Topology.IsEmbedding ⇑(QuotientGroup.kerLift f)

A group homomorphism is strict if and only if its QuotientGroup.kerLift is an embedding.

theorem AddMonoidHom.isStrictMap_iff_isEmbedding_kerLift {G : Type u_1} {H : Type u_2} [AddGroup G] [AddGroup H] {f : G →+ H} [TopologicalSpace G] [TopologicalSpace H] : Topology.IsStrictMap ⇑f ↔ Topology.IsEmbedding ⇑(QuotientAddGroup.kerLift f)

An additive group homomorphism is strict if and only if its QuotientAddGroup.kerLift is an embedding.

theorem MonoidHom.isStrictMap_iff_isHomeomorph_quotientKerEquivRange {G : Type u_1} {H : Type u_2} [Group G] [Group H] {f : G →* H} [TopologicalSpace G] [TopologicalSpace H] : Topology.IsStrictMap ⇑f ↔ IsHomeomorph ⇑(QuotientGroup.quotientKerEquivRange f)

A group homomorphism is strict if and only if the canonical isomorphism G ⧸ f.ker ≃ f.range is a homeomorphism.

theorem AddMonoidHom.isStrictMap_iff_isHomeomorph_quotientKerEquivRange {G : Type u_1} {H : Type u_2} [AddGroup G] [AddGroup H] {f : G →+ H} [TopologicalSpace G] [TopologicalSpace H] : Topology.IsStrictMap ⇑f ↔ IsHomeomorph ⇑(QuotientAddGroup.quotientKerEquivRange f)

An additive group homomorphism is strict if and only if the canonical isomorphism G ⧸ f.ker ≃ f.range is a homeomorphism.

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

The isomorphism of topological groups G ⧸ f.ker ≃ f.range given by a strict group homomorphism f. This is an avatar of the first isomorphism theorem.

Equations

• ContinuousMulEquiv.quotientKerEquivRange hf = { toMulEquiv := QuotientGroup.quotientKerEquivRange f, continuous_toFun := ⋯, continuous_invFun := ⋯ }

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

The isomorphism of topological additive groups G ⧸ f.ker ≃ f.range given by a strict additive group homomorphism f. This is an avatar of the first isomorphism theorem.

Equations

• ContinuousAddEquiv.quotientKerEquivRange hf = { toAddEquiv := QuotientAddGroup.quotientKerEquivRange f, continuous_toFun := ⋯, continuous_invFun := ⋯ }

theorem MonoidHom.isStrictMap_iff_isOpenQuotientMap_rangeRestrict {G : Type u_1} {H : Type u_2} [Group G] [Group H] {f : G →* H} [TopologicalSpace G] [TopologicalSpace H] [IsTopologicalGroup G] : Topology.IsStrictMap ⇑f ↔ IsOpenQuotientMap ⇑f.rangeRestrict

A group homomorphism is strict if and only if its rangeRestrict is an open quotient map.

theorem AddMonoidHom.isStrictMap_iff_isOpenQuotientMap_rangeRestrict {G : Type u_1} {H : Type u_2} [AddGroup G] [AddGroup H] {f : G →+ H} [TopologicalSpace G] [TopologicalSpace H] [IsTopologicalAddGroup G] : Topology.IsStrictMap ⇑f ↔ IsOpenQuotientMap ⇑f.rangeRestrict

An additive group homomorphism is strict if and only if its rangeRestrict is an open quotient map.

theorem MonoidHom.isStrictMap_prodMap_iff {G : Type u_1} {H : Type u_2} {G' : Type u_3} {H' : Type u_4} [Group G'] [Group H'] [Group G] [Group H] {f : G →* H} {g : G' →* H'} [TopologicalSpace G] [TopologicalSpace H] [IsTopologicalGroup G] [TopologicalSpace G'] [IsTopologicalGroup G'] [TopologicalSpace H'] : Topology.IsStrictMap ⇑(f.prodMap g) ↔ Topology.IsStrictMap ⇑f ∧ Topology.IsStrictMap ⇑g

The product (in the sense of MonoidHom.prodMap) of group homomorphisms is strict if and only if both homomorphisms are strict.

theorem AddMonoidHom.isStrictMap_prodMap_iff {G : Type u_1} {H : Type u_2} {G' : Type u_3} {H' : Type u_4} [AddGroup G'] [AddGroup H'] [AddGroup G] [AddGroup H] {f : G →+ H} {g : G' →+ H'} [TopologicalSpace G] [TopologicalSpace H] [IsTopologicalAddGroup G] [TopologicalSpace G'] [IsTopologicalAddGroup G'] [TopologicalSpace H'] : Topology.IsStrictMap ⇑(f.prodMap g) ↔ Topology.IsStrictMap ⇑f ∧ Topology.IsStrictMap ⇑g

The product (in the sense of AddMonoidHom.prodMap) of additive group homomorphisms is strict if and only if both homomorphisms are strict.

theorem MonoidHom.isStrictMap_prodMap {G : Type u_1} {H : Type u_2} {G' : Type u_3} {H' : Type u_4} [Group G'] [Group H'] [Group G] [Group H] {f : G →* H} {g : G' →* H'} [TopologicalSpace G] [TopologicalSpace H] [IsTopologicalGroup G] [TopologicalSpace G'] [IsTopologicalGroup G'] [TopologicalSpace H'] (hf : Topology.IsStrictMap ⇑f) (hg : Topology.IsStrictMap ⇑g) : Topology.IsStrictMap ⇑(f.prodMap g)

The product (in the sense of MonoidHom.prodMap) of strict group homomorphisms is strict.

theorem AddMonoidHom.isStrictMap_prodMap {G : Type u_1} {H : Type u_2} {G' : Type u_3} {H' : Type u_4} [AddGroup G'] [AddGroup H'] [AddGroup G] [AddGroup H] {f : G →+ H} {g : G' →+ H'} [TopologicalSpace G] [TopologicalSpace H] [IsTopologicalAddGroup G] [TopologicalSpace G'] [IsTopologicalAddGroup G'] [TopologicalSpace H'] (hf : Topology.IsStrictMap ⇑f) (hg : Topology.IsStrictMap ⇑g) : Topology.IsStrictMap ⇑(f.prodMap g)

The product (in the sense of AddMonoidHom.prodMap) of strict additive group homomorphisms is strict.