mathlib documentation

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₁) [category_theory.category J] :
Type u₁

This type indexes the connected components of the category J.

Equations
Instances for category_theory.connected_components

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

Equations
Instances for category_theory.component

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

Equations
Instances for category_theory.component.ι
@[simp]
theorem category_theory.component.ι_obj {J : Type u₁} [category_theory.category J] (j : category_theory.connected_components J) (self : {X // (λ (k : J), quotient.mk' k = j) X}) :
@[protected, instance]

Each connected component of the category is nonempty.

@[protected, instance]

Each connected component of the category is connected.

@[reducible]
def category_theory.decomposed (J : Type u₁) [category_theory.category J] :
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.

@[reducible]

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.

@[protected, instance]
Equations

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

Equations