# mathlibdocumentation

category_theory.connected_components

# Connected components of a category #

Defines a type connected_components J indexing the connected components of a category, and the full subcategories giving each connected component: component j : Type u₁. We show that each component j is in fact connected.

We show every category can be expressed as a disjoint union of its connected components, in particular decomposed J is the category (definitionally) given by the sigma-type of the connected components of J, and it is shown that this is equivalent to J.

def category_theory.connected_components (J : Type u₁)  :
Type u₁

This type indexes the connected components of the category J.

Equations
@[instance]
Equations
@[instance]
def category_theory.component {J : Type u₁}  :
Type u₁

Given an index for a connected component, produce the actual component as a full subcategory.

Equations
• = {k // = j}
@[instance]
@[instance]
def category_theory.component.ι {J : Type u₁}  :

The inclusion functor from a connected component to the whole category.

Equations
@[simp]
theorem category_theory.component.ι_obj {J : Type u₁} (self : {X // (λ (k : J), = j) X}) :
self = self.val
@[simp]
theorem category_theory.component.ι_map {J : Type u₁} (f : x y) :
= f
@[instance]
def category_theory.component.nonempty {J : Type u₁}  :

Each connected component of the category is nonempty.

@[instance]
def category_theory.component.inhabited {J : Type u₁}  :
Equations
@[instance]

Each connected component of the category is connected.

def category_theory.decomposed (J : Type u₁)  :
Type u₁

The disjoint union of Js connected components, written explicitly as a sigma-type with the category structure. This category is equivalent to J.

def category_theory.inclusion {J : Type u₁}  :

The inclusion of each component into the decomposed category. This is just sigma.incl but having this abbreviation helps guide typeclass search to get the right category instance on decomposed J.

@[simp]
theorem category_theory.decomposed_to_map (J : Type u₁) (X Y : Σ (i : , i) (g : X Y) :
def category_theory.decomposed_to (J : Type u₁)  :

The forward direction of the equivalence between the decomposed category and the original.

Equations
@[simp]
theorem category_theory.decomposed_to_obj (J : Type u₁) (X : Σ (i : , i) :
@[simp]
@[instance]
Equations
@[instance]
@[instance]
@[instance]
Equations
@[simp]
def category_theory.decomposed_equiv {J : Type u₁}  :

This gives that any category is equivalent to a disjoint union of connected categories.

Equations