English
The space of connected components is Hausdorff when X is Hausdorff and compact.
Русский
Пространство компонент связности хаусдорфово, если X хаусдорфово и компактно.
LaTeX
$$$ [T2Space X] [CompactSpace X] \\Rightarrow [T2Space (ConnectedComponents X)]$$$
Lean4
/-- `ConnectedComponents X` is Hausdorff when `X` is Hausdorff and compact -/
@[stacks 0900 "The Stacks entry proves profiniteness."]
instance t2 [T2Space X] [CompactSpace X] : T2Space (ConnectedComponents X) := by
-- Fix 2 distinct connected components, with points a and b
refine ⟨ConnectedComponents.surjective_coe.forall₂.2 fun a b ne => ?_⟩
rw [ConnectedComponents.coe_ne_coe] at ne
have h := connectedComponent_disjoint ne
rw [connectedComponent_eq_iInter_isClopen b, disjoint_iff_inter_eq_empty] at h
obtain ⟨U, V, hU, ha, hb, rfl⟩ :
∃ (U : Set X) (V : Set (ConnectedComponents X)),
IsClopen U ∧ connectedComponent a ∩ U = ∅ ∧ connectedComponent b ⊆ U ∧ (↑) ⁻¹' V = U :=
by
have h :=
(isClosed_connectedComponent (α := X)).isCompact.elim_finite_subfamily_closed _
(fun s : { s : Set X // IsClopen s ∧ b ∈ s } => s.2.1.1) h
obtain ⟨fin_a, ha⟩ := h
set U : Set X := ⋂ (i : { s // IsClopen s ∧ b ∈ s }) (_ : i ∈ fin_a), i
have hU : IsClopen U := isClopen_biInter_finset fun i _ => i.2.1
exact
⟨U, (↑) '' U, hU, ha, subset_iInter₂ fun s _ => s.2.1.connectedComponent_subset s.2.2,
(connectedComponents_preimage_image U).symm ▸ hU.biUnion_connectedComponent_eq⟩
rw [ConnectedComponents.isQuotientMap_coe.isClopen_preimage] at hU
refine ⟨Vᶜ, V, hU.compl.isOpen, hU.isOpen, ?_, hb mem_connectedComponent, disjoint_compl_left⟩
exact fun h => flip Set.Nonempty.ne_empty ha ⟨a, mem_connectedComponent, h⟩
