# mathlib3documentation

category_theory.skeletal

# Skeleton of a category #

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

Define skeletal categories as categories in which any two isomorphic objects are equal.

Construct the skeleton of an arbitrary category by taking isomorphism classes, and show it is a skeleton of the original category.

In addition, construct the skeleton of a thin category as a partial ordering, and (noncomputably) show it is a skeleton of the original category. The advantage of this special case being handled separately is that lemmas and definitions about orderings can be used directly, for example for the subobject lattice. In addition, some of the commutative diagrams about the functors commute definitionally on the nose which is convenient in practice.

def category_theory.skeletal (C : Type u₁)  :
Prop

A category is skeletal if isomorphic objects are equal.

Equations
structure category_theory.is_skeleton_of (C : Type u₁) (D : Type u₂) (F : D C) :
Type (max u₁ u₂ v₁ v₂)
• skel :
• eqv :

is_skeleton_of C D F says that F : D ⥤ C exhibits D as a skeletal full subcategory of C, in particular F is a (strong) equivalence and D is skeletal.

Instances for category_theory.is_skeleton_of
theorem category_theory.functor.eq_of_iso {C : Type u₁} {D : Type u₂} {F₁ F₂ : D C} (hC : category_theory.skeletal C) (hF : F₁ F₂) :
F₁ = F₂

If C is thin and skeletal, then any naturally isomorphic functors to C are equal.

theorem category_theory.functor_skeletal {C : Type u₁} {D : Type u₂} (hC : category_theory.skeletal C) :

If C is thin and skeletal, D ⥤ C is skeletal. category_theory.functor_thin shows it is thin also.

@[protected, instance]
noncomputable def category_theory.skeleton.category (C : Type u₁)  :
def category_theory.skeleton (C : Type u₁)  :
Type u₁

Construct the skeleton category as the induced category on the isomorphism classes, and derive its category structure.

Equations
Instances for category_theory.skeleton
@[protected, instance]
Equations
@[simp]
theorem category_theory.from_skeleton_map (C : Type u₁) (f : x y) :
@[protected, instance]
noncomputable def category_theory.from_skeleton.full (C : Type u₁)  :
noncomputable def category_theory.from_skeleton (C : Type u₁)  :

The functor from the skeleton of C to C.

Equations
Instances for category_theory.from_skeleton
@[protected, instance]
@[simp]
theorem category_theory.from_skeleton_obj (C : Type u₁)  :
= ᾰ.out
@[protected, instance]
@[protected, instance]
noncomputable def category_theory.from_skeleton.is_equivalence (C : Type u₁)  :
Equations
noncomputable def category_theory.skeleton_equivalence (C : Type u₁)  :

The equivalence between the skeleton and the category itself.

Equations
noncomputable def category_theory.skeleton_is_skeleton (C : Type u₁)  :

The skeleton of C given by choice is a skeleton of C.

Equations
noncomputable def category_theory.equivalence.skeleton_equiv {C : Type u₁} {D : Type u₂} (e : C D) :

Two categories which are categorically equivalent have skeletons with equivalent objects.

Equations
def category_theory.thin_skeleton (C : Type u₁)  :
Type u₁

Construct the skeleton category by taking the quotient of objects. This construction gives a preorder with nice definitional properties, but is only really appropriate for thin categories. If your original category is not thin, you probably want to be using skeleton instead of this.

Equations
Instances for category_theory.thin_skeleton
@[protected, instance]
Equations
@[protected, instance]
Equations

The functor from a category to its thin skeleton.

Equations
Instances for category_theory.to_thin_skeleton
@[simp]
theorem category_theory.to_thin_skeleton_map (C : Type u₁) (X Y : C) (f : X Y) :
@[simp]
theorem category_theory.to_thin_skeleton_obj (C : Type u₁) (a : C) :

The constructions here are intended to be used when the category C is thin, even though some of the statements can be shown without this assumption.

@[protected, instance]

The thin skeleton is thin.

