Lean4
/-- The quotient `G ⧸ N` of a complete first countable topological group `G` by a normal subgroup
is itself complete. [N. Bourbaki, *General Topology*, IX.3.1 Proposition 4][bourbaki1966b]
Because a topological group is not equipped with a `UniformSpace` instance by default, we must
explicitly provide it in order to consider completeness. See `QuotientGroup.completeSpace` for a
version in which `G` is already equipped with a uniform structure. -/
@[to_additive /-- The quotient `G ⧸ N` of a complete first countable topological additive group
`G` by a normal additive subgroup is itself complete. Consequently, quotients of Banach spaces by
subspaces are complete. [N. Bourbaki, *General Topology*, IX.3.1 Proposition 4][bourbaki1966b]
Because an additive topological group is not equipped with a `UniformSpace` instance by default,
we must explicitly provide it in order to consider completeness. See
`QuotientAddGroup.completeSpace` for a version in which `G` is already equipped with a uniform
structure. -/
]
instance completeSpace' (G : Type u) [Group G] [TopologicalSpace G] [IsTopologicalGroup G] [FirstCountableTopology G]
(N : Subgroup G) [N.Normal] [@CompleteSpace G (IsTopologicalGroup.toUniformSpace G)] :
@CompleteSpace (G ⧸ N) (IsTopologicalGroup.toUniformSpace (G ⧸ N)) := by
/- Since `G ⧸ N` is a topological group it is a uniform space, and since `G` is first countable
the uniformities of both `G` and `G ⧸ N` are countably generated. Moreover, we may choose a
sequential antitone neighborhood basis `u` for `𝓝 (1 : G)` so that `(u (n + 1)) ^ 2 ⊆ u n`, and
this descends to an antitone neighborhood basis `v` for `𝓝 (1 : G ⧸ N)`. Since `𝓤 (G ⧸ N)` is
countably generated, it suffices to show any Cauchy sequence `x` converges. -/
letI : UniformSpace (G ⧸ N) := IsTopologicalGroup.toUniformSpace (G ⧸ N)
letI : UniformSpace G := IsTopologicalGroup.toUniformSpace G
haveI : (𝓤 (G ⧸ N)).IsCountablyGenerated := comap.isCountablyGenerated _ _
obtain ⟨u, hu, u_mul⟩ := IsTopologicalGroup.exists_antitone_basis_nhds_one G
obtain ⟨hv, v_anti⟩ := hu.map ((↑) : G → G ⧸ N)
rw [← QuotientGroup.nhds_eq N 1, QuotientGroup.mk_one] at hv
refine
UniformSpace.complete_of_cauchySeq_tendsto fun x hx =>
?_
/- Given `n : ℕ`, for sufficiently large `a b : ℕ`, given any lift of `x b`, we can find a lift
of `x a` such that the quotient of the lifts lies in `u n`. -/
have key₀ :
∀ i j : ℕ, ∃ M : ℕ, j < M ∧ ∀ a b : ℕ, M ≤ a → M ≤ b → ∀ g : G, x b = g → ∃ g' : G, g / g' ∈ u i ∧ x a = g' :=
by
have h𝓤GN : (𝓤 (G ⧸ N)).HasBasis (fun _ ↦ True) fun i ↦ {x | x.snd / x.fst ∈ (↑) '' u i} := by
simpa [uniformity_eq_comap_nhds_one'] using hv.comap _
rw [h𝓤GN.cauchySeq_iff] at hx
simp only [mem_setOf_eq, forall_true_left, mem_image] at hx
intro i j
rcases hx i with ⟨M, hM⟩
refine ⟨max j M + 1, (le_max_left _ _).trans_lt (lt_add_one _), fun a b ha hb g hg => ?_⟩
obtain ⟨y, y_mem, hy⟩ :=
hM a (((le_max_right j _).trans (lt_add_one _).le).trans ha) b
(((le_max_right j _).trans (lt_add_one _).le).trans hb)
refine ⟨y⁻¹ * g, by simpa only [div_eq_mul_inv, mul_inv_rev, inv_inv, mul_inv_cancel_left] using y_mem, ?_⟩
rw [QuotientGroup.mk_mul, QuotientGroup.mk_inv, hy, hg, inv_div, div_mul_cancel]
/- Inductively construct a subsequence `φ : ℕ → ℕ` using `key₀` so that if `a b : ℕ` exceed
`φ (n + 1)`, then we may find lifts whose quotients lie within `u n`. -/
set φ : ℕ → ℕ := fun n => Nat.recOn n (choose <| key₀ 0 0) fun k yk => choose <| key₀ (k + 1) yk
have hφ :
∀ n : ℕ,
φ n < φ (n + 1) ∧
∀ a b : ℕ, φ (n + 1) ≤ a → φ (n + 1) ≤ b → ∀ g : G, x b = g → ∃ g' : G, g / g' ∈ u (n + 1) ∧ x a = g' :=
fun n =>
choose_spec
(key₀ (n + 1) (φ n))
/- Inductively construct a sequence `x' n : G` of lifts of `x (φ (n + 1))` such that quotients of
successive terms lie in `x' n / x' (n + 1) ∈ u (n + 1)`. We actually need the proofs that each
term is a lift to construct the next term, so we use a Σ-type. -/
set x' : ∀ n, PSigma fun g : G => x (φ (n + 1)) = g := fun n =>
Nat.recOn n
⟨choose (QuotientGroup.mk_surjective (x (φ 1))), (choose_spec (QuotientGroup.mk_surjective (x (φ 1)))).symm⟩
fun k hk =>
⟨choose <| (hφ k).2 _ _ (hφ (k + 1)).1.le le_rfl hk.fst hk.snd,
(choose_spec <| (hφ k).2 _ _ (hφ (k + 1)).1.le le_rfl hk.fst hk.snd).2⟩
have hx' : ∀ n : ℕ, (x' n).fst / (x' (n + 1)).fst ∈ u (n + 1) := fun n =>
(choose_spec <| (hφ n).2 _ _ (hφ (n + 1)).1.le le_rfl (x' n).fst (x' n).snd).1
/- The sequence `x'` is Cauchy. This is where we exploit the condition on `u`. The key idea
is to show by decreasing induction that `x' m / x' n ∈ u m` if `m ≤ n`. -/
have x'_cauchy : CauchySeq fun n => (x' n).fst :=
by
have h𝓤G : (𝓤 G).HasBasis (fun _ => True) fun i => {x | x.snd / x.fst ∈ u i} := by
simpa [uniformity_eq_comap_nhds_one'] using hu.toHasBasis.comap _
rw [h𝓤G.cauchySeq_iff']
simp only [mem_setOf_eq, forall_true_left]
exact fun m =>
⟨m, fun n hmn =>
Nat.decreasingInduction' (fun k _ _ hk => u_mul k ⟨_, hx' k, _, hk, div_mul_div_cancel _ _ _⟩) hmn
(by simpa only [div_self'] using mem_of_mem_nhds (hu.mem _))⟩
/- Since `G` is complete, `x'` converges to some `x₀`, and so the image of this sequence under
the quotient map converges to `↑x₀`. The image of `x'` is a convergent subsequence of `x`, and
since `x` is Cauchy, this implies it converges. -/
rcases cauchySeq_tendsto_of_complete x'_cauchy with ⟨x₀, hx₀⟩
refine
⟨↑x₀, tendsto_nhds_of_cauchySeq_of_subseq hx (strictMono_nat_of_lt_succ fun n => (hφ (n + 1)).1).tendsto_atTop ?_⟩
convert ((continuous_coinduced_rng : Continuous ((↑) : G → G ⧸ N)).tendsto x₀).comp hx₀
exact funext fun n => (x' n).snd
