Right uniformities and homomorphisms

The canonical right uniformity makes a topological group a right-uniform group. An inducing homomorphism between right-uniform groups is uniformly inducing, so an embedding homomorphism is a uniform embedding. These facts let topological group isomorphisms transport completeness without requiring two-sided uniformities.

The inducing and embedding lemmas generalize Mathlib's MonoidHom.isUniformInducing_of_isInducing and MonoidHom.isUniformEmbedding_of_isEmbedding from uniform groups to right-uniform groups. All results also have additive forms.

theorem IsTopologicalGroup.isRightUniformGroup (G : Type u_1) [Group G] [TopologicalSpace G] [IsTopologicalGroup G] : IsRightUniformGroup G

The canonical right uniformity on a topological group makes it a right-uniform group.

theorem IsTopologicalAddGroup.isRightUniformAddGroup (G : Type u_1) [AddGroup G] [TopologicalSpace G] [IsTopologicalAddGroup G] : IsRightUniformAddGroup G

The canonical right uniformity on a topological additive group makes it a right-uniform additive group.

theorem MonoidHom.isUniformInducing_of_isInducing_right {G : Type u_1} {H : Type u_2} {F : Type u_3} [Group G] [UniformSpace G] [IsRightUniformGroup G] [Group H] [UniformSpace H] [IsRightUniformGroup H] [FunLike F G H] [MonoidHomClass F G H] {f : F} (hf : Topology.IsInducing ⇑f) : IsUniformInducing ⇑f

An inducing homomorphism between right-uniform groups is uniformly inducing.

theorem AddMonoidHom.isUniformInducing_of_isInducing_right {G : Type u_1} {H : Type u_2} {F : Type u_3} [AddGroup G] [UniformSpace G] [IsRightUniformAddGroup G] [AddGroup H] [UniformSpace H] [IsRightUniformAddGroup H] [FunLike F G H] [AddMonoidHomClass F G H] {f : F} (hf : Topology.IsInducing ⇑f) : IsUniformInducing ⇑f

An inducing homomorphism between right-uniform additive groups is uniformly inducing.

theorem MonoidHom.isUniformEmbedding_of_isEmbedding_right {G : Type u_1} {H : Type u_2} {F : Type u_3} [Group G] [UniformSpace G] [IsRightUniformGroup G] [Group H] [UniformSpace H] [IsRightUniformGroup H] [FunLike F G H] [MonoidHomClass F G H] {f : F} (hf : Topology.IsEmbedding ⇑f) : IsUniformEmbedding ⇑f

An embedding homomorphism between right-uniform groups is a uniform embedding.

theorem AddMonoidHom.isUniformEmbedding_of_isEmbedding_right {G : Type u_1} {H : Type u_2} {F : Type u_3} [AddGroup G] [UniformSpace G] [IsRightUniformAddGroup G] [AddGroup H] [UniformSpace H] [IsRightUniformAddGroup H] [FunLike F G H] [AddMonoidHomClass F G H] {f : F} (hf : Topology.IsEmbedding ⇑f) : IsUniformEmbedding ⇑f

An embedding homomorphism between right-uniform additive groups is a uniform embedding.