feat(topology/homeomorph): add (co)map_cocompact (#13861)

Also rename `filter.comap_cocompact` to `filter.comap_cocompact_le`.

src/number_theory/modular.lean

@@ -226,7 +226,7 @@ begin
   { simp only [continuous_pi_iff, fin.forall_fin_two],
     have : ∀ c : ℝ, continuous (λ x : ℝ, c) := λ c, continuous_const,
     exact ⟨⟨continuous_id, @this (-1 : ℤ)⟩, ⟨this (cd 0), this (cd 1)⟩⟩ },
-  refine filter.tendsto.of_tendsto_comp _ (comap_cocompact hmB),
+  refine filter.tendsto.of_tendsto_comp _ (comap_cocompact_le hmB),
   let f₁ : SL(2, ℤ) → matrix (fin 2) (fin 2) ℝ :=
     λ g, matrix.map (↑g : matrix _ _ ℤ) (coe : ℤ → ℝ),
   have cocompact_ℝ_to_cofinite_ℤ_matrix :

src/topology/homeomorph.lean

@@ -174,6 +174,14 @@ h.embedding.is_compact_iff_is_compact_image.symm
 lemma compact_preimage {s : set β} (h : α ≃ₜ β) : is_compact (h ⁻¹' s) ↔ is_compact s :=
 by rw ← image_symm; exact h.symm.compact_image
 
+@[simp] lemma comap_cocompact (h : α ≃ₜ β) : comap h (cocompact β) = cocompact α :=
+(comap_cocompact_le h.continuous).antisymm $
+  (has_basis_cocompact.le_basis_iff (has_basis_cocompact.comap h)).2 $ λ K hK,
+    ⟨h ⁻¹' K, h.compact_preimage.2 hK, subset.rfl⟩
+
+@[simp] lemma map_cocompact (h : α ≃ₜ β) : map h (cocompact α) = cocompact β :=
+by rw [← h.comap_cocompact, map_comap_of_surjective h.surjective]
+
 protected lemma compact_space [compact_space α] (h : α ≃ₜ β) : compact_space β :=
 { compact_univ := by { rw [← image_univ_of_surjective h.surjective, h.compact_image],
     apply compact_space.compact_univ } }

src/topology/subset_properties.lean

@@ -759,7 +759,7 @@ fintype_of_univ_finite (hf.finite_of_compact hne)
 /-- The comap of the cocompact filter on `β` by a continuous function `f : α → β` is less than or
 equal to the cocompact filter on `α`.
 This is a reformulation of the fact that images of compact sets are compact. -/
-lemma filter.comap_cocompact {f : α → β} (hf : continuous f) :
+lemma filter.comap_cocompact_le {f : α → β} (hf : continuous f) :
   (filter.cocompact β).comap f ≤ filter.cocompact α :=
 begin
   rw (filter.has_basis_cocompact.comap f).le_basis_iff filter.has_basis_cocompact,
@@ -974,7 +974,7 @@ type `Π d, κ d` the `filter.Coprod` of filters `filter.cocompact` on `κ d`. -
 lemma filter.Coprod_cocompact {δ : Type*} {κ : δ → Type*} [Π d, topological_space (κ d)] :
   filter.Coprod (λ d, filter.cocompact (κ d)) = filter.cocompact (Π d, κ d) :=
 begin
-  refine le_antisymm (supr_le $ λ i, filter.comap_cocompact (continuous_apply i)) _,
+  refine le_antisymm (supr_le $ λ i, filter.comap_cocompact_le (continuous_apply i)) _,
   refine compl_surjective.forall.2 (λ s H, _),
   simp only [compl_mem_Coprod, filter.mem_cocompact, compl_subset_compl, image_subset_iff] at H ⊢,
   choose K hKc htK using H,