# Documentation

Mathlib.CategoryTheory.ConnectedComponents

# Connected components of a category #

Defines a type ConnectedComponents 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.

This type indexes the connected components of the category J.

Instances For
def CategoryTheory.Component {J : Type u₁} [] :
Type u₁

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

Instances For
@[simp]
theorem CategoryTheory.Component.ι_map {J : Type u₁} [] :
∀ {X Y : CategoryTheory.InducedCategory J CategoryTheory.FullSubcategory.obj} (f : X Y), ().map f = f
@[simp]
theorem CategoryTheory.Component.ι_obj {J : Type u₁} [] (self : CategoryTheory.FullSubcategory fun k => ) :
().obj self = self.obj
def CategoryTheory.Component.ι {J : Type u₁} [] :

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

Instances For

Each connected component of the category is nonempty.

Each connected component of the category is connected.

@[inline, reducible]
abbrev CategoryTheory.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.

Instances For
@[inline, reducible]
abbrev CategoryTheory.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.

Instances For
@[simp]
theorem CategoryTheory.decomposedTo_map (J : Type u₁) [] :
∀ {X Y : (i : ) × (fun j => ) i} (g : X Y), ().map g = CategoryTheory.Sigma.descMap CategoryTheory.Component.ι X Y g
@[simp]
theorem CategoryTheory.decomposedTo_obj (J : Type u₁) [] (X : (i : ) × (fun j => ) i) :
().obj X = X.snd.obj
def CategoryTheory.decomposedTo (J : Type u₁) [] :

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

Instances For
@[simp]
@[simp]
theorem CategoryTheory.decomposedEquiv_functor {J : Type u₁} [] :
CategoryTheory.decomposedEquiv.functor =

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

Instances For