@[simp]
theorem category_theory.thin_skeleton.map_obj {C : Type u₁} {D : Type u₂} (F : C D)  :
= _
@[simp]
theorem category_theory.thin_skeleton.map_map {C : Type u₁} {D : Type u₂} (F : C D) (X Y : category_theory.thin_skeleton C) (ᾰ : X Y) :
= (λ (x y : C) (k : x y),
def category_theory.thin_skeleton.map {C : Type u₁} {D : Type u₂} (F : C D) :

A functor C ⥤ D computably lowers to a functor thin_skeleton C ⥤ thin_skeleton D.

Equations
theorem category_theory.thin_skeleton.comp_to_thin_skeleton {C : Type u₁} {D : Type u₂} (F : C D) :
def category_theory.thin_skeleton.map_nat_trans {C : Type u₁} {D : Type u₂} {F₁ F₂ : C D} (k : F₁ F₂) :

Given a natural transformation F₁ ⟶ F₂, induce a natural transformation map F₁ ⟶ map F₂.

Equations
@[simp]
theorem category_theory.thin_skeleton.map₂_obj_obj {C : Type u₁} {D : Type u₂} {E : Type u₃} (F : C D E)  :
.obj y = quotient.map₂ (λ (X : C) (Y : D), (F.obj X).obj Y) _ x y
@[simp]
theorem category_theory.thin_skeleton.map₂_obj_map {C : Type u₁} {D : Type u₂} {E : Type u₃} (F : C D E) (y₁ y₂ : category_theory.thin_skeleton D) (ᾰ : y₁ y₂) :
.map = (λ (X : C), (λ (Y₁ Y₂ : D) (hY : Y₁ Y₂),
@[simp]
theorem category_theory.thin_skeleton.map₂_map {C : Type u₁} {D : Type u₂} {E : Type u₃} (F : C D E) (x₁ x₂ : category_theory.thin_skeleton C) (ᾰ : x₁ x₂) :
= (λ (X₁ X₂ : C) (f : X₁ X₂), {app := λ (y : , (λ (Y : D), , naturality' := _})
def category_theory.thin_skeleton.map₂ {C : Type u₁} {D : Type u₂} {E : Type u₃} (F : C D E) :

A functor C ⥤ D ⥤ E computably lowers to a functor thin_skeleton C ⥤ thin_skeleton D ⥤ thin_skeleton E

Equations
@[protected, instance]
@[simp]
theorem category_theory.thin_skeleton.from_thin_skeleton_map (C : Type u₁) (x y : category_theory.thin_skeleton C) (ᾰ : x y) :
= (λ (X Y : C) (f : X Y), .hom .inv)
noncomputable def category_theory.thin_skeleton.from_thin_skeleton (C : Type u₁)  :

Use quotient.out to create a functor out of the thin skeleton.

Equations
Instances for category_theory.thin_skeleton.from_thin_skeleton
@[simp]
@[protected, instance]
Equations
noncomputable def category_theory.thin_skeleton.equivalence (C : Type u₁)  :

The equivalence between the thin skeleton and the category itself.

Equations
theorem category_theory.thin_skeleton.equiv_of_both_ways {C : Type u₁} {X Y : C} (f : X Y) (g : Y X) :
X Y
@[protected, instance]
Equations
theorem category_theory.thin_skeleton.map_comp_eq {C : Type u₁} {D : Type u₂} {E : Type u₃} (F : E D) (G : D C) :
theorem category_theory.thin_skeleton.map_iso_eq {C : Type u₁} {D : Type u₂} {F₁ F₂ : D C} (h : F₁ F₂) :

from_thin_skeleton C exhibits the thin skeleton as a skeleton.

Equations
@[protected, instance]
Equations
def category_theory.thin_skeleton.lower_adjunction {C : Type u₁} {D : Type u₂} (R : D C) (L : C D) (h : L R) :

An adjunction between thin categories gives an adjunction between their thin skeletons.

Equations
noncomputable def category_theory.equivalence.thin_skeleton_order_iso {C : Type u₁} {α : Type u_1} (e : C α) :

When e : C ≌ α is a categorical equivalence from a thin category C to some partial order α, the thin_skeleton C is order isomorphic to α.

Equations