mathlib3 documentation

category_theory.connected_components

Connected components of a category #

THIS FILE IS SYNCHRONIZED WITH MATHLIB4. Any changes to this file require a corresponding PR to mathlib4.

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.

source
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
source
@[protected, instance]
def category_theory.connected_components.inhabited {J : Type u₁} [category_theory.category J] [inhabited J] :
inhabited (category_theory.connected_components J)
Equations
source
@[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)
source
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
Instances for category_theory.component
source
@[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)
source
@[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)
source
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
Instances for category_theory.component.ι
source
@[simp]
theorem category_theory.component.ι_obj {J : Type u₁} [category_theory.category J] (j : category_theory.connected_components J) (self : category_theory.full_subcategory (λ (k : J), quotient.mk' k = j)) :
(category_theory.component.ι j).obj self = self.obj
source
@[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 category_theory.full_subcategory.obj) (f : x ⟶ y) :
(category_theory.component.ι j).map f = f
source
@[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.

source
@[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
source
@[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.

source
@[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.

source
@[reducible]
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.

source
@[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
source
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
Instances for category_theory.decomposed_to
source
@[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
source
@[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
source
@[protected, instance]
def category_theory.decomposed_to.full {J : Type u₁} [category_theory.category J] :
category_theory.full (category_theory.decomposed_to J)
Equations
source
@[protected, instance]
def category_theory.decomposed_to.faithful {J : Type u₁} [category_theory.category J] :
category_theory.faithful (category_theory.decomposed_to J)
source
@[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)
source
@[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
source
@[simp]
theorem category_theory.decomposed_equiv_functor {J : Type u₁} [category_theory.category J] :
category_theory.decomposed_equiv.functor = category_theory.decomposed_to J
source
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