feat(topology/connected.lean): define pi_0 and prove basic properties (#6188)

Define and prove basic properties of pi_0, the functor quotienting a space by its connected components. 

For dot notation convenience, this PR renames `subset_connected_component` to `is_preconnected.subset_connected_component` and also defines the weaker version `is_connected.subset_connected_component`.



Co-authored-by: Bryan Gin-ge Chen <bryangingechen@gmail.com>

Author: callesonne

src/topology/connected.lean

@@ -198,25 +198,48 @@ def connected_component_in (F : set α) (x : F) : set α := coe '' (connected_co
 theorem mem_connected_component {x : α} : x ∈ connected_component x :=
 mem_sUnion_of_mem (mem_singleton x) ⟨is_connected_singleton.is_preconnected, mem_singleton x⟩
 
+theorem is_preconnected_connected_component {x : α} : is_preconnected (connected_component x) :=
+is_preconnected_sUnion x _ (λ _, and.right) (λ _, and.left)
+
 theorem is_connected_connected_component {x : α} : is_connected (connected_component x) :=
-⟨⟨x, mem_connected_component⟩, is_preconnected_sUnion x _ (λ _, and.right) (λ _, and.left)⟩
+⟨⟨x, mem_connected_component⟩, is_preconnected_connected_component⟩
 
-theorem subset_connected_component {x : α} {s : set α} (H1 : is_preconnected s) (H2 : x ∈ s) :
-  s ⊆ connected_component x :=
+theorem is_preconnected.subset_connected_component {x : α} {s : set α}
+  (H1 : is_preconnected s) (H2 : x ∈ s) : s ⊆ connected_component x :=
 λ z hz, mem_sUnion_of_mem hz ⟨H1, H2⟩
 
+theorem is_connected.subset_connected_component {x : α} {s : set α}
+  (H1 : is_connected s) (H2 : x ∈ s) : s ⊆ connected_component x :=
+H1.2.subset_connected_component H2
+
+theorem connected_component_eq {x y : α} (h : y ∈ connected_component x) :
+  connected_component x = connected_component y :=
+eq_of_subset_of_subset
+  (is_connected_connected_component.subset_connected_component h)
+  (is_connected_connected_component.subset_connected_component
+    (set.mem_of_mem_of_subset mem_connected_component
+      (is_connected_connected_component.subset_connected_component h)))
+
+lemma connected_component_disjoint {x y : α} (h : connected_component x ≠ connected_component y) :
+  disjoint (connected_component x) (connected_component y) :=
+set.disjoint_left.2 (λ a h1 h2, h
+  ((connected_component_eq h1).trans (connected_component_eq h2).symm))
+
 theorem is_closed_connected_component {x : α} :
   is_closed (connected_component x) :=
 closure_eq_iff_is_closed.1 $ subset.antisymm
-  (subset_connected_component
-    is_connected_connected_component.closure.is_preconnected
+  (is_connected_connected_component.closure.subset_connected_component
     (subset_closure mem_connected_component))
   subset_closure
 
+lemma continuous.image_connected_component_subset {β : Type*} [topological_space β] {f : α → β}
+  (h : continuous f) (a : α) : f '' connected_component a ⊆ connected_component (f a) :=
+(is_connected_connected_component.image f h.continuous_on).subset_connected_component
+  ((mem_image f (connected_component a) (f a)).2 ⟨a, mem_connected_component, rfl⟩)
+
 theorem irreducible_component_subset_connected_component {x : α} :
   irreducible_component x ⊆ connected_component x :=
-subset_connected_component
-  is_irreducible_irreducible_component.is_connected.is_preconnected
+is_irreducible_irreducible_component.is_connected.subset_connected_component
   mem_irreducible_component
 
 /-- A preconnected space is one where there is no non-trivial open partition. -/
@@ -246,9 +269,9 @@ begin
   split,
   { rintros ⟨h, ⟨x⟩⟩,
     exactI ⟨x, eq_univ_of_univ_subset $
-      subset_connected_component is_preconnected_univ (mem_univ x)⟩ },
+      is_preconnected_univ.subset_connected_component (mem_univ x)⟩ },
   { rintros ⟨x, h⟩,
-    haveI : preconnected_space α := ⟨by {rw ← h, exact is_connected_connected_component.2 }⟩,
+    haveI : preconnected_space α := ⟨by { rw ← h, exact is_preconnected_connected_component }⟩,
     exact ⟨⟨x⟩⟩ }
 end
 
@@ -489,6 +512,116 @@ begin
   exact h,
 end
 
+/-- The preimage of a connected component is connected if the function has connected fibers
+and a subset is closed iff the preimage is. -/
+lemma preimage_connected_component_connected {β : Type*} [topological_space β] {f : α → β}
+  (connected_fibers : ∀ t : β, is_connected (f ⁻¹' {t}))
+  (hcl : ∀ (T : set β), is_closed T ↔ is_closed (f ⁻¹' T)) (t : β) :
+  is_connected (f ⁻¹' connected_component t) :=
+begin
+  -- The following proof is essentially https://stacks.math.columbia.edu/tag/0377
+  -- although the statement is slightly different
+  have hf : function.surjective f := function.surjective.of_comp (λ t : β, (connected_fibers t).1),
+
+  split,
+  { cases hf t with s hs,
+    use s,
+    rw [mem_preimage, hs],
+    exact mem_connected_component },
+
+  have hT : is_closed (f ⁻¹' connected_component t) :=
+    (hcl (connected_component t)).1 is_closed_connected_component,
+
+  -- To show it's preconnected we decompose (f ⁻¹' connected_component t) as a subset of two
+  -- closed disjoint sets in α. We want to show that it's a subset of either.
+  rw is_preconnected_iff_subset_of_fully_disjoint_closed hT,
+  intros u v hu hv huv uv_disj,
+
+  -- To do this we decompose connected_component t into T₁ and T₂
+  -- we will show that connected_component t is a subset of either and hence
+  -- (f ⁻¹' connected_component t) is a subset of u or v
+  let T₁ := {t' ∈ connected_component t | f ⁻¹' {t'} ⊆ u},
+  let T₂ := {t' ∈ connected_component t | f ⁻¹' {t'} ⊆ v},
+
+  have fiber_decomp : ∀ t' ∈ connected_component t, f ⁻¹' {t'} ⊆ u ∨ f ⁻¹' {t'} ⊆ v,
+  { intros t' ht',
+    apply is_preconnected_iff_subset_of_disjoint_closed.1 (connected_fibers t').2 u v hu hv,
+    { exact subset.trans (hf.preimage_subset_preimage_iff.2 (singleton_subset_iff.2 ht')) huv },
+    rw uv_disj,
+    exact inter_empty _ },
+
+  have T₁_u : f ⁻¹' T₁ = (f ⁻¹' connected_component t) ∩ u,
+  { apply eq_of_subset_of_subset,
+    { rw ←bUnion_preimage_singleton,
+      refine bUnion_subset (λ t' ht', subset_inter _ ht'.2),
+      rw [hf.preimage_subset_preimage_iff, singleton_subset_iff],
+      exact ht'.1 },
+    rintros a ⟨hat, hau⟩,
+    constructor,
+    { exact mem_preimage.1 hat },
+    dsimp only,
+    cases fiber_decomp (f a) (mem_preimage.1 hat),
+    { exact h },
+    { exfalso,
+      rw ←not_nonempty_iff_eq_empty at uv_disj,
+      exact uv_disj (nonempty_of_mem (mem_inter hau (h rfl))) } },
+  -- This proof is exactly the same as the above (modulo some symmetry)
+  have T₂_v : f ⁻¹' T₂ = (f ⁻¹' connected_component t) ∩ v,
+  { apply eq_of_subset_of_subset,
+    { rw ←bUnion_preimage_singleton,
+      refine bUnion_subset (λ t' ht', subset_inter _ ht'.2),
+      rw [hf.preimage_subset_preimage_iff, singleton_subset_iff],
+      exact ht'.1 },
+    rintros a ⟨hat, hav⟩,
+    constructor,
+    { exact mem_preimage.1 hat },
+    dsimp only,
+    cases fiber_decomp (f a) (mem_preimage.1 hat),
+    { exfalso,
+      rw ←not_nonempty_iff_eq_empty at uv_disj,
+      exact uv_disj (nonempty_of_mem (mem_inter (h rfl) hav)) },
+    { exact h } },
+
+  -- Now we show T₁, T₂ are closed, cover connected_component t and are disjoint.
+  have hT₁ : is_closed T₁ := ((hcl T₁).2 (T₁_u.symm ▸ (is_closed_inter hT hu))),
+  have hT₂ : is_closed T₂ := ((hcl T₂).2 (T₂_v.symm ▸ (is_closed_inter hT hv))),
+
+  have T_decomp : connected_component t ⊆ T₁ ∪ T₂,
+  { intros t' ht',
+    rw mem_union t' T₁ T₂,
+    cases fiber_decomp t' ht' with htu htv,
+    { left, exact ⟨ht', htu⟩ },
+    right, exact ⟨ht', htv⟩ },
+
+  have T_disjoint : T₁ ∩ T₂ = ∅,
+  { rw ←image_preimage_eq (T₁ ∩ T₂) hf,
+    suffices : f ⁻¹' (T₁ ∩ T₂) = ∅,
+    { rw this, exact image_empty _ },
+    rw [preimage_inter, T₁_u, T₂_v],
+    rw inter_comm at uv_disj,
+    conv
+    { congr,
+      rw [inter_assoc],
+      congr, skip,
+      rw [←inter_assoc, inter_comm, ←inter_assoc, uv_disj, empty_inter], },
+    exact inter_empty _ },
+
+  -- Now we do cases on whether (connected_component t) is a subset of T₁ or T₂ to show
+  -- that the preimage is a subset of u or v.
+  cases (is_preconnected_iff_subset_of_fully_disjoint_closed is_closed_connected_component).1
+    is_preconnected_connected_component T₁ T₂ hT₁ hT₂ T_decomp T_disjoint,
+  { left,
+    rw subset.antisymm_iff at T₁_u,
+    suffices : f ⁻¹' connected_component t ⊆ f ⁻¹' T₁,
+    { exact subset.trans (subset.trans this T₁_u.1) (inter_subset_right _ _) },
+    exact preimage_mono h },
+  right,
+  rw subset.antisymm_iff at T₂_v,
+  suffices : f ⁻¹' connected_component t ⊆ f ⁻¹' T₂,
+  { exact subset.trans (subset.trans this T₂_v.1) (inter_subset_right _ _) },
+  exact preimage_mono h,
+end
+
 end preconnected
 
 section totally_disconnected
@@ -528,6 +661,61 @@ instance subtype.totally_disconnected_space {α : Type*} {p : α → Prop} [topo
     totally_disconnected_space.is_totally_disconnected_univ (subtype.val '' s) (set.subset_univ _)
       ((is_preconnected.image h2 _) (continuous.continuous_on (@continuous_subtype_val _ _ p))))⟩
 
+/-- A space is totally disconnected iff its connected components are subsingletons. -/
+lemma totally_disconnected_space_iff_connected_component_subsingleton :
+  totally_disconnected_space α ↔ ∀ x : α, subsingleton (connected_component x) :=
+begin
+  split,
+  { intros h x,
+    apply h.1,
+    { exact subset_univ _ },
+    exact is_preconnected_connected_component },
+  intro h, constructor,
+  intros s s_sub hs,
+  rw subsingleton_coe,
+  by_cases s.nonempty,
+  { choose x hx using h,
+    have H := h x,
+    rw subsingleton_coe at H,
+    exact H.mono (hs.subset_connected_component hx) },
+  rw not_nonempty_iff_eq_empty at h,
+  rw h,
+  exact subsingleton_empty,
+end
+
+/-- A space is totally disconnected iff its connected components are singletons. -/
+lemma totally_disconnected_space_iff_connected_component_singleton :
+  totally_disconnected_space α ↔ ∀ x : α, connected_component x = {x} :=
+begin
+  split,
+  { intros h x,
+    rw totally_disconnected_space_iff_connected_component_subsingleton at h,
+    specialize h x,
+    rw subsingleton_coe at h,
+    rw h.eq_singleton_of_mem,
+    exact mem_connected_component },
+  intro h,
+  rw totally_disconnected_space_iff_connected_component_subsingleton,
+  intro x,
+  rw [h x, subsingleton_coe],
+  exact subsingleton_singleton,
+end
+
+/-- 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 : α) :
+  f '' connected_component a = {f a} :=
+begin
+  have ha : subsingleton (f '' connected_component a),
+  { apply _inst_3.1,
+    { exact subset_univ _ },
+    apply is_preconnected_connected_component.image,
+    exact h.continuous_on },
+  rw subsingleton_coe at ha,
+  rw ha.eq_singleton_of_mem,
+  exact ⟨a, mem_connected_component, refl (f a)⟩,
+end
+
 end totally_disconnected
 
 section totally_separated
@@ -568,3 +756,113 @@ instance totally_separated_space.of_discrete
 ⟨λ a _ b _ h, ⟨{b}ᶜ, {b}, is_open_discrete _, is_open_discrete _, by simpa⟩⟩
 
 end totally_separated
+
+section connected_component_setoid
+
+/-- The setoid of connected components of a topological space -/
+def connected_component_setoid (α : Type*) [topological_space α] : setoid α :=
+⟨λ x y, connected_component x = connected_component y,
+  ⟨λ x, by trivial, λ x y h1, h1.symm, λ x y z h1 h2, h1.trans h2⟩⟩
+-- see Note [lower instance priority]
+local attribute [instance, priority 100] connected_component_setoid
+
+lemma connected_component_rel_iff {x y : α} : ⟦x⟧ = ⟦y⟧ ↔
+  connected_component x = connected_component y :=
+⟨λ h, quotient.exact h, λ h, quotient.sound h⟩
+
+/-- The quotient of a space by its connected components -/
+def pi0 (α : Type u) [topological_space α] := quotient (connected_component_setoid α)
+
+localized "notation `π₀` := pi0" in topological_space
+
+instance [inhabited α] : inhabited (π₀ α) := ⟨quotient.mk (default _)⟩
+instance pi0.topological_space : topological_space (π₀ α) := quotient.topological_space
+
+lemma continuous.image_eq_of_equiv {β : Type*} [topological_space β] [totally_disconnected_space β]
+  {f : α → β} (h : continuous f) (a b : α) (hab : a ≈ b) : f a = f b :=
+singleton_eq_singleton_iff.1 $
+  h.image_connected_component_eq_singleton a ▸
+  h.image_connected_component_eq_singleton b ▸ hab ▸ rfl
+
+/-- The lift to `π₀ α` of a continuous map from `α` to a totally disconnected space -/
+def continuous.pi0_lift {β : Type*} [topological_space β] [totally_disconnected_space β] {f : α → β}
+  (h : continuous f) : π₀ α → β :=
+quotient.lift f h.image_eq_of_equiv
+
+@[continuity] lemma continuous.pi0_lift_continuous {β : Type*} [topological_space β]
+  [totally_disconnected_space β] {f : α → β} (h : continuous f) : continuous h.pi0_lift :=
+continuous_quotient_lift h.image_eq_of_equiv h
+
+@[simp] lemma continuous.pi0_lift_factors {β : Type*} [topological_space β]
+  [totally_disconnected_space β] {f : α → β} (h : continuous f) :
+  h.pi0_lift ∘ quotient.mk = f := rfl
+
+lemma continuous.pi0_lift_unique {β : Type*} [topological_space β] [totally_disconnected_space β]
+  {f : α → β} (h : continuous f) (g : π₀ α → β) (hg : g ∘ quotient.mk = f) : g = h.pi0_lift :=
+by { subst hg, ext1 x, exact quotient.induction_on x (λ a, refl _) }
+
+lemma pi0_lift_unique' {β : Type*} (g₁ : π₀ α → β) (g₂ : π₀ α → β)
+  (hg : g₁ ∘ quotient.mk = g₂ ∘ quotient.mk ) : g₁ = g₂ :=
+begin
+  ext1 x,
+  refine quotient.induction_on x (λ a, _),
+  change (g₁ ∘ quotient.mk) a = (g₂ ∘ quotient.mk) a,
+  rw hg,
+end
+
+/-- The preimage of a singleton in `π₀` is the connected component of an element in the
+equivalence class. -/
+lemma pi0_preimage_singleton {t : α} : connected_component t = quotient.mk ⁻¹' {⟦t⟧} :=
+begin
+  apply set.eq_of_subset_of_subset; intros a ha,
+  { have H : ⟦a⟧ = ⟦t⟧ := quotient.sound (connected_component_eq ha).symm,
+    rw [mem_preimage, H],
+    exact mem_singleton ⟦t⟧ },
+  rw [mem_preimage, mem_singleton_iff] at ha,
+  have ha' : connected_component a = connected_component t := quotient.exact ha,
+  rw ←ha',
+  exact mem_connected_component,
+end
+
+/-- The preimage of the image of a set under the quotient map to `π₀ α` is the union of the
+connected components of the elements in it. -/
+lemma pi0_preimage_image (U : set α) :
+  quotient.mk ⁻¹' (quotient.mk '' U) = ⋃ (x : α) (h : x ∈ U), connected_component x :=
+begin
+  apply set.eq_of_subset_of_subset,
+  { rintros a ⟨b, hb, hab⟩,
+    refine mem_Union.2 ⟨b, mem_Union.2 ⟨hb, _⟩⟩,
+    rw connected_component_rel_iff.1 hab,
+    exact mem_connected_component },
+  refine Union_subset (λ a, Union_subset (λ ha, _)),
+  rw [pi0_preimage_singleton, (surjective_quotient_mk _).preimage_subset_preimage_iff,
+    singleton_subset_iff],
+  exact ⟨a, ha, refl _⟩,
+end
+
+instance pi0.totally_disconnected_space :
+  totally_disconnected_space (π₀ α) :=
+begin
+  rw totally_disconnected_space_iff_connected_component_singleton,
+  refine λ x, quotient.induction_on x (λ a, _),
+  apply eq_of_subset_of_subset _ (singleton_subset_iff.2 mem_connected_component),
+  rw subset_singleton_iff,
+  refine λ x, quotient.induction_on x (λ b hb, _),
+  rw [connected_component_rel_iff, connected_component_eq],
+  suffices : is_preconnected (quotient.mk ⁻¹' connected_component ⟦a⟧),
+  { apply mem_of_subset_of_mem (this.subset_connected_component hb),
+    exact mem_preimage.2 mem_connected_component },
+  apply (@preimage_connected_component_connected _ _ _ _ _ _ _ _).2,
+  { refine λ t, quotient.induction_on t (λ s, _),
+    rw ←pi0_preimage_singleton,
+    exact is_connected_connected_component },
+  refine λ T, ⟨λ hT, hT.preimage continuous_quotient_mk, λ hT, _⟩,
+  rwa [←is_open_compl_iff, ←preimage_compl, quotient_map_quotient_mk.is_open_preimage] at hT,
+end
+
+/-- Functoriality of `π₀` -/
+def continuous.pi0_map {β : Type*} [topological_space β] {f : α → β} (h : continuous f) :
+  π₀ α → π₀ β :=
+continuous.pi0_lift (continuous_quotient_mk.comp h)
+
+end connected_component_setoid

src/topology/path_connected.lean

@@ -577,7 +577,7 @@ begin
 end
 
 lemma path_component_subset_component (x : X) : path_component x ⊆ connected_component x :=
-λ y h, subset_connected_component (is_connected_range h.some_path.continuous).2
+λ y h, (is_connected_range h.some_path.continuous).subset_connected_component
   ⟨0, by simp⟩ ⟨1, by simp⟩
 
 /-- The path component of `x` in `F` is the set of points that can be joined to `x` in `F`. -/

src/topology/separation.lean

@@ -674,7 +674,7 @@ lemma connected_component_eq_Inter_clopen [t2_space α] [compact_space α] {x :
 begin
   apply eq_of_subset_of_subset connected_component_subset_Inter_clopen,
   -- Reduce to showing that the clopen intersection is connected.
-  refine subset_connected_component _ (mem_Inter.2 (λ Z, Z.2.2)),
+  refine is_preconnected.subset_connected_component _ (mem_Inter.2 (λ Z, Z.2.2)),
   -- We do this by showing that any disjoint cover by two closed sets implies
   -- that one of these closed sets must contain our whole thing. To reduce to the case
   -- where the cover is disjoint on all of α we need that s is closed: