Skeleton of a category

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 CategoryTheory.Skeletal (C : Type u₁) [Category.{v₁, u₁} C] : Prop

A category is skeletal if isomorphic objects are equal.

structure CategoryTheory.IsSkeletonOf (C : Type u₁) [Category.{v₁, u₁} C] (D : Type u₂) [Category.{v₂, u₂} D] (F : Functor D C) : Prop

IsSkeletonOf 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.

• skel : Skeletal D

  The category D has isomorphic objects equal

• eqv : F.IsEquivalence

  The functor F is an equivalence

theorem CategoryTheory.Functor.eq_of_iso {C : Type u₁} [Category.{v₁, u₁} C] {D : Type u₂} [Category.{v₂, u₂} D] {F₁ F₂ : Functor D C} [Quiver.IsThin C] (hC : Skeletal C) (hF : F₁ ≅ F₂) : F₁ = F₂

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

theorem CategoryTheory.functor_skeletal {C : Type u₁} [Category.{v₁, u₁} C] {D : Type u₂} [Category.{v₂, u₂} D] [Quiver.IsThin C] (hC : Skeletal C) : Skeletal (Functor D C)

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

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

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

instance CategoryTheory.instCategorySkeleton (C : Type u_2) [Category.{u_1, u_2} C] : Category.{u_1, u_2} (Skeleton C)

instance CategoryTheory.instInhabitedSkeleton (C : Type u_1) [Category.{u_2, u_1} C] [Inhabited C] : Inhabited (Skeleton C)

instance CategoryTheory.instCoeSortSkeleton (C : Type u_1) [Category.{u_3, u_1} C] (α : Sort u_2) [CoeSort C α] : CoeSort (Skeleton C) α

noncomputable def CategoryTheory.fromSkeleton (C : Type u₁) [Category.{v₁, u₁} C] : Functor (Skeleton C) C

The functor from the skeleton of C to C.

@[simp]

theorem CategoryTheory.fromSkeleton_map (C : Type u₁) [Category.{v₁, u₁} C] {X✝ Y✝ : InducedCategory C Quotient.out} (f : X✝ ⟶ Y✝) : (fromSkeleton C).map f = f.hom

@[simp]

theorem CategoryTheory.fromSkeleton_obj (C : Type u₁) [Category.{v₁, u₁} C] (a✝ : _root_.Quotient (isIsomorphicSetoid C)) : (fromSkeleton C).obj a✝ = a✝.out

instance CategoryTheory.instFullSkeletonFromSkeleton (C : Type u₁) [Category.{v₁, u₁} C] : (fromSkeleton C).Full

instance CategoryTheory.instFaithfulSkeletonFromSkeleton (C : Type u₁) [Category.{v₁, u₁} C] : (fromSkeleton C).Faithful

instance CategoryTheory.instEssSurjSkeletonFromSkeleton (C : Type u₁) [Category.{v₁, u₁} C] : (fromSkeleton C).EssSurj

instance CategoryTheory.fromSkeleton.isEquivalence (C : Type u₁) [Category.{v₁, u₁} C] : (fromSkeleton C).IsEquivalence

@[reducible, inline]

abbrev CategoryTheory.toSkeleton {C : Type u₁} [Category.{v₁, u₁} C] (X : C) : Skeleton C

The class of an object in the skeleton.

noncomputable def CategoryTheory.fromSkeletonToSkeletonIso {C : Type u₁} [Category.{v₁, u₁} C] (X : C) : (fromSkeleton C).obj (toSkeleton X) ≅ X

The isomorphism between ⟦X⟧.out and X.

@[deprecated CategoryTheory.fromSkeletonToSkeletonIso (since := "2025-12-18")]

def CategoryTheory.preCounitIso {C : Type u₁} [Category.{v₁, u₁} C] (X : C) : (fromSkeleton C).obj (toSkeleton X) ≅ X

Alias of CategoryTheory.fromSkeletonToSkeletonIso.

