English
The quotient G/N carries a complete uniform structure when G is complete and N is normal, via the induced uniform structure on the quotient.
Русский
Фактор-группа G/N обладает полной униформной структурой, когда G полна и N является нормальной, через индуцированную структуру на фактор-группе.
LaTeX
$$$[UniformSpace G]\land [IsUniformGroup G] \Rightarrow [FirstCountableTopology G] \Rightarrow [CompleteSpace G] \Rightarrow \text{CompleteSpace } (G/N).$$$
Lean4
/-- The quotient `G ⧸ N` of a complete first countable uniform group `G` by a normal subgroup
is itself complete. In contrast to `QuotientGroup.completeSpace'`, in this version `G` is
already equipped with a uniform structure.
[N. Bourbaki, *General Topology*, IX.3.1 Proposition 4][bourbaki1966b]
Even though `G` is equipped with a uniform structure, the quotient `G ⧸ N` does not inherit a
uniform structure, so it is still provided manually via `IsTopologicalGroup.toUniformSpace`.
In the most common use cases, this coincides (definitionally) with the uniform structure on the
quotient obtained via other means. -/
@[to_additive /-- The quotient `G ⧸ N` of a complete first countable uniform additive group
`G` by a normal additive subgroup is itself complete. Consequently, quotients of Banach spaces by
subspaces are complete. In contrast to `QuotientAddGroup.completeSpace'`, in this version
`G` is already equipped with a uniform structure.
[N. Bourbaki, *General Topology*, IX.3.1 Proposition 4][bourbaki1966b]
Even though `G` is equipped with a uniform structure, the quotient `G ⧸ N` does not inherit a
uniform structure, so it is still provided manually via `IsTopologicalAddGroup.toUniformSpace`.
In the most common use case ─ quotients of normed additive commutative groups by subgroups ─
significant care was taken so that the uniform structure inherent in that setting coincides
(definitionally) with the uniform structure provided here. -/
]
instance completeSpace (G : Type u) [Group G] [us : UniformSpace G] [IsUniformGroup G] [FirstCountableTopology G]
(N : Subgroup G) [N.Normal] [hG : CompleteSpace G] :
@CompleteSpace (G ⧸ N) (IsTopologicalGroup.toUniformSpace (G ⧸ N)) :=
by
rw [← @IsUniformGroup.toUniformSpace_eq _ us _ _] at hG
infer_instance
