refactor(topology/connected): drop `local attribute [instance] connec…

…ted_component_setoid` (#11365)

Add a coercion from `X` to `connected_components X` instead.

src/data/set/lattice.lean

@@ -1434,10 +1434,12 @@ disjoint_iff
 lemma not_disjoint_iff : ¬disjoint s t ↔ ∃ x, x ∈ s ∧ x ∈ t :=
 not_forall.trans $ exists_congr $ λ x, not_not
 
-lemma not_disjoint_iff_nonempty_inter {α : Type*} {s t : set α} :
-  ¬disjoint s t ↔ (s ∩ t).nonempty :=
+lemma not_disjoint_iff_nonempty_inter : ¬disjoint s t ↔ (s ∩ t).nonempty :=
 by simp [set.not_disjoint_iff, set.nonempty_def]
 
+lemma disjoint_or_nonempty_inter (s t : set α) : disjoint s t ∨ (s ∩ t).nonempty :=
+(em _).imp_right not_disjoint_iff_nonempty_inter.mp
+
 lemma disjoint_left : disjoint s t ↔ ∀ {a}, a ∈ s → a ∉ t :=
 show (∀ x, ¬(x ∈ s ∩ t)) ↔ _, from ⟨λ h a, not_and.1 $ h a, λ h a, not_and.2 $ h a⟩
 

src/topology/category/Profinite/default.lean

@@ -96,7 +96,6 @@ def Profinite.to_Top : Profinite ⥤ Top := forget₂ _ _
 rfl
 
 section Profinite
-local attribute [instance] connected_component_setoid
 
 /--
 (Implementation) The object part of the connected_components functor from compact Hausdorff spaces
@@ -118,13 +117,11 @@ spaces in compact Hausdorff spaces.
 -/
 def Profinite.to_CompHaus_equivalence (X : CompHaus.{u}) (Y : Profinite.{u}) :
   (CompHaus.to_Profinite_obj X ⟶ Y) ≃ (X ⟶ Profinite_to_CompHaus.obj Y) :=
-{ to_fun := λ f,
-  { to_fun := f.1 ∘ quotient.mk,
-    continuous_to_fun := continuous.comp f.2 (continuous_quotient_mk) },
+{ to_fun := λ f, f.comp ⟨quotient.mk', continuous_quotient_mk⟩,
   inv_fun := λ g,
     { to_fun := continuous.connected_components_lift g.2,
       continuous_to_fun := continuous.connected_components_lift_continuous g.2},
-  left_inv := λ f, continuous_map.ext $ λ x, quotient.induction_on x $ λ a, rfl,
+  left_inv := λ f, continuous_map.ext $ connected_components.surjective_coe.forall.2 $ λ a, rfl,
   right_inv := λ f, continuous_map.ext $ λ x, rfl }
 
 /--

src/topology/connected.lean

@@ -694,27 +694,25 @@ begin
 end
 
 /-- Preconnected sets are either contained in or disjoint to any given clopen set. -/
-theorem subset_or_disjoint_of_clopen {α : Type*} [topological_space α] {s t : set α}
-  (h : is_preconnected t) (h1 : is_clopen s) : s ∩ t = ∅ ∨ t ⊆ s :=
+theorem is_preconnected.subset_clopen {s t : set α} (hs : is_preconnected s) (ht : is_clopen t)
+  (hne : (s ∩ t).nonempty) : s ⊆ t :=
 begin
-  by_contradiction h2,
-  have h3 : (s ∩ t).nonempty := ne_empty_iff_nonempty.mp (mt or.inl h2),
-  have h4 : (t ∩ sᶜ).nonempty,
-  { apply inter_compl_nonempty_iff.2,
-    push_neg at h2,
-    exact h2.2 },
-  rw [inter_comm] at h3,
-  apply ne_empty_iff_nonempty.2 (h s sᶜ h1.1 (is_open_compl_iff.2 h1.2) _ h3 h4),
-  { rw [inter_compl_self, inter_empty] },
-  { rw [union_compl_self],
-    exact subset_univ t },
+  by_contra h,
+  have : (s ∩ tᶜ).nonempty := inter_compl_nonempty_iff.2 h,
+  obtain ⟨x, -, hx, hx'⟩ : (s ∩ (t ∩ tᶜ)).nonempty,
+    from hs t tᶜ ht.is_open ht.compl.is_open (λ x hx, em _) hne this,
+  exact hx' hx
 end
 
+/-- Preconnected sets are either contained in or disjoint to any given clopen set. -/
+theorem disjoint_or_subset_of_clopen {s t : set α} (hs : is_preconnected s) (ht : is_clopen t) :
+  disjoint s t ∨ s ⊆ t :=
+(disjoint_or_nonempty_inter s t).imp_right $ hs.subset_clopen ht
+
 /-- A set `s` is preconnected if and only if
 for every cover by two closed sets that are disjoint on `s`,
 it is contained in one of the two covering sets. -/
-theorem is_preconnected_iff_subset_of_disjoint_closed {α : Type*} {s : set α}
-  [topological_space α] :
+theorem is_preconnected_iff_subset_of_disjoint_closed :
   is_preconnected s ↔
     ∀ (u v : set α) (hu : is_closed u) (hv : is_closed v) (hs : s ⊆ u ∪ v) (huv : s ∩ (u ∩ v) = ∅),
       s ⊆ u ∨ s ⊆ v :=
@@ -769,28 +767,21 @@ begin
         inter_comm, inter_assoc, inter_comm v u, huv] }
 end
 