---

The isomorphism between ⟦X⟧.out and X.

@[simp]

theorem CategoryTheory.Skeleton.comp_hom {C : Type u₁} [Category.{v₁, u₁} C] {X Y Z : Skeleton C} (f : X ⟶ Y) (g : Y ⟶ Z) : (CategoryStruct.comp f g).hom = CategoryStruct.comp f.hom g.hom

theorem CategoryTheory.Skeleton.comp_hom_assoc {C : Type u₁} [Category.{v₁, u₁} C] {X Y Z : Skeleton C} (f : X ⟶ Y) (g : Y ⟶ Z) {Z✝ : C} (h : Quotient.out Z ⟶ Z✝) : CategoryStruct.comp (CategoryStruct.comp f g).hom h = CategoryStruct.comp f.hom (CategoryStruct.comp g.hom h)

noncomputable def CategoryTheory.toSkeletonFunctor (C : Type u₁) [Category.{v₁, u₁} C] : Functor C (Skeleton C)

An inverse to fromSkeleton C that forms an equivalence with it.

@[simp]

theorem CategoryTheory.toSkeletonFunctor_obj (C : Type u₁) [Category.{v₁, u₁} C] (X : C) : (toSkeletonFunctor C).obj X = toSkeleton X

@[simp]

theorem CategoryTheory.toSkeletonFunctor_map_hom (C : Type u₁) [Category.{v₁, u₁} C] {X Y : C} (f : X ⟶ Y) : ((toSkeletonFunctor C).map f).hom = CategoryStruct.comp (fromSkeletonToSkeletonIso X).hom (CategoryStruct.comp f (fromSkeletonToSkeletonIso Y).inv)

noncomputable def CategoryTheory.skeletonEquivalence (C : Type u₁) [Category.{v₁, u₁} C] : Skeleton C ≌ C

The equivalence between the skeleton and the category itself.

@[simp]

theorem CategoryTheory.skeletonEquivalence_unitIso (C : Type u₁) [Category.{v₁, u₁} C] : (skeletonEquivalence C).unitIso = NatIso.ofComponents (fun (X : Skeleton C) => InducedCategory.isoMk (Nonempty.some ⋯).symm) ⋯

@[simp]

theorem CategoryTheory.skeletonEquivalence_counitIso (C : Type u₁) [Category.{v₁, u₁} C] : (skeletonEquivalence C).counitIso = NatIso.ofComponents fromSkeletonToSkeletonIso ⋯

@[simp]

theorem CategoryTheory.skeletonEquivalence_inverse (C : Type u₁) [Category.{v₁, u₁} C] : (skeletonEquivalence C).inverse = toSkeletonFunctor C

@[simp]

theorem CategoryTheory.skeletonEquivalence_functor (C : Type u₁) [Category.{v₁, u₁} C] : (skeletonEquivalence C).functor = fromSkeleton C

theorem CategoryTheory.skeleton_skeletal (C : Type u₁) [Category.{v₁, u₁} C] : Skeletal (Skeleton C)

theorem CategoryTheory.skeleton_isSkeleton (C : Type u₁) [Category.{v₁, u₁} C] : IsSkeletonOf C (Skeleton C) (fromSkeleton C)

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

theorem CategoryTheory.toSkeleton_fromSkeleton_obj {C : Type u₁} [Category.{v₁, u₁} C] (X : Skeleton C) : toSkeleton ((fromSkeleton C).obj X) = X

theorem CategoryTheory.toSkeleton_eq_toSkeleton_iff {C : Type u₁} [Category.{v₁, u₁} C] {X Y : C} : toSkeleton X = toSkeleton Y ↔ Nonempty (X ≅ Y)

theorem CategoryTheory.congr_toSkeleton_of_iso {C : Type u₁} [Category.{v₁, u₁} C] {X Y : C} (e : X ≅ Y) : toSkeleton X = toSkeleton Y

noncomputable def CategoryTheory.Skeleton.isoOfEq {C : Type u₁} [Category.{v₁, u₁} C] {X Y : C} (h : toSkeleton X = toSkeleton Y) : X ≅ Y

Provides a (noncomputable) isomorphism X ≅ Y given that toSkeleton X = toSkeleton Y.

theorem CategoryTheory.toSkeleton_eq_iff {C : Type u₁} [Category.{v₁, u₁} C] {X : C} {Y : Skeleton C} : toSkeleton X = Y ↔ Nonempty (X ≅ (fromSkeleton C).obj Y)

noncomputable def CategoryTheory.Functor.mapSkeleton {C : Type u₁} [Category.{v₁, u₁} C] {D : Type u₂} [Category.{v₂, u₂} D] (F : Functor C D) : Functor (Skeleton C) (Skeleton D)

From a functor C ⥤ D, construct a map of skeletons Skeleton C → Skeleton D.

theorem CategoryTheory.Functor.mapSkeleton_obj_toSkeleton {C : Type u₁} [Category.{v₁, u₁} C] {D : Type u₂} [Category.{v₂, u₂} D] (F : Functor C D) (X : C) : F.mapSkeleton.obj (toSkeleton X) = toSkeleton (F.obj X)

instance CategoryTheory.Functor.instFullSkeletonMapSkeleton {C : Type u₁} [Category.{v₁, u₁} C] {D : Type u₂} [Category.{v₂, u₂} D] (F : Functor C D) [F.Full] : F.mapSkeleton.Full

instance CategoryTheory.Functor.instFaithfulSkeletonMapSkeleton {C : Type u₁} [Category.{v₁, u₁} C] {D : Type u₂} [Category.{v₂, u₂} D] (F : Functor C D) [F.Faithful] : F.mapSkeleton.Faithful

instance CategoryTheory.Functor.instEssSurjSkeletonMapSkeleton {C : Type u₁} [Category.{v₁, u₁} C] {D : Type u₂} [Category.{v₂, u₂} D] (F : Functor C D) [F.EssSurj] : F.mapSkeleton.EssSurj

noncomputable def CategoryTheory.Functor.toSkeletonFunctorCompMapSkeletonIso {C : Type u₁} [Category.{v₁, u₁} C] {D : Type u₂} [Category.{v₂, u₂} D] (F : Functor C D) : (toSkeletonFunctor C).comp F.mapSkeleton ≅ F.comp (toSkeletonFunctor D)

A natural isomorphism between X ↦ ⟦X⟧ ↦ ⟦FX⟧ and X ↦ FX ↦ ⟦FX⟧. On the level of categories, these are C ⥤ Skeleton C ⥤ Skeleton D and C ⥤ D ⥤ Skeleton D. So this says that the square formed by these 4 objects and 4 functors commutes.

theorem CategoryTheory.Functor.mapSkeleton_injective {C : Type u₁} [Category.{v₁, u₁} C] {D : Type u₂} [Category.{v₂, u₂} D] (F : Functor C D) [F.Full] [F.Faithful] : Function.Injective F.mapSkeleton.obj

theorem CategoryTheory.Functor.mapSkeleton_surjective {C : Type u₁} [Category.{v₁, u₁} C] {D : Type u₂} [Category.{v₂, u₂} D] (F : Functor C D) [F.EssSurj] : Function.Surjective F.mapSkeleton.obj

noncomputable def CategoryTheory.Equivalence.skeletonEquiv {C : Type u₁} [Category.{v₁, u₁} C] {D : Type u₂} [Category.{v₂, u₂} D] (e : C ≌ D) : Skeleton C ≃ Skeleton D

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

def CategoryTheory.ThinSkeleton (C : Type u₁) [Category.{v₁, u₁} C] : 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.

@[reducible, inline]

abbrev CategoryTheory.ThinSkeleton.mk {C : Type u₁} [Category.{v₁, u₁} C] (c : C) : ThinSkeleton C

