Connected components

This file records general topological properties of connected components, and of the quotient of a space by them.

Main declarations

• Homeomorph.image_connectedComponent: a homeomorphism maps a connected component onto the connected component of the image point.
• TauCeti.frontier_connectedComponentIn_subset_compl: in a locally connected space, a connected component of an open set has its frontier in the complement of that set.
• TauCeti.isPreconnected_compl_of_isPreconnected_frontier: in a preconnected, locally connected space, an open set with preconnected frontier has preconnected complement.
• TauCeti.instT1SpaceConnectedComponents: the connected-components quotient of any topological space is a T1 space.
• TauCeti.connectedComponentsSigmaHomeomorph: a locally connected space is homeomorphic to the disjoint union of its connected components.
• TauCeti.finite_connectedComponents_of_finite_irreducibleComponents: finiteness of the irreducible components implies finiteness of the connected components.
• TauCeti.natCard_connectedComponents_eq_of_iUnion_eq_univ: a space covered by finitely many pairwise disjoint closed connected sets has exactly as many connected components as sets.

@[simp]

theorem Homeomorph.image_connectedComponent {X : Type u} [TopologicalSpace X] {Y : Type u_1} [TopologicalSpace Y] (e : X ≃ₜ Y) (x : X) : ⇑e '' connectedComponent x = connectedComponent (e x)

A homeomorphism maps a connected component onto the connected component of the image point.

theorem TauCeti.frontier_connectedComponentIn_subset_compl {X : Type u} [TopologicalSpace X] [LocallyConnectedSpace X] {F : Set X} (hF : IsOpen F) (x : X) : frontier (connectedComponentIn F x) ⊆ Fᶜ

The frontier of a connected component of an open set misses the set. Equivalently, frontier (connectedComponentIn F x) ∩ F = ∅: the component is clopen in F.

theorem TauCeti.isPreconnected_compl_of_isPreconnected_frontier {X : Type u} [TopologicalSpace X] [LocallyConnectedSpace X] [PreconnectedSpace X] {U : Set X} (hU : IsOpen U) (hf : IsPreconnected (frontier U)) : IsPreconnected Uᶜ

An open set with preconnected frontier has preconnected complement, in a preconnected, locally connected space.

Openness is needed: in ℝ the frontier of {0} is {0}, while {0}ᶜ is disconnected.

instance TauCeti.instT1SpaceConnectedComponents {X : Type u} [TopologicalSpace X] : T1Space (ConnectedComponents X)

The quotient of a topological space by its connected components is a T1 space.

instance TauCeti.instPathConnectedSpaceConnectedComponentsFiber {X : Type u} [TopologicalSpace X] [LocallyPathConnectedSpace X] (C : ConnectedComponents X) : PathConnectedSpace ↑(ConnectedComponents.mk ⁻¹' {C})

A fibre of the quotient to connected components is path-connected when the ambient space is locally path-connected.

instance TauCeti.instLocallyPathConnectedSpaceConnectedComponentsFiber {X : Type u} [TopologicalSpace X] [LocallyPathConnectedSpace X] (C : ConnectedComponents X) : LocallyPathConnectedSpace ↑(ConnectedComponents.mk ⁻¹' {C})

A fibre of the quotient to connected components is locally path-connected when the ambient space is locally path-connected.

noncomputable def TauCeti.connectedComponentsSigmaHomeomorph {X : Type u} [TopologicalSpace X] [LocallyConnectedSpace X] : (C : ConnectedComponents X) × ↑(ConnectedComponents.mk ⁻¹' {C}) ≃ₜ X

A locally connected space is the disjoint union of its connected components.

The summand indexed by C : ConnectedComponents X is the fibre of the canonical quotient map over C, so this decomposition does not require choosing representatives.

Equations

• TauCeti.connectedComponentsSigmaHomeomorph = (Equiv.sigmaPreimageEquiv ConnectedComponents.mk).toHomeomorphOfContinuousOpen ⋯ ⋯

@[simp]

theorem TauCeti.connectedComponentsSigmaHomeomorph_apply {X : Type u} [TopologicalSpace X] [LocallyConnectedSpace X] (z : (C : ConnectedComponents X) × ↑(ConnectedComponents.mk ⁻¹' {C})) : connectedComponentsSigmaHomeomorph z = ↑z.snd

@[simp]

theorem TauCeti.connectedComponentsSigmaHomeomorph_symm_apply {X : Type u} [TopologicalSpace X] [LocallyConnectedSpace X] (x : X) : connectedComponentsSigmaHomeomorph.symm x = ⟨ConnectedComponents.mk x, ⟨x, ⋯⟩⟩

theorem TauCeti.finite_connectedComponents_of_finite_irreducibleComponents {X : Type u} [TopologicalSpace X] (h : (irreducibleComponents X).Finite) : Finite (ConnectedComponents X)

A space with finitely many irreducible components has finitely many connected components.

theorem TauCeti.natCard_connectedComponents_eq_of_iUnion_eq_univ {X : Type u} [TopologicalSpace X] {ι : Type u_1} [Finite ι] {U : ι → Set X} (hclosed : ∀ (i : ι), IsClosed (U i)) (hdisj : Pairwise (Function.onFun Disjoint U)) (hunion : ⋃ (i : ι), U i = Set.univ) (hconn : ∀ (i : ι), IsConnected (U i)) : Nat.card (ConnectedComponents X) = Nat.card ι

A space covered by finitely many pairwise disjoint closed connected sets has exactly as many connected components as sets: the sets are its connected components.