+lemma is_clopen.connected_component_subset {x} (hs : is_clopen s) (hx : x ∈ s) :
+  connected_component x ⊆ s :=
+is_preconnected_connected_component.subset_clopen hs ⟨x, mem_connected_component, hx⟩
+
 /-- The connected component of a point is always a subset of the intersection of all its clopen
 neighbourhoods. -/
 lemma connected_component_subset_Inter_clopen {x : α} :
   connected_component x ⊆ ⋂ Z : {Z : set α // is_clopen Z ∧ x ∈ Z}, Z :=
-begin
-  apply subset_Inter (λ Z, _),
-  cases (subset_or_disjoint_of_clopen (@is_connected_connected_component _ _ x).2 Z.2.1),
-  { exfalso,
-    apply nonempty.ne_empty
-      (nonempty_of_mem (mem_inter (@mem_connected_component _ _ x) Z.2.2)),
-    rw inter_comm,
-    exact h },
-  exact h,
-end
+subset_Inter $ λ Z, Z.2.1.connected_component_subset Z.2.2
 
 /-- A clopen set is the union of its connected components. -/
-lemma is_clopen.eq_union_connected_components {Z : set α} (h : is_clopen Z) :
-  Z = (⋃ (x : α) (H : x ∈ Z), connected_component x) :=
-eq_of_subset_of_subset (λ x xZ, mem_Union.2 ⟨x, mem_Union.2 ⟨xZ, mem_connected_component⟩⟩)
-  (Union_subset $ λ x, Union_subset $ λ xZ,
-    (by { apply subset.trans connected_component_subset_Inter_clopen
-      (Inter_subset _ ⟨Z, ⟨h, xZ⟩⟩) }))
+lemma is_clopen.bUnion_connected_component_eq {Z : set α} (h : is_clopen Z) :
+  (⋃ x ∈ Z, connected_component x) = Z :=
+(bUnion_subset $ λ x, h.connected_component_subset).antisymm $
+  λ x hx, mem_bUnion hx mem_connected_component
 
 /-- The preimage of a connected component is preconnected if the function has connected fibers
 and a subset is closed iff the preimage is. -/
@@ -902,6 +893,18 @@ begin
   exact preimage_mono h,
 end
 
+lemma quotient_map.preimage_connected_component [topological_space β] {f : α → β}
+  (hf : quotient_map f) (h_fibers : ∀ y : β, is_connected (f ⁻¹' {y})) (a : α) :
+  f ⁻¹' connected_component (f a) = connected_component a :=
+((preimage_connected_component_connected h_fibers
+  (λ _, hf.is_closed_preimage.symm) _).subset_connected_component mem_connected_component).antisymm
+  (hf.continuous.maps_to_connected_component a)
+
+lemma quotient_map.image_connected_component [topological_space β] {f : α → β}
+  (hf : quotient_map f) (h_fibers : ∀ y : β, is_connected (f ⁻¹' {y})) (a : α) :
+  f '' connected_component a = connected_component (f a) :=
+by rw [← hf.preimage_connected_component h_fibers, image_preimage_eq _ hf.surjective]
+
 end preconnected
 
 section totally_disconnected
@@ -1081,111 +1084,100 @@ section connected_component_setoid
 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⟩
-
-lemma connected_component_nrel_iff {x y : α} : ⟦x⟧ ≠ ⟦y⟧ ↔
-  connected_component x ≠ connected_component y :=
-by { rw not_iff_not, exact connected_component_rel_iff }
 
 /-- The quotient of a space by its connected components -/
 def connected_components (α : Type u) [topological_space α] :=
-  quotient (connected_component_setoid α)
+quotient (connected_component_setoid α)
+
+instance : has_coe_t α (connected_components α) := ⟨quotient.mk'⟩
+
+namespace connected_components
+
+@[simp] lemma coe_eq_coe {x y : α} :
+  (x : connected_components α) = y ↔ connected_component x = connected_component y :=
+quotient.eq'
+
+lemma coe_ne_coe {x y : α} :
+  (x : connected_components α) ≠ y ↔ connected_component x ≠ connected_component y :=
+not_congr coe_eq_coe
 
-instance [inhabited α] : inhabited (connected_components α) := ⟨quotient.mk default⟩
-instance connected_components.topological_space : topological_space (connected_components α) :=
-  quotient.topological_space
+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⟩
 
-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 :=
+instance [inhabited α] : inhabited (connected_components α) := ⟨↑(default : α)⟩
+
+instance : topological_space (connected_components α) :=
+quotient.topological_space
+
+lemma surjective_coe : surjective (coe : α → connected_components α) := surjective_quot_mk _
+lemma quotient_map_coe : quotient_map (coe : α → connected_components α) := quotient_map_quot_mk
+
+@[continuity]
+lemma continuous_coe : continuous (coe : α → connected_components α) := quotient_map_coe.continuous
+
+@[simp] lemma range_coe : range (coe : α → connected_components α)= univ :=
+surjective_coe.range_eq
+
+end connected_components
+
+variables [topological_space β] [totally_disconnected_space β] {f : α → β}
+
+lemma continuous.image_eq_of_connected_component_eq (h : continuous f) (a b : α)
+  (hab : connected_component a = connected_component 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 `connected_components α` of a continuous map from `α` to a totally disconnected space
 -/
-def continuous.connected_components_lift {β : Type*} [topological_space β]
-  [totally_disconnected_space β] {f : α → β} (h : continuous f) : connected_components α → β :=
-quotient.lift f h.image_eq_of_equiv
+def continuous.connected_components_lift (h : continuous f) :
+  connected_components α → β :=
+λ x, quotient.lift_on' x f h.image_eq_of_connected_component_eq
 
-@[continuity] lemma continuous.connected_components_lift_continuous {β : Type*}
-  [topological_space β] [totally_disconnected_space β] {f : α → β} (h : continuous f) :
+@[continuity] lemma continuous.connected_components_lift_continuous (h : continuous f) :
   continuous h.connected_components_lift :=
-continuous_quotient_lift h.image_eq_of_equiv h
+continuous_quotient_lift_on' h.image_eq_of_connected_component_eq h
 
-@[simp] lemma continuous.connected_components_lift_factors {β : Type*} [topological_space β]
-  [totally_disconnected_space β] {f : α → β} (h : continuous f) :
-  h.connected_components_lift ∘ quotient.mk = f := rfl
+@[simp] lemma continuous.connected_components_lift_apply_coe (h : continuous f) (x : α) :
+  h.connected_components_lift x = f x := rfl
 
-lemma continuous.connected_components_lift_unique {β : Type*} [topological_space β]
-  [totally_disconnected_space β] {f : α → β} (h : continuous f) (g : connected_components α → β)
-  (hg : g ∘ quotient.mk = f) : g = h.connected_components_lift :=
-by { subst hg, ext1 x, exact quotient.induction_on x (λ a, refl _) }
+@[simp] lemma continuous.connected_components_lift_comp_coe (h : continuous f) :
+  h.connected_components_lift ∘ coe = f := rfl
 
-lemma connected_components_lift_unique' {β : Type*} (g₁ : connected_components α → β)
-  (g₂ : connected_components α → β) (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
+lemma connected_components_lift_unique' {β : Sort*} {g₁ g₂ : connected_components α → β}
+  (hg : g₁ ∘ (coe : α → connected_components α) = g₂ ∘ coe) :
+  g₁ = g₂ :=
+connected_components.surjective_coe.injective_comp_right hg
+
+lemma continuous.connected_components_lift_unique (h : continuous f)
+  (g : connected_components α → β) (hg : g ∘ coe = f) : g = h.connected_components_lift :=
+connected_components_lift_unique' $ hg.trans h.connected_components_lift_comp_coe.symm
 
 /-- The preimage of a singleton in `connected_components` is the connected component
 of an element in the equivalence class. -/
-lemma connected_components_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
+lemma connected_components_preimage_singleton {x : α} :
+  coe ⁻¹' ({x} : set (connected_components α)) = connected_component x :=
+by { ext y, simp [connected_components.coe_eq_coe'] }
 
 /-- The preimage of the image of a set under the quotient map to `connected_components α`
 is the union of the connected components of the elements in it. -/
 lemma connected_components_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 [connected_components_preimage_singleton,
-    (surjective_quotient_mk _).preimage_subset_preimage_iff, singleton_subset_iff],
-  exact ⟨a, ha, refl _⟩,
-end
+  coe ⁻¹' (coe '' U : set (connected_components α)) = ⋃ x ∈ U, connected_component x :=
+by simp only [connected_components_preimage_singleton, preimage_bUnion, image_eq_Union]
 
 instance connected_components.totally_disconnected_space :
   totally_disconnected_space (connected_components α) :=
 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 ←connected_components_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,
-    is_open_compl_iff] at hT,
+  refine connected_components.surjective_coe.forall.2 (λ x, _),
+  rw [← connected_components.quotient_map_coe.image_connected_component,
+    ← connected_components_preimage_singleton,
+    image_preimage_eq _ connected_components.surjective_coe],
+  refine connected_components.surjective_coe.forall.2 (λ y, _),
+  rw connected_components_preimage_singleton,
+  exact is_connected_connected_component
 end
 
 /-- Functoriality of `connected_components` -/

src/topology/constructions.lean

@@ -751,6 +751,10 @@ lemma continuous_quotient_lift {f : α → β} (hs : ∀ a b, a ≈ b → f a =
   (h : continuous f) : continuous (quotient.lift f hs : quotient s → β) :=
 continuous_coinduced_dom h
 
+lemma continuous_quotient_lift_on' {f : α → β} (hs : ∀ a b, a ≈ b → f a = f b)
+  (h : continuous f) : continuous (λ x, quotient.lift_on' x f hs : quotient s → β) :=
+continuous_coinduced_dom h
+
 end quotient
 
 section pi