Convenience constructor for ThinSkeleton.

instance CategoryTheory.inhabitedThinSkeleton (C : Type u₁) [Category.{v₁, u₁} C] [Inhabited C] : Inhabited (ThinSkeleton C)

instance CategoryTheory.ThinSkeleton.preorder (C : Type u₁) [Category.{v₁, u₁} C] : Preorder (ThinSkeleton C)

def CategoryTheory.toThinSkeleton (C : Type u₁) [Category.{v₁, u₁} C] : Functor C (ThinSkeleton C)

The functor from a category to its thin skeleton.

@[simp]

theorem CategoryTheory.toThinSkeleton_map (C : Type u₁) [Category.{v₁, u₁} C] {X✝ Y✝ : C} (f : X✝ ⟶ Y✝) : (toThinSkeleton C).map f = homOfLE ⋯

@[simp]

theorem CategoryTheory.toThinSkeleton_obj (C : Type u₁) [Category.{v₁, u₁} C] (c : C) : (toThinSkeleton C).obj c = ThinSkeleton.mk 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.

instance CategoryTheory.ThinSkeleton.thin (C : Type u₁) [Category.{v₁, u₁} C] : Quiver.IsThin (ThinSkeleton C)

The thin skeleton is thin.

def CategoryTheory.ThinSkeleton.map {C : Type u₁} [Category.{v₁, u₁} C] {D : Type u₂} [Category.{v₂, u₂} D] (F : Functor C D) : Functor (ThinSkeleton C) (ThinSkeleton D)

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

@[simp]

theorem CategoryTheory.ThinSkeleton.map_obj {C : Type u₁} [Category.{v₁, u₁} C] {D : Type u₂} [Category.{v₂, u₂} D] (F : Functor C D) (a✝ : _root_.Quotient (isIsomorphicSetoid C)) : (map F).obj a✝ = Quotient.map F.obj ⋯ a✝

@[simp]

theorem CategoryTheory.ThinSkeleton.map_map {C : Type u₁} [Category.{v₁, u₁} C] {D : Type u₂} [Category.{v₂, u₂} D] (F : Functor C D) {X Y : ThinSkeleton C} (a✝ : X ⟶ Y) : (map F).map a✝ = Quotient.recOnSubsingleton₂ (motive := fun (x x_1 : ThinSkeleton C) => (x ⟶ x_1) → (Quotient.map F.obj ⋯ x ⟶ Quotient.map F.obj ⋯ x_1)) X Y (fun (x x_1 : C) (k : ⟦x⟧ ⟶ ⟦x_1⟧) => homOfLE ⋯) a✝

theorem CategoryTheory.ThinSkeleton.comp_toThinSkeleton {C : Type u₁} [Category.{v₁, u₁} C] {D : Type u₂} [Category.{v₂, u₂} D] (F : Functor C D) : F.comp (toThinSkeleton D) = (toThinSkeleton C).comp (map F)

def CategoryTheory.ThinSkeleton.mapNatTrans {C : Type u₁} [Category.{v₁, u₁} C] {D : Type u₂} [Category.{v₂, u₂} D] {F₁ F₂ : Functor C D} (k : F₁ ⟶ F₂) : map F₁ ⟶ map F₂

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

def CategoryTheory.ThinSkeleton.map₂ObjMap {C : Type u₁} [Category.{v₁, u₁} C] {D : Type u₂} [Category.{v₂, u₂} D] {E : Type u₃} [Category.{v₃, u₃} E] (F : Functor C (Functor D E)) : ThinSkeleton C → ThinSkeleton D → ThinSkeleton E

Given a bifunctor, we descend to a function on objects of ThinSkeleton

def CategoryTheory.ThinSkeleton.map₂Functor {C : Type u₁} [Category.{v₁, u₁} C] {D : Type u₂} [Category.{v₂, u₂} D] {E : Type u₃} [Category.{v₃, u₃} E] (F : Functor C (Functor D E)) : ThinSkeleton C → Functor (ThinSkeleton D) (ThinSkeleton E)

