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

category_theory.connected_components J = quotient (category_theory.zigzag.setoid J)

@[protected, instance]

def category_theory.connected_components.inhabited {J : Type u₁} [category_theory.category J] [inhabited J] :

inhabited (category_theory.connected_components J)

Equations

category_theory.connected_components.inhabited = {default := quotient.mk' default}

@[protected, instance]

def category_theory.component.category {J : Type u₁} [category_theory.category J] (j : category_theory.connected_components J) :

category_theory.category (category_theory.component j)

def category_theory.component {J : Type u₁} [category_theory.category J] (j : category_theory.connected_components J) :

Type u₁

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

Equations

category_theory.component j = {k // quotient.mk' k = j}

@[protected, instance]

def category_theory.component.ι.full {J : Type u₁} [category_theory.category J] (j : category_theory.connected_components J) :

category_theory.full (category_theory.component.ι j)

@[protected, instance]

def category_theory.component.ι.faithful {J : Type u₁} [category_theory.category J] (j : category_theory.connected_components J) :

category_theory.faithful (category_theory.component.ι j)

def category_theory.component.ι {J : Type u₁} [category_theory.category J] (j : category_theory.connected_components J) :

category_theory.component j ⥤ J

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

Equations

category_theory.component.ι j = category_theory.full_subcategory_inclusion (λ (k : J), quotient.mk' k = j)

@[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}) :

(category_theory.component.ι j).obj self = self.val

@[simp]

theorem category_theory.component.ι_map {J : Type u₁} [category_theory.category J] (j : category_theory.connected_components J) (x y : category_theory.induced_category J subtype.val) (f : x ⟶ y) :

(category_theory.component.ι j).map f = f

@[protected, instance]

def category_theory.component.nonempty {J : Type u₁} [category_theory.category J] (j : category_theory.connected_components J) :

nonempty (category_theory.component j)

Each connected component of the category is nonempty.

@[protected, instance]

noncomputable def category_theory.component.inhabited {J : Type u₁} [category_theory.category J] (j : category_theory.connected_components J) :

inhabited (category_theory.component j)

Equations

category_theory.component.inhabited j = classical.inhabited_of_nonempty'

@[protected, instance]

def category_theory.component.is_connected {J : Type u₁} [category_theory.category J] (j : category_theory.connected_components J) :

category_theory.is_connected (category_theory.component j)

Each connected component of the category is connected.

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.

def category_theory.inclusion {J : Type u₁} [category_theory.category J] (j : category_theory.connected_components J) :

category_theory.component j ⥤ category_theory.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.

@[simp]

theorem category_theory.decomposed_to_map (J : Type u₁) [category_theory.category J] (X Y : Σ (i : category_theory.connected_components J), (λ (j : category_theory.connected_components J), category_theory.component j) i) (g : X ⟶ Y) :

(category_theory.decomposed_to J).map g = category_theory.sigma.desc_map category_theory.component.ι X Y g

def category_theory.decomposed_to (J : Type u₁) [category_theory.category J] :

category_theory.decomposed J ⥤ J

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

Equations

category_theory.decomposed_to J = category_theory.sigma.desc category_theory.component.ι

@[simp]

theorem category_theory.decomposed_to_obj (J : Type u₁) [category_theory.category J] (X : Σ (i : category_theory.connected_components J), (λ (j : category_theory.connected_components J), category_theory.component j) i) :

(category_theory.decomposed_to J).obj X = (category_theory.component.ι X.fst).obj X.snd

@[simp]

theorem category_theory.inclusion_comp_decomposed_to {J : Type u₁} [category_theory.category J] (j : category_theory.connected_components J) :

category_theory.inclusion j ⋙ category_theory.decomposed_to J = category_theory.component.ι j

@[protected, instance]

def category_theory.decomposed_to.full {J : Type u₁} [category_theory.category J] :

category_theory.full (category_theory.decomposed_to J)

Equations

category_theory.decomposed_to.full = {preimage := λ (X Y : category_theory.decomposed J) (f : (category_theory.decomposed_to J).obj X ⟶ (category_theory.decomposed_to J).obj Y), sigma.cases_on X (λ (j' : category_theory.connected_components J) (X_snd : category_theory.component j') (f : (category_theory.decomposed_to J).obj ⟨j', X_snd⟩ ⟶ (category_theory.decomposed_to J).obj Y), subtype.cases_on X_snd (λ (X : J) (hX : quotient.mk' X = j') (f : (category_theory.decomposed_to J).obj ⟨j', ⟨X, hX⟩⟩ ⟶ (category_theory.decomposed_to J).obj Y), sigma.cases_on Y (λ (k' : category_theory.connected_components J) (Y_snd : category_theory.component k') (f : (category_theory.decomposed_to J).obj ⟨j', ⟨X, hX⟩⟩ ⟶ (category_theory.decomposed_to J).obj ⟨k', Y_snd⟩), subtype.cases_on Y_snd (λ (Y : J) (hY : quotient.mk' Y = k') (f : (category_theory.decomposed_to J).obj ⟨j', ⟨X, hX⟩⟩ ⟶ (category_theory.decomposed_to J).obj ⟨k', ⟨Y, hY⟩⟩), id (λ (f : X ⟶ Y), eq.rec (λ (hY : quotient.mk' Y = j'), category_theory.sigma.sigma_hom.mk f) _ hY) f) f) f) f) f, witness' := _}

@[protected, instance]

def category_theory.decomposed_to.faithful {J : Type u₁} [category_theory.category J] :

category_theory.faithful (category_theory.decomposed_to J)

@[protected, instance]

def category_theory.decomposed_to.ess_surj {J : Type u₁} [category_theory.category J] :

category_theory.ess_surj (category_theory.decomposed_to J)

@[protected, instance]

noncomputable def category_theory.decomposed_to.is_equivalence {J : Type u₁} [category_theory.category J] :

category_theory.is_equivalence (category_theory.decomposed_to J)

Equations

category_theory.decomposed_to.is_equivalence = category_theory.equivalence.of_fully_faithfully_ess_surj (category_theory.decomposed_to J)

@[simp]

theorem category_theory.decomposed_equiv_functor {J : Type u₁} [category_theory.category J] :

category_theory.decomposed_equiv.functor = category_theory.decomposed_to J

noncomputable def category_theory.decomposed_equiv {J : Type u₁} [category_theory.category J] :

category_theory.decomposed J ≌ J

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

Equations

category_theory.decomposed_equiv = (category_theory.decomposed_to J).as_equivalence