Completeness of open quotients of right-uniform groups

Mathlib's QuotientGroup.completeSpace_right makes the quotient G ⧸ N of a complete first countable right-uniform group complete for its right uniformity. A group H receiving an open quotient map f : G → H is that quotient in disguise: the induced isomorphism G ⧸ ker f ≃* H is a homeomorphism, hence a uniform embedding for the right uniformities. Consequently H is complete. No commutativity is needed.

This is the form in which completeness is needed for a ring presented as an open quotient of a complete ring, such as an algebra topologically of finite type over a Tate ring.

Main results

• IsOpenQuotientMap.completeSpace_mul: a right-uniform group admitting an open quotient map from a complete first countable right-uniform group is complete.
• IsOpenQuotientMap.completeSpace: the additive counterpart.

References

• [N. Bourbaki, General Topology][bourbaki1966b], IX.3.1 Proposition 4.

theorem IsOpenQuotientMap.completeSpace_mul {G : Type u_1} {H : Type u_2} [Group G] [UniformSpace G] [IsRightUniformGroup G] [CompleteSpace G] [FirstCountableTopology G] [Group H] [UniformSpace H] [IsRightUniformGroup H] {F : Type u_3} [FunLike F G H] [MonoidHomClass F G H] {f : F} (hf : IsOpenQuotientMap ⇑f) : CompleteSpace H

An open quotient of a complete first countable right-uniform group is complete. If f : G → H is a continuous open surjective homomorphism, G is complete and first countable, and H is a right-uniform group, then H is complete.

theorem IsOpenQuotientMap.completeSpace {G : Type u_1} {H : Type u_2} [AddGroup G] [UniformSpace G] [IsRightUniformAddGroup G] [CompleteSpace G] [FirstCountableTopology G] [AddGroup H] [UniformSpace H] [IsRightUniformAddGroup H] {F : Type u_3} [FunLike F G H] [AddMonoidHomClass F G H] {f : F} (hf : IsOpenQuotientMap ⇑f) : CompleteSpace H

An open quotient of a complete first countable right-uniform additive group is complete. If f : G → H is a continuous open surjective additive homomorphism, G is complete and first countable, and H is a right-uniform additive group, then H is complete.