For each x : ThinSkeleton C, we promote map₂ObjMap F x to a functor

def CategoryTheory.ThinSkeleton.map₂NatTrans {C : Type u₁} [Category.{v₁, u₁} C] {D : Type u₂} [Category.{v₂, u₂} D] {E : Type u₃} [Category.{v₃, u₃} E] (F : Functor C (Functor D E)) {x₁ x₂ : ThinSkeleton C} : (x₁ ⟶ x₂) → (map₂Functor F x₁ ⟶ map₂Functor F x₂)

This provides natural transformations map₂Functor F x₁ ⟶ map₂Functor F x₂ given x₁ ⟶ x₂

def CategoryTheory.ThinSkeleton.map₂ {C : Type u₁} [Category.{v₁, u₁} C] {D : Type u₂} [Category.{v₂, u₂} D] {E : Type u₃} [Category.{v₃, u₃} E] (F : Functor C (Functor D E)) : Functor (ThinSkeleton C) (Functor (ThinSkeleton D) (ThinSkeleton E))

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

@[simp]

theorem CategoryTheory.ThinSkeleton.map₂_map {C : Type u₁} [Category.{v₁, u₁} C] {D : Type u₂} [Category.{v₂, u₂} D] {E : Type u₃} [Category.{v₃, u₃} E] (F : Functor C (Functor D E)) {X✝ Y✝ : ThinSkeleton C} (a✝ : X✝ ⟶ Y✝) : (map₂ F).map a✝ = map₂NatTrans F a✝

@[simp]

theorem CategoryTheory.ThinSkeleton.map₂_obj {C : Type u₁} [Category.{v₁, u₁} C] {D : Type u₂} [Category.{v₂, u₂} D] {E : Type u₃} [Category.{v₃, u₃} E] (F : Functor C (Functor D E)) (a✝ : ThinSkeleton C) : (map₂ F).obj a✝ = map₂Functor F a✝

instance CategoryTheory.ThinSkeleton.toThinSkeleton_faithful (C : Type u₁) [Category.{v₁, u₁} C] [Quiver.IsThin C] : (toThinSkeleton C).Faithful

noncomputable def CategoryTheory.ThinSkeleton.fromThinSkeleton (C : Type u₁) [Category.{v₁, u₁} C] [Quiver.IsThin C] : Functor (ThinSkeleton C) C

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

@[simp]

theorem CategoryTheory.ThinSkeleton.fromThinSkeleton_obj (C : Type u₁) [Category.{v₁, u₁} C] [Quiver.IsThin C] (a✝ : _root_.Quotient (isIsomorphicSetoid C)) : (fromThinSkeleton C).obj a✝ = a✝.out

@[simp]

theorem CategoryTheory.ThinSkeleton.fromThinSkeleton_map (C : Type u₁) [Category.{v₁, u₁} C] [Quiver.IsThin C] {x y : ThinSkeleton C} (a✝ : x ⟶ y) : (fromThinSkeleton C).map a✝ = Quotient.recOnSubsingleton₂ (motive := fun (x x_1 : ThinSkeleton C) => (x ⟶ x_1) → (Quotient.out x ⟶ Quotient.out x_1)) x y (fun (X Y : C) (f : ⟦X⟧ ⟶ ⟦Y⟧) => CategoryStruct.comp (Nonempty.some ⋯).hom (CategoryStruct.comp (Nonempty.some ⋯) (Nonempty.some ⋯).inv)) a✝

noncomputable def CategoryTheory.ThinSkeleton.equivalence (C : Type u₁) [Category.{v₁, u₁} C] [Quiver.IsThin C] : ThinSkeleton C ≌ C

The equivalence between the thin skeleton and the category itself.

