refactor(topology/discrete_quotient): review API (#18401)

urkud · urkud · commit d101e93197bb · 2023-02-08T18:27:03.000Z
Backport various changes I made to the API while porting to Lean 4 in leanprover-community/mathlib4#2157. * extend `setoid X`; * require only that the fibers are open in the definition, prove that they are clopen; * golf proofs, reuse lattice structure on `setoid`s; * use bundled continuous maps for `comap`; * swap LHS and RHS in some `simp` lemmas; * generalize the `order_bot` instance from a discrete space to a locally connected space; * prove that a discrete topological space is locally connected.
diff --git a/src/topology/category/Profinite/as_limit.lean b/src/topology/category/Profinite/as_limit.lean
@@ -40,7 +40,7 @@ variables (X : Profinite.{u})
 
 /-- The functor `discrete_quotient X ⥤ Fintype` whose limit is isomorphic to `X`. -/
 def fintype_diagram : discrete_quotient X ⥤ Fintype :=
-{ obj := λ S, Fintype.of S,
+{ obj := λ S, by haveI := fintype.of_finite S; exact Fintype.of S,
   map := λ S T f, discrete_quotient.of_le f.le }
 
 /-- An abbreviation for `X.fintype_diagram ⋙ Fintype_to_Profinite`. -/
@@ -56,9 +56,8 @@ instance is_iso_as_limit_cone_lift :
   is_iso ((limit_cone_is_limit X.diagram).lift X.as_limit_cone) :=
 is_iso_of_bijective _
 begin
-  refine ⟨λ a b, _, λ a, _⟩,
-  { intro h,
-    refine discrete_quotient.eq_of_proj_eq (λ S, _),
+  refine ⟨λ a b h, _, λ a, _⟩,
+  { refine discrete_quotient.eq_of_forall_proj_eq (λ S, _),
     apply_fun (λ f : (limit_cone X.diagram).X, f.val S) at h,
     exact h },
   { obtain ⟨b, hb⟩ := discrete_quotient.exists_of_compat
diff --git a/src/topology/connected.lean b/src/topology/connected.lean
@@ -678,6 +678,10 @@ eq_of_subset_of_subset
     (set.mem_of_mem_of_subset mem_connected_component
       (is_connected_connected_component.subset_connected_component h)))
 
+theorem connected_component_eq_iff_mem {x y : α} :
+  connected_component x = connected_component y ↔ x ∈ connected_component y :=
+⟨λ h, h ▸ mem_connected_component, λ h, (connected_component_eq h).symm⟩
+
 lemma connected_component_in_eq {x y : α} {F : set α} (h : y ∈ connected_component_in F x) :
   connected_component_in F x = connected_component_in F y :=
 begin
@@ -1168,6 +1172,14 @@ begin
                 λ ⟨V, ⟨hV, hxV, _⟩, hVU⟩, mem_nhds_iff.mpr ⟨V, hVU, hV, hxV⟩⟩⟩ }
 end
 
+/-- A space with discrete topology is a locally connected space. -/
+@[priority 100]
+instance discrete_topology.to_locally_connected_space (α) [topological_space α]
+  [discrete_topology α] : locally_connected_space α :=
+locally_connected_space_iff_open_connected_subsets.2 $ λ x _U hU,
+  ⟨{x}, singleton_subset_iff.2 $ mem_of_mem_nhds hU, is_open_discrete _, mem_singleton _,
+    is_connected_singleton⟩
+
 lemma connected_component_in_mem_nhds [locally_connected_space α] {F : set α} {x : α}
   (h : F ∈ 𝓝 x) :
   connected_component_in F x ∈ 𝓝 x :=
@@ -1353,6 +1365,10 @@ begin
   exact mem_connected_component
 end
 
+@[simp] theorem connected_component_eq_singleton [totally_disconnected_space α] (x : α) :
+  connected_component x = {x} :=
+totally_disconnected_space_iff_connected_component_singleton.1 ‹_› x
+
 /-- The image of a connected component in a totally disconnected space is a singleton. -/
 @[simp] lemma continuous.image_connected_component_eq_singleton {β : Type*} [topological_space β]
   [totally_disconnected_space β] {f : α → β} (h : continuous f) (a : α) :
@@ -1463,7 +1479,7 @@ not_congr coe_eq_coe
 
 lemma coe_eq_coe' {x y : α} :
   (x : connected_components α) = y ↔ x ∈ connected_component y :=
-coe_eq_coe.trans ⟨λ h, h ▸ mem_connected_component, λ h, (connected_component_eq h).symm⟩
+coe_eq_coe.trans connected_component_eq_iff_mem
 
 instance [inhabited α] : inhabited (connected_components α) := ⟨↑(default : α)⟩
 
diff --git a/src/topology/discrete_quotient.lean b/src/topology/discrete_quotient.lean
