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.

def CategoryTheory.ConnectedComponents (J : Type u₁) [Category.{v₁, u₁} J] : Type u₁

This type indexes the connected components of the category J.

def CategoryTheory.Functor.mapConnectedComponents {J : Type u₁} [Category.{v₁, u₁} J] {K : Type u₂} [Category.{v₂, u₂} K] (F : Functor J K) (x : ConnectedComponents J) : ConnectedComponents K

The map ConnectedComponents J → ConnectedComponents K induced by a functor J ⥤ K.

@[simp]

theorem CategoryTheory.Functor.mapConnectedComponents_mk {J : Type u₁} [Category.{v₁, u₁} J] {K : Type u₂} [Category.{v₂, u₂} K] (F : Functor J K) (j : J) : F.mapConnectedComponents ⟦j⟧ = ⟦F.obj j⟧

@[implicit_reducible]

instance CategoryTheory.instInhabitedConnectedComponents {J : Type u₁} [Category.{v₁, u₁} J] [Inhabited J] : Inhabited (ConnectedComponents J)

def CategoryTheory.ConnectedComponents.functorToDiscrete {J : Type u₁} [Category.{v₁, u₁} J] (X : Type u_1) (f : ConnectedComponents J → X) : Functor J (Discrete X)

Every function from connected components of a category gives a functor to discrete category

def CategoryTheory.ConnectedComponents.liftFunctor (J : Type u_2) [Category.{v_1, u_2} J] {X : Type u_1} (F : Functor J (Discrete X)) : ConnectedComponents J → X

Every functor to a discrete category gives a function from connected components

def CategoryTheory.ConnectedComponents.typeToCatHomEquiv (J : Type u_2) [Category.{v_1, u_2} J] (X : Type u_1) : (ConnectedComponents J → X) ≃ Functor J (Discrete X)

Functions from connected components and functors to discrete category are in bijection

def CategoryTheory.ConnectedComponents.objectProperty {J : Type u₁} [Category.{v₁, u₁} J] (j : ConnectedComponents J) : ObjectProperty J

Given an index for a connected component, this is the property of the objects which belong to this component.

@[reducible, inline]

abbrev CategoryTheory.ConnectedComponents.Component {J : Type u₁} [Category.{v₁, u₁} J] (j : ConnectedComponents J) : Type u₁

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

@[reducible, inline]

abbrev CategoryTheory.ConnectedComponents.ι {J : Type u₁} [Category.{v₁, u₁} J] (j : ConnectedComponents J) : Functor j.Component J

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

@[reducible, inline]

abbrev CategoryTheory.ConnectedComponents.mk {J : Type u₁} [Category.{v₁, u₁} J] (j : J) : ConnectedComponents J

The connected component of an object in a category.

instance CategoryTheory.instNonemptyComponent {J : Type u₁} [Category.{v₁, u₁} J] (j : ConnectedComponents J) : Nonempty j.Component

Each connected component of the category is nonempty.

@[implicit_reducible]

noncomputable instance CategoryTheory.instInhabitedComponent {J : Type u₁} [Category.{v₁, u₁} J] (j : ConnectedComponents J) : Inhabited j.Component

instance CategoryTheory.instIsConnectedComponent {J : Type u₁} [Category.{v₁, u₁} J] (j : ConnectedComponents J) : IsConnected j.Component

Each connected component of the category is connected.

@[reducible, inline]

abbrev CategoryTheory.Decomposed (J : Type u₁) [Category.{v₁, u₁} J] : Type u₁

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

@[reducible, inline]

abbrev CategoryTheory.inclusion {J : Type u₁} [Category.{v₁, u₁} J] (j : ConnectedComponents J) : Functor j.Component (Decomposed J)

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.

def CategoryTheory.decomposedTo (J : Type u₁) [Category.{v₁, u₁} J] : Functor (Decomposed J) J

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

@[simp]

theorem CategoryTheory.decomposedTo_map (J : Type u₁) [Category.{v₁, u₁} J] {X✝ Y✝ : (i : ConnectedComponents J) × i.Component} (g : X✝ ⟶ Y✝) : (decomposedTo J).map g = Sigma.descMap ConnectedComponents.ι X✝ Y✝ g

@[simp]

theorem CategoryTheory.decomposedTo_obj (J : Type u₁) [Category.{v₁, u₁} J] (X : (i : ConnectedComponents J) × i.Component) : (decomposedTo J).obj X = X.snd.obj

@[simp]

theorem CategoryTheory.inclusion_comp_decomposedTo {J : Type u₁} [Category.{v₁, u₁} J] (j : ConnectedComponents J) : (inclusion j).comp (decomposedTo J) = j.ι

instance CategoryTheory.instFullDecomposedDecomposedTo {J : Type u₁} [Category.{v₁, u₁} J] : (decomposedTo J).Full

instance CategoryTheory.instFaithfulDecomposedDecomposedTo {J : Type u₁} [Category.{v₁, u₁} J] : (decomposedTo J).Faithful

instance CategoryTheory.instEssSurjDecomposedDecomposedTo {J : Type u₁} [Category.{v₁, u₁} J] : (decomposedTo J).EssSurj

instance CategoryTheory.instIsEquivalenceDecomposedDecomposedTo {J : Type u₁} [Category.{v₁, u₁} J] : (decomposedTo J).IsEquivalence

noncomputable def CategoryTheory.decomposedEquiv {J : Type u₁} [Category.{v₁, u₁} J] : Decomposed J ≌ J

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

@[simp]

theorem CategoryTheory.decomposedEquiv_functor {J : Type u₁} [Category.{v₁, u₁} J] : decomposedEquiv.functor = decomposedTo J