instance CategoryTheory.ThinSkeleton.fromThinSkeleton_isEquivalence (C : Type u₁) [Category.{v₁, u₁} C] [Quiver.IsThin C] : (fromThinSkeleton C).IsEquivalence

theorem CategoryTheory.ThinSkeleton.equiv_of_both_ways {C : Type u₁} [Category.{v₁, u₁} C] [Quiver.IsThin C] {X Y : C} (f : X ⟶ Y) (g : Y ⟶ X) : X ≈ Y

instance CategoryTheory.ThinSkeleton.thinSkeletonPartialOrder {C : Type u₁} [Category.{v₁, u₁} C] [Quiver.IsThin C] : PartialOrder (ThinSkeleton C)

theorem CategoryTheory.ThinSkeleton.skeletal {C : Type u₁} [Category.{v₁, u₁} C] [Quiver.IsThin C] : Skeletal (ThinSkeleton C)

theorem CategoryTheory.ThinSkeleton.map_comp_eq {C : Type u₁} [Category.{v₁, u₁} C] {D : Type u₂} [Category.{v₂, u₂} D] {E : Type u₃} [Category.{v₃, u₃} E] [Quiver.IsThin C] (F : Functor E D) (G : Functor D C) : map (F.comp G) = (map F).comp (map G)

theorem CategoryTheory.ThinSkeleton.map_id_eq {C : Type u₁} [Category.{v₁, u₁} C] [Quiver.IsThin C] : map (Functor.id C) = Functor.id (ThinSkeleton C)

theorem CategoryTheory.ThinSkeleton.map_iso_eq {C : Type u₁} [Category.{v₁, u₁} C] {D : Type u₂} [Category.{v₂, u₂} D] [Quiver.IsThin C] {F₁ F₂ : Functor D C} (h : F₁ ≅ F₂) : map F₁ = map F₂

noncomputable def CategoryTheory.ThinSkeleton.fromThinSkeletonCompToThinSkeletonIso {C : Type u₁} [Category.{v₁, u₁} C] {D : Type u₂} [Category.{v₂, u₂} D] [Quiver.IsThin C] (F : Functor C D) : (fromThinSkeleton C).comp (F.comp (toThinSkeleton D)) ≅ map F

Applying fromThinSkeleton, F and then toThinSkeleton is isomorphic to applying map F.

noncomputable def CategoryTheory.ThinSkeleton.mapCompFromThinSkeletonIso {C : Type u₁} [Category.{v₁, u₁} C] {D : Type u₂} [Category.{v₂, u₂} D] [Quiver.IsThin C] [Quiver.IsThin D] (F : Functor C D) : (map F).comp (fromThinSkeleton D) ≅ (fromThinSkeleton C).comp F

Applying map F and then fromThinSkeleton is isomorphic to first applying fromThinSkeleton and then applying F.

theorem CategoryTheory.ThinSkeleton.thinSkeleton_isSkeleton {C : Type u₁} [Category.{v₁, u₁} C] [Quiver.IsThin C] : IsSkeletonOf C (ThinSkeleton C) (fromThinSkeleton C)

fromThinSkeleton C exhibits the thin skeleton as a skeleton.

instance CategoryTheory.ThinSkeleton.isSkeletonOfInhabited {C : Type u₁} [Category.{v₁, u₁} C] [Quiver.IsThin C] : Inhabited (IsSkeletonOf C (ThinSkeleton C) (fromThinSkeleton C))

def CategoryTheory.ThinSkeleton.lowerAdjunction {C : Type u₁} [Category.{v₁, u₁} C] {D : Type u₂} [Category.{v₂, u₂} D] (R : Functor D C) (L : Functor C D) (h : L ⊣ R) : map L ⊣ map R

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

noncomputable def CategoryTheory.Equivalence.thinSkeletonOrderIso {C : Type u₁} [Category.{v₁, u₁} C] {α : Type u_1} [PartialOrder α] [Quiver.IsThin C] (e : C ≌ α) : ThinSkeleton C ≃o α

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