feat(topology/algebra/uniform_group): the quotient of a first countab…

…le complete topological group by a normal subgroup is itself complete (#16368)

docs/references.bib

@@ -251,6 +251,17 @@ @Book{            bourbaki1966
   mrnumber      = {0205210}
 }
 
+@Book{            bourbaki1966b,
+  author        = {Bourbaki, Nicolas},
+  title         = {Elements of mathematics. {G}eneral topology. {P}art 2},
+  publisher     = {Hermann, Paris; Addison-Wesley Publishing Co., Reading,
+                  Mass.-London-Don Mills, Ont.},
+  year          = {1966},
+  pages         = {iv+363},
+  mrclass       = {54-02 (00A05 54-01)},
+  mrnumber      = {979295},
+}
+
 @Book{            bourbaki1968,
   author        = {Bourbaki, Nicolas},
   title         = {Lie groups and {L}ie algebras. {C}hapters 4--6},

src/order/filter/bases.lean

@@ -954,6 +954,11 @@ begin
     ⟨hs.to_has_basis.inf ht.to_has_basis, set.to_countable _⟩
 end
 
+instance map.is_countably_generated (l : filter α) [l.is_countably_generated] (f : α → β) :
+  (map f l).is_countably_generated :=
+let ⟨x, hxl⟩ := l.exists_antitone_basis in
+has_countable_basis.is_countably_generated ⟨hxl.map.to_has_basis, to_countable _⟩
+
 instance comap.is_countably_generated (l : filter β) [l.is_countably_generated] (f : α → β) :
   (comap f l).is_countably_generated :=
 let ⟨x, hxl⟩ := l.exists_antitone_basis in

src/topology/algebra/group.lean

@@ -749,6 +749,47 @@ instance topological_group_quotient [N.normal] : topological_group (G ⧸ N) :=
   end,
   continuous_inv := by convert (@continuous_inv G _ _ _).quotient_map' _ }
 
+/-- Neighborhoods in the quotient are precisely the map of neighborhoods in the prequotient. -/
+@[to_additive "Neighborhoods in the quotient are precisely the map of neighborhoods in
+the prequotient."]
+lemma quotient_group.nhds_eq (x : G) : 𝓝 (x : G ⧸ N) = map coe (𝓝 x) :=
+le_antisymm ((quotient_group.is_open_map_coe N).nhds_le x) continuous_quot_mk.continuous_at
+
+variables (G) [first_countable_topology G]
+
+/-- Any first countable topological group has an antitone neighborhood basis `u : ℕ → set G` for
+which `(u (n + 1)) ^ 2 ⊆ u n`. The existence of such a neighborhood basis is a key tool for
+`quotient_group.complete_space` -/
+@[to_additive "Any first countable topological additive group has an antitone neighborhood basis
+`u : ℕ → set G` for which `u (n + 1) + u (n + 1) ⊆ u n`. The existence of such a neighborhood basis
+is a key tool for `quotient_add_group.complete_space`"]
+lemma topological_group.exists_antitone_basis_nhds_one :
+  ∃ (u : ℕ → set G), (𝓝 1).has_antitone_basis u ∧ (∀ n, u (n + 1) * u (n + 1) ⊆ u n) :=
+begin
+  rcases (𝓝 (1 : G)).exists_antitone_basis with ⟨u, hu, u_anti⟩,
+  have := ((hu.prod_nhds hu).tendsto_iff hu).mp
+    (by simpa only [mul_one] using continuous_mul.tendsto ((1, 1) : G × G)),
+  simp only [and_self, mem_prod, and_imp, prod.forall, exists_true_left, prod.exists,
+    forall_true_left] at this,
+  have event_mul : ∀ n : ℕ, ∀ᶠ m in at_top, u m * u m ⊆ u n,
+  { intros n,
+    rcases this n with ⟨j, k, h⟩,
+    refine at_top_basis.eventually_iff.mpr ⟨max j k, true.intro, λ m hm, _⟩,
+    rintro - ⟨a, b, ha, hb, rfl⟩,
+    exact h a b (u_anti ((le_max_left _ _).trans hm) ha) (u_anti ((le_max_right _ _).trans hm) hb)},
+  obtain ⟨φ, -, hφ, φ_anti_basis⟩ := has_antitone_basis.subbasis_with_rel ⟨hu, u_anti⟩ event_mul,
+  exact ⟨u ∘ φ, φ_anti_basis, λ n, hφ n.lt_succ_self⟩,
+end
+
+include n
+
+/-- In a first countable topological group `G` with normal subgroup `N`, `1 : G ⧸ N` has a
+countable neighborhood basis. -/
+@[to_additive "In a first countable topological additive group `G` with normal additive subgroup
+`N`, `0 : G ⧸ N` has a countable neighborhood basis."]
+instance quotient_group.nhds_one_is_countably_generated : (𝓝 (1 : G ⧸ N)).is_countably_generated :=
+(quotient_group.nhds_eq N 1).symm ▸ map.is_countably_generated _ _
+
 end quotient_topological_group
 
 /-- A typeclass saying that `λ p : G × G, p.1 - p.2` is a continuous function. This property

src/topology/algebra/uniform_group.lean

@@ -27,6 +27,10 @@ group naturally induces a uniform structure.
   to construct a canonical uniformity for a topological add group.
 
 * extension of ℤ-bilinear maps to complete groups (useful for ring completions)
+
+* `quotient_group.complete_space` and `quotient_add_group.complete_space` guarantee that quotients
+  of first countable topological groups by normal subgroups are themselves complete. In particular,
+  the quotient of a Banach space by a subspace is complete.
 -/
 
 noncomputable theory
@@ -745,3 +749,118 @@ begin
       apply h ; tauto } }
 end
 end dense_inducing
+
+section complete_quotient
+
+universe u
+open topological_space classical
+
+/-- 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 `uniform_space` instance by default, we must
+explicitly provide it in order to consider completeness. See `quotient_group.complete_space` 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 `uniform_space` instance by default,
+we must explicitly provide it in order to consider completeness. See
+`quotient_add_group.complete_space` for a version in which `G` is already equipped with a uniform
+structure."]
+instance quotient_group.complete_space' (G : Type u) [group G] [topological_space G]
+  [topological_group G] [first_countable_topology G] (N : subgroup G) [N.normal]
+  [@complete_space G (topological_group.to_uniform_space G)] :
+  @complete_space (G ⧸ N) (topological_group.to_uniform_space (G ⧸ N)) :=
+begin
+  /- 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 : uniform_space (G ⧸ N) := topological_group.to_uniform_space (G ⧸ N),
+  letI : uniform_space G := topological_group.to_uniform_space G,
+  haveI : (𝓤 (G ⧸ N)).is_countably_generated := comap.is_countably_generated _ _,
+  obtain ⟨u, hu, u_mul⟩ := topological_group.exists_antitone_basis_nhds_one G,
+  obtain ⟨hv, v_anti⟩ := @has_antitone_basis.map _ _ _ _ _ _ (coe : G → G ⧸ N) hu,
+  rw [←quotient_group.nhds_eq N 1, quotient_group.coe_one] at hv,
+  refine uniform_space.complete_of_cauchy_seq_tendsto (λ 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',
+  { have h𝓤GN : (𝓤 (G ⧸ N)).has_basis (λ _, true) (λ i, {x | x.snd / x.fst ∈ coe '' u i}),
+    { simpa [uniformity_eq_comap_nhds_one'] using hv.comap _ },
+    simp only [h𝓤GN.cauchy_seq_iff, ge_iff_le, mem_set_of_eq, forall_true_left, mem_image] at hx,
+    intros i j,
+    rcases hx i with ⟨M, hM⟩,
+    refine ⟨max j M + 1, (le_max_left _ _).trans_lt (lt_add_one _), λ 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 [quotient_group.coe_mul, quotient_group.coe_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 φ : ℕ → ℕ := λ n, nat.rec_on n (some $ key₀ 0 0) (λ k yk, some $ 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'),
+    from λ n, some_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 (λ g : G, x (φ (n + 1)) = g) :=
+    λ n, nat.rec_on n
+      ⟨some (quotient_group.mk_surjective (x (φ 1))),
+       (some_spec (quotient_group.mk_surjective (x (φ 1)))).symm⟩
+      (λ k hk, ⟨some $ (hφ k).2 _ _ (hφ (k + 1)).1.le le_rfl hk.fst hk.snd,
+          (some_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) :=
+    λ n, (some_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 : cauchy_seq (λ n, (x' n).fst),
+  { have h𝓤G : (𝓤 G).has_basis (λ _, true) (λ i, {x | x.snd / x.fst ∈ u i}),
+    { simpa [uniformity_eq_comap_nhds_one'] using hu.to_has_basis.comap _ },
+    simp only [h𝓤G.cauchy_seq_iff', ge_iff_le, mem_set_of_eq, forall_true_left],
+    exact λ m, ⟨m, λ n hmn, nat.decreasing_induction'
+      (λ k hkn hkm 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 cauchy_seq_tendsto_of_complete x'_cauchy with ⟨x₀, hx₀⟩,
+  refine ⟨↑x₀, tendsto_nhds_of_cauchy_seq_of_subseq hx
+    (strict_mono_nat_of_lt_succ $ λ n, (hφ (n + 1)).1).tendsto_at_top _⟩,
+  convert ((continuous_coinduced_rng : continuous (coe : G → G ⧸ N)).tendsto x₀).comp hx₀,
+  exact funext (λ n, (x' n).snd),
+end
+
+/-- The quotient `G ⧸ N` of a complete first countable uniform group `G` by a normal subgroup
+is itself complete. In constrast to `quotient_group.complete_space'`, 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 `topological_group.to_uniform_space`.
+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 constrast to `quotient_add_group.complete_space'`, 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 `topological_add_group.to_uniform_space`.
+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 quotient_group.complete_space (G : Type u) [group G] [us : uniform_space G]
+  [uniform_group G] [first_countable_topology G] (N : subgroup G) [N.normal]
+  [hG : complete_space G] : @complete_space (G ⧸ N) (topological_group.to_uniform_space (G ⧸ N)) :=
+by { unfreezingI { rw ←@uniform_group.to_uniform_space_eq _ us _ _ at hG }, apply_instance }
+
+
+end complete_quotient