Mathlib.CategoryTheory.Skeletal

CategoryTheory.Skeletal definition

: Prop

Full source

/-- A category is skeletal if isomorphic objects are equal. -/
def Skeletal : Prop :=
  ∀ ⦃X Y : C⦄, IsIsomorphic X Y → X = Y

Skeletal category

Informal description

A category $\mathcal{C}$ is called *skeletal* if any two isomorphic objects $X$ and $Y$ in $\mathcal{C}$ are equal, i.e., $X \cong Y$ implies $X = Y$.

CategoryTheory.IsSkeletonOf structure

(F : D ⥤ C)

Full source

/-- `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.
-/
structure IsSkeletonOf (F : D ⥤ C) : Prop where
  /-- The category `D` has isomorphic objects equal -/
  skel : Skeletal D
  /-- The functor `F` is an equivalence -/
  eqv : F.IsEquivalence := by infer_instance

Skeleton of a category

Informal description

The structure `IsSkeletonOf C D F` states that a functor $F: D \to C$ exhibits $D$ as a skeletal full subcategory of $C$, where: 1. $F$ is a (strong) equivalence of categories 2. $D$ is skeletal (any two isomorphic objects in $D$ are equal)

CategoryTheory.functor_skeletal theorem

[Quiver.IsThin C] (hC : Skeletal C) : Skeletal (D ⥤ C)

Full source

/-- If `C` is thin and skeletal, `D ⥤ C` is skeletal.
`CategoryTheory.functor_thin` shows it is thin also.
-/
theorem functor_skeletal [Quiver.IsThin C] (hC : Skeletal C) : Skeletal (D ⥤ C) := fun _ _ h =>
  h.elim (Functor.eq_of_iso hC)

Functor Category to Thin Skeletal Category is Skeletal

Informal description

If $\mathcal{C}$ is a thin and skeletal category, then for any category $\mathcal{D}$, the functor category $\mathcal{D} \to \mathcal{C}$ is skeletal. Here, a *thin* category means there is at most one morphism between any two objects, and a *skeletal* category means any two isomorphic objects are equal.

CategoryTheory.Skeleton definition

: Type u₁

Full source

/-- Construct the skeleton category as the induced category on the isomorphism classes, and derive
its category structure.
-/
def Skeleton : Type u₁ := InducedCategory (C := Quotient (isIsomorphicSetoid C)) C Quotient.out

Skeleton of a category

Informal description

The skeleton of a category $\mathcal{C}$ is defined as the induced category on the quotient of the objects of $\mathcal{C}$ by the equivalence relation of isomorphism. Specifically, it is constructed by taking the objects to be the isomorphism classes of $\mathcal{C}$ (using the quotient of the setoid of isomorphic objects) and defining the morphisms between two isomorphism classes as the morphisms between any representatives of those classes in $\mathcal{C}$. This construction ensures that the skeleton is a skeletal category (i.e., any two isomorphic objects are equal) and that it is equivalent to the original category $\mathcal{C}$.

CategoryTheory.instInhabitedSkeleton instance

[Inhabited C] : Inhabited (Skeleton C)

Full source

instance [Inhabited C] : Inhabited (Skeleton C) :=
  ⟨⟦default⟧⟩

Inhabitedness of Category Skeletons

Informal description

For any inhabited category $\mathcal{C}$, its skeleton is also inhabited.

CategoryTheory.instCategorySkeleton instance

: Category (Skeleton C)

Full source

noncomputable instance : Category (Skeleton C) := by
  apply InducedCategory.category

Category Structure on the Skeleton of a Category

Informal description

The skeleton of a category $\mathcal{C}$ forms a category, where the objects are isomorphism classes of objects in $\mathcal{C}$ and the morphisms are induced by the morphisms in $\mathcal{C}$ between representatives of these classes.

CategoryTheory.instCoeSortSkeleton instance

{α} [CoeSort C α] : CoeSort (Skeleton C) α

Full source

noncomputable instance {α} [CoeSort C α] : CoeSort (Skeleton C) α :=
  inferInstanceAs (CoeSort (InducedCategory _ _) _)

Coercion from Skeleton to Base Category's Objects

Informal description

For any type $\alpha$ that can be coerced into objects of a category $\mathcal{C}$, the skeleton of $\mathcal{C}$ can also be coerced into $\alpha$.

CategoryTheory.fromSkeleton definition

: Skeleton C ⥤ C

Full source

/-- The functor from the skeleton of `C` to `C`. -/
@[simps!]
noncomputable def fromSkeleton : SkeletonSkeleton C ⥤ C :=
  inducedFunctor _

Inclusion functor from skeleton to original category

Informal description

The functor from the skeleton of a category $\mathcal{C}$ to $\mathcal{C}$ itself, which maps each isomorphism class in the skeleton to a representative object in $\mathcal{C}$ and each morphism between classes to the corresponding morphism between representatives.

CategoryTheory.instFullSkeletonFromSkeleton instance

: (fromSkeleton C).Full

Full source

noncomputable instance : (fromSkeleton C).Full := by
  apply InducedCategory.full

Fullness of the Inclusion Functor from Skeleton to Category

Informal description

The inclusion functor from the skeleton of a category $\mathcal{C}$ to $\mathcal{C}$ is full. That is, for any two objects $X$ and $Y$ in the skeleton, the map $\text{Hom}(X, Y) \to \text{Hom}(F(X), F(Y))$ is surjective, where $F$ is the inclusion functor.

CategoryTheory.instFaithfulSkeletonFromSkeleton instance

: (fromSkeleton C).Faithful

Full source

noncomputable instance : (fromSkeleton C).Faithful := by
  apply InducedCategory.faithful

Faithfulness of the Skeleton Inclusion Functor

Informal description

The inclusion functor from the skeleton of a category $\mathcal{C}$ to $\mathcal{C}$ is faithful. That is, for any two objects $X$ and $Y$ in the skeleton, the map $\text{Hom}(X, Y) \to \text{Hom}(F(X), F(Y))$ is injective, where $F$ is the inclusion functor.

CategoryTheory.instEssSurjSkeletonFromSkeleton instance

: (fromSkeleton C).EssSurj

Full source

instance : (fromSkeleton C).EssSurj where mem_essImage X := ⟨Quotient.mk' X, Quotient.mk_out X⟩

Essential Surjectivity of the Skeleton Inclusion Functor

Informal description

The inclusion functor from the skeleton of a category $\mathcal{C}$ to $\mathcal{C}$ is essentially surjective. That is, every object in $\mathcal{C}$ is isomorphic to an object in the image of the skeleton inclusion functor.

CategoryTheory.fromSkeleton.isEquivalence instance

: (fromSkeleton C).IsEquivalence

Full source

noncomputable instance fromSkeleton.isEquivalence : (fromSkeleton C).IsEquivalence where

Skeleton Inclusion Functor is an Equivalence

Informal description

The inclusion functor from the skeleton of a category $\mathcal{C}$ to $\mathcal{C}$ is an equivalence of categories. That is, it is faithful, full, and essentially surjective.

CategoryTheory.toSkeleton abbrev

(X : C) : Skeleton C

Full source

/-- The class of an object in the skeleton. -/
abbrev toSkeleton (X : C) : Skeleton C := ⟦X⟧

Canonical map to the skeleton of a category

Informal description

For any object $X$ in a category $\mathcal{C}$, the function $\text{toSkeleton}$ maps $X$ to its isomorphism class in the skeleton of $\mathcal{C}$, denoted $\text{Skeleton}(\mathcal{C})$. This construction sends each object to its equivalence class under the relation of isomorphism.

CategoryTheory.preCounitIso definition

(X : C) : (fromSkeleton C).obj (toSkeleton X) ≅ X

Full source

/-- The isomorphism between `⟦X⟧.out` and `X`. -/
noncomputable def preCounitIso (X : C) : (fromSkeleton C).obj (toSkeleton X) ≅ X :=
  Nonempty.some (Quotient.mk_out X)

Isomorphism between skeleton representative and original object

Informal description

For any object $X$ in a category $\mathcal{C}$, the isomorphism $\text{preCounitIso}(X)$ relates the representative of the isomorphism class of $X$ in the skeleton of $\mathcal{C}$ (obtained by applying the inclusion functor $\text{fromSkeleton}$ to $\text{toSkeleton}(X)$) back to the original object $X$ in $\mathcal{C}$. In other words, $\text{preCounitIso}(X)$ provides a natural isomorphism between the composition $\text{fromSkeleton} \circ \text{toSkeleton}$ and the identity functor on $\mathcal{C}$, ensuring that the skeleton construction is equivalent to the original category.

CategoryTheory.toSkeletonFunctor definition

: C ⥤ Skeleton C

Full source

/-- An inverse to `fromSkeleton C` that forms an equivalence with it. -/
@[simps] noncomputable def toSkeletonFunctor : C ⥤ Skeleton C where
  obj := toSkeleton
  map {X Y} f := by apply (preCounitIso X).hom ≫ f ≫ (preCounitIso Y).inv
  map_id _ := by aesop
  map_comp _ _ := by change _ = CategoryStruct.comp (obj := C) _ _; simp

Functor from category to its skeleton

Informal description

The functor from a category $\mathcal{C}$ to its skeleton, which maps each object $X$ in $\mathcal{C}$ to its isomorphism class $\text{toSkeleton}(X)$ in the skeleton, and each morphism $f : X \to Y$ to the morphism obtained by composing with the isomorphisms $\text{preCounitIso}(X)$ and $\text{preCounitIso}(Y)^{-1}$.

CategoryTheory.skeletonEquivalence definition

: Skeleton C ≌ C

Full source

/-- The equivalence between the skeleton and the category itself. -/
@[simps] noncomputable def skeletonEquivalence : SkeletonSkeleton C ≌ C where
  functor := fromSkeleton C
  inverse := toSkeletonFunctor C
  unitIso := NatIso.ofComponents
    (fun X ↦ InducedCategory.isoMk (Nonempty.some <| Quotient.mk_out X.out).symm)
    fun _ ↦ .symm <| Iso.inv_hom_id_assoc _ _
  counitIso := NatIso.ofComponents preCounitIso
  functor_unitIso_comp _ := Iso.inv_hom_id _

Equivalence between a category and its skeleton

Informal description

The equivalence of categories between the skeleton $\text{Skeleton}(\mathcal{C})$ and the original category $\mathcal{C}$, consisting of: - A functor $\text{fromSkeleton} \colon \text{Skeleton}(\mathcal{C}) \to \mathcal{C}$ that maps each isomorphism class to a representative object, - A functor $\text{toSkeletonFunctor} \colon \mathcal{C} \to \text{Skeleton}(\mathcal{C})$ that maps each object to its isomorphism class, - Natural isomorphisms $\text{unitIso}$ and $\text{counitIso}$ witnessing the equivalence.

CategoryTheory.skeleton_skeletal theorem

: Skeletal (Skeleton C)

Full source

theorem skeleton_skeletal : Skeletal (Skeleton C) := by
  rintro X Y ⟨h⟩
  have : X.out ≈ Y.out := ⟨(fromSkeleton C).mapIso h⟩
  simpa using Quotient.sound this

Skeleton of a Category is Skeletal

Informal description

The skeleton of a category $\mathcal{C}$ is a skeletal category, meaning that any two isomorphic objects in the skeleton are equal.

CategoryTheory.skeleton_isSkeleton theorem

: IsSkeletonOf C (Skeleton C) (fromSkeleton C)

Full source

/-- The `skeleton` of `C` given by choice is a skeleton of `C`. -/
lemma skeleton_isSkeleton : IsSkeletonOf C (Skeleton C) (fromSkeleton C) where
  skel := skeleton_skeletal C
  eqv := fromSkeleton.isEquivalence C

Skeleton Inclusion Functor Exhibits Skeleton as Skeletal Full Subcategory

Informal description

The inclusion functor $\text{fromSkeleton} \colon \text{Skeleton}(\mathcal{C}) \to \mathcal{C}$ exhibits the skeleton of $\mathcal{C}$ as a skeletal full subcategory of $\mathcal{C}$. That is: 1. The functor $\text{fromSkeleton}$ is a (strong) equivalence of categories. 2. The category $\text{Skeleton}(\mathcal{C})$ is skeletal (any two isomorphic objects are equal).

CategoryTheory.Equivalence.skeletonEquiv definition

(e : C ≌ D) : Skeleton C ≃ Skeleton D

Full source

/-- Two categories which are categorically equivalent have skeletons with equivalent objects.
-/
noncomputable def Equivalence.skeletonEquiv (e : C ≌ D) : SkeletonSkeleton C ≃ Skeleton D :=
  let f := ((skeletonEquivalence C).trans e).trans (skeletonEquivalence D).symm
  { toFun := f.functor.obj
    invFun := f.inverse.obj
    left_inv := fun X => skeleton_skeletal C ⟨(f.unitIso.app X).symm⟩
    right_inv := fun Y => skeleton_skeletal D ⟨f.counitIso.app Y⟩ }

Equivalence of skeletons induced by an equivalence of categories

Informal description

Given an equivalence of categories $e \colon C \simeq D$, there is an equivalence between their skeletons $\text{Skeleton}(C) \simeq \text{Skeleton}(D)$. This equivalence is constructed by composing the skeleton equivalence of $C$, the given equivalence $e$, and the inverse of the skeleton equivalence of $D$, and then using the skeletal property to define the inverse maps.

CategoryTheory.ThinSkeleton definition

: Type u₁

Full source

/-- 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.
-/
def ThinSkeleton : Type u₁ :=
  Quotient (isIsomorphicSetoid C)

Thin skeleton of a category

Informal description

The thin skeleton of a category $\mathcal{C}$ is constructed by taking the quotient of the objects of $\mathcal{C}$ by the equivalence relation of isomorphism. This results in a preorder where each equivalence class consists of all objects in $\mathcal{C}$ that are isomorphic to each other. This construction is particularly well-suited for thin categories (categories where there is at most one morphism between any two objects), as it allows for direct application of order-theoretic lemmas and definitions. For non-thin categories, the general `skeleton` construction is more appropriate.

CategoryTheory.inhabitedThinSkeleton instance

[Inhabited C] : Inhabited (ThinSkeleton C)

Full source

instance inhabitedThinSkeleton [Inhabited C] : Inhabited (ThinSkeleton C) :=
  ⟨@Quotient.mk' C (isIsomorphicSetoid C) default⟩

Inhabitedness of the Thin Skeleton of a Category

Informal description

For any inhabited category $\mathcal{C}$, its thin skeleton is also inhabited.

CategoryTheory.ThinSkeleton.preorder instance

: Preorder (ThinSkeleton C)

Full source

instance ThinSkeleton.preorder : Preorder (ThinSkeleton C) where
  le :=
    @Quotient.lift₂ C C _ (isIsomorphicSetoid C) (isIsomorphicSetoid C)
      (fun X Y => Nonempty (X ⟶ Y))
        (by
          rintro _ _ _ _ ⟨i₁⟩ ⟨i₂⟩
          exact
            propext
              ⟨Nonempty.map fun f => i₁.inv ≫ f ≫ i₂.hom,
                Nonempty.map fun f => i₁.hom ≫ f ≫ i₂.inv⟩)
  le_refl := by
    refine Quotient.ind fun a => ?_
    exact ⟨𝟙 _⟩
  le_trans a b c := Quotient.inductionOn₃ a b c fun _ _ _ => Nonempty.map2 (· ≫ ·)

Preorder Structure on the Thin Skeleton of a Category

Informal description

The thin skeleton of a category $\mathcal{C}$ carries a canonical preorder structure, where the order relation is induced by the existence of morphisms in $\mathcal{C}$ between representatives of isomorphism classes.

CategoryTheory.toThinSkeleton definition

: C ⥤ ThinSkeleton C

Full source

/-- The functor from a category to its thin skeleton. -/
@[simps]
def toThinSkeleton : C ⥤ ThinSkeleton C where
  obj := @Quotient.mk' C _
  map f := homOfLE (Nonempty.intro f)

Functor to the thin skeleton of a category

Informal description

The functor from a category $\mathcal{C}$ to its thin skeleton, which maps each object to its isomorphism class and each morphism to the induced relation in the skeleton. Specifically, the functor sends an object $X$ to its equivalence class $[X]$ under the isomorphism relation, and a morphism $f : X \to Y$ to the relation $[X] \leq [Y]$ in the thin skeleton, which holds since there exists a morphism between representatives of these classes.

CategoryTheory.ThinSkeleton.thin instance

: Quiver.IsThin (ThinSkeleton C)

Full source

/-- The thin skeleton is thin. -/
instance thin : Quiver.IsThin (ThinSkeleton C) := fun _ _ =>
  ⟨by
    rintro ⟨⟨f₁⟩⟩ ⟨⟨_⟩⟩
    rfl⟩

Thin Skeleton is Thin

Informal description

The thin skeleton of a category $\mathcal{C}$ is a thin category, meaning there is at most one morphism between any two objects.

CategoryTheory.ThinSkeleton.map definition

(F : C ⥤ D) : ThinSkeleton C ⥤ ThinSkeleton D

Full source

/-- A functor `C ⥤ D` computably lowers to a functor `ThinSkeleton C ⥤ ThinSkeleton D`. -/
@[simps]
def map (F : C ⥤ D) : ThinSkeletonThinSkeleton C ⥤ ThinSkeleton D where
  obj := Quotient.map F.obj fun _ _ ⟨hX⟩ => ⟨F.mapIso hX⟩
  map {X} {Y} := Quotient.recOnSubsingleton₂ X Y fun _ _ k => homOfLE (k.le.elim fun t => ⟨F.map t⟩)

Functor between thin skeletons induced by a functor

Informal description

Given a functor $F \colon \mathcal{C} \to \mathcal{D}$, the induced functor $\text{ThinSkeleton} \mathcal{C} \to \text{ThinSkeleton} \mathcal{D}$ maps each isomorphism class of objects in $\mathcal{C}$ to the corresponding isomorphism class in $\mathcal{D}$ via $F$, and each morphism in the thin skeleton of $\mathcal{C}$ to the corresponding morphism in the thin skeleton of $\mathcal{D}$ induced by $F$.

CategoryTheory.ThinSkeleton.comp_toThinSkeleton theorem

(F : C ⥤ D) : F ⋙ toThinSkeleton D = toThinSkeleton C ⋙ map F

Full source

theorem comp_toThinSkeleton (F : C ⥤ D) : F ⋙ toThinSkeleton D = toThinSkeletontoThinSkeleton C ⋙ map F :=
  rfl

Functoriality of Thin Skeleton Construction: $F \circ \text{toThinSkeleton}_{\mathcal{D}} = \text{toThinSkeleton}_{\mathcal{C}} \circ \text{map}(F)$

Informal description

For any functor $F \colon \mathcal{C} \to \mathcal{D}$, the composition of $F$ with the functor to the thin skeleton of $\mathcal{D}$ is equal to the composition of the functor to the thin skeleton of $\mathcal{C}$ with the induced functor on thin skeletons. In other words, the following diagram commutes: \[ \begin{CD} \mathcal{C} @>{F}>> \mathcal{D} \\ @V{\text{toThinSkeleton}_{\mathcal{C}}}VV @VV{\text{toThinSkeleton}_{\mathcal{D}}}V \\ \text{ThinSkeleton}(\mathcal{C}) @>{\text{map}(F)}>> \text{ThinSkeleton}(\mathcal{D}) \end{CD} \]

CategoryTheory.ThinSkeleton.mapNatTrans definition

{F₁ F₂ : C ⥤ D} (k : F₁ ⟶ F₂) : map F₁ ⟶ map F₂

Full source

/-- Given a natural transformation `F₁ ⟶ F₂`, induce a natural transformation `map F₁ ⟶ map F₂`. -/
def mapNatTrans {F₁ F₂ : C ⥤ D} (k : F₁ ⟶ F₂) : mapmap F₁ ⟶ map F₂ where
  app X := Quotient.recOnSubsingleton X fun x => ⟨⟨⟨k.app x⟩⟩⟩

/- Porting note: `map₂ObjMap`, `map₂Functor`, and `map₂NatTrans` were all extracted
from the original `map₂` proof. Lean needed an extensive amount explicit type
annotations to figure things out. This also translated into repeated deterministic
timeouts. The extracted defs allow for explicit motives for the multiple
descents to the quotients.

It would be better to prove that
`ThinSkeleton (C × D) ≌ ThinSkeleton C × ThinSkeleton D`
which is more immediate from comparing the preorders. Then one could get
`map₂` by currying.
-/

Induced natural transformation on thin skeletons

Informal description

Given a natural transformation $k \colon F_1 \to F_2$ between functors $F_1, F_2 \colon \mathcal{C} \to \mathcal{D}$, this induces a natural transformation $\text{map} F_1 \to \text{map} F_2$ between the corresponding functors on the thin skeletons of $\mathcal{C}$ and $\mathcal{D}$. For each object $X$ in the thin skeleton of $\mathcal{C}$, the component of the induced natural transformation at $X$ is obtained by applying $k$ to a representative of the isomorphism class $X$.

CategoryTheory.ThinSkeleton.map₂ObjMap definition

(F : C ⥤ D ⥤ E) : ThinSkeleton C → ThinSkeleton D → ThinSkeleton E

Full source

/-- Given a bifunctor, we descend to a function on objects of `ThinSkeleton` -/
def map₂ObjMap (F : C ⥤ D ⥤ E) : ThinSkeleton C → ThinSkeleton D → ThinSkeleton E :=
  fun x y =>
    @Quotient.map₂ C D (isIsomorphicSetoid C) (isIsomorphicSetoid D) E (isIsomorphicSetoid E)
      (fun X Y => (F.obj X).obj Y)
          (fun X₁ _ ⟨hX⟩ _ Y₂ ⟨hY⟩ => ⟨(F.obj X₁).mapIso hY ≪≫ (F.mapIso hX).app Y₂⟩) x y

Object mapping of a bifunctor on thin skeletons

Informal description

Given a bifunctor $F \colon \mathcal{C} \to \mathcal{D} \to \mathcal{E}$, the function maps objects $x$ in the thin skeleton of $\mathcal{C}$ and $y$ in the thin skeleton of $\mathcal{D}$ to an object in the thin skeleton of $\mathcal{E}$. This is done by descending the bifunctor $F$ to a function on the isomorphism classes of objects in $\mathcal{C}$ and $\mathcal{D}$. Specifically, for objects $X$ in $\mathcal{C}$ and $Y$ in $\mathcal{D}$, the function maps the isomorphism classes of $X$ and $Y$ to the isomorphism class of $(F(X))(Y)$ in $\mathcal{E}$.

CategoryTheory.ThinSkeleton.map₂Functor definition

(F : C ⥤ D ⥤ E) : ThinSkeleton C → ThinSkeleton D ⥤ ThinSkeleton E

Full source

/-- For each `x : ThinSkeleton C`, we promote `map₂ObjMap F x` to a functor -/
def map₂Functor (F : C ⥤ D ⥤ E) : ThinSkeleton C → ThinSkeletonThinSkeleton D ⥤ ThinSkeleton E :=
  fun x =>
    { obj := fun y => map₂ObjMap F x y
      map := fun {y₁} {y₂} => @Quotient.recOnSubsingleton C (isIsomorphicSetoid C)
        (fun x => (y₁ ⟶ y₂) → (map₂ObjMapmap₂ObjMap F x y₁ ⟶ map₂ObjMap F x y₂)) _ x fun X
          => Quotient.recOnSubsingleton₂ y₁ y₂ fun _ _ hY =>
            homOfLE (hY.le.elim fun g => ⟨(F.obj X).map g⟩) }

Functorial action of a bifunctor on thin skeletons

Informal description

Given a bifunctor $ F \colon \mathcal{C} \to \mathcal{D} \to \mathcal{E} $, the function maps each object $ x $ in the thin skeleton of $\mathcal{C}$ to a functor from the thin skeleton of $\mathcal{D}$ to the thin skeleton of $\mathcal{E}$. For objects $ y_1 $ and $ y_2 $ in the thin skeleton of $\mathcal{D}$, the functor maps a morphism $ y_1 \to y_2 $ to a morphism $ F(x, y_1) \to F(x, y_2) $ in the thin skeleton of $\mathcal{E}$, where $ F(x, y) $ denotes the object obtained by applying the bifunctor $ F $ to representatives of the isomorphism classes $ x $ and $ y $.

CategoryTheory.ThinSkeleton.map₂NatTrans definition

 (F : C ⥤ D ⥤ E) : {x₁ x₂ : ThinSkeleton C} → (x₁ ⟶ x₂) → (map₂Functor F x₁ ⟶ map₂Functor F x₂)

Full source

/-- This provides natural transformations `map₂Functor F x₁ ⟶ map₂Functor F x₂` given
`x₁ ⟶ x₂` -/
def map₂NatTrans (F : C ⥤ D ⥤ E) : {x₁ x₂ : ThinSkeleton C} → (x₁ ⟶ x₂) →
    (map₂Functormap₂Functor F x₁ ⟶ map₂Functor F x₂) := fun {x₁} {x₂} =>
  @Quotient.recOnSubsingleton₂ C C (isIsomorphicSetoid C) (isIsomorphicSetoid C)
    (fun x x' : ThinSkeleton C => (x ⟶ x') → (map₂Functormap₂Functor F x ⟶ map₂Functor F x')) _ x₁ x₂
    (fun X₁ X₂ f => { app := fun y =>
      Quotient.recOnSubsingleton y fun Y => homOfLE (f.le.elim fun f' => ⟨(F.map f').app Y⟩) })

Natural transformation induced by a morphism in the thin skeleton

Informal description

Given a bifunctor $ F \colon \mathcal{C} \to \mathcal{D} \to \mathcal{E} $, for any objects $ x_1 $ and $ x_2 $ in the thin skeleton of $\mathcal{C}$ and a morphism $ f \colon x_1 \to x_2 $, this defines a natural transformation from the functor $ \text{map₂Functor}\, F\, x_1 $ to $ \text{map₂Functor}\, F\, x_2 $. The natural transformation is constructed by descending the morphism $ f $ to a morphism between the corresponding functors applied to representatives of the isomorphism classes $ x_1 $ and $ x_2 $.

CategoryTheory.ThinSkeleton.map₂ definition

(F : C ⥤ D ⥤ E) : ThinSkeleton C ⥤ ThinSkeleton D ⥤ ThinSkeleton E

Full source

/-- A functor `C ⥤ D ⥤ E` computably lowers to a functor
`ThinSkeleton C ⥤ ThinSkeleton D ⥤ ThinSkeleton E` -/
@[simps]
def map₂ (F : C ⥤ D ⥤ E) : ThinSkeletonThinSkeleton C ⥤ ThinSkeleton D ⥤ ThinSkeleton E where
  obj := map₂Functor F
  map := map₂NatTrans F

Functorial action of a bifunctor on thin skeletons

Informal description

Given a bifunctor $ F \colon \mathcal{C} \to \mathcal{D} \to \mathcal{E} $, this defines a functor from the thin skeleton of $\mathcal{C}$ to the category of functors from the thin skeleton of $\mathcal{D}$ to the thin skeleton of $\mathcal{E}$. The functor maps each object $ x $ in the thin skeleton of $\mathcal{C}$ to the functor $\text{map₂Functor}\, F\, x$, and each morphism $ f \colon x_1 \to x_2 $ to the natural transformation $\text{map₂NatTrans}\, F\, f$.

CategoryTheory.ThinSkeleton.toThinSkeleton_faithful instance

: (toThinSkeleton C).Faithful

Full source

instance toThinSkeleton_faithful : (toThinSkeleton C).Faithful where

Faithfulness of the Functor to the Thin Skeleton

Informal description

The functor from a category $\mathcal{C}$ to its thin skeleton is faithful, meaning it is injective on morphisms between any two objects.

CategoryTheory.ThinSkeleton.fromThinSkeleton definition

: ThinSkeleton C ⥤ C

Full source

/-- Use `Quotient.out` to create a functor out of the thin skeleton. -/
@[simps]
noncomputable def fromThinSkeleton : ThinSkeletonThinSkeleton C ⥤ C where
  obj := Quotient.out
  map {x} {y} :=
    Quotient.recOnSubsingleton₂ x y fun X Y f =>
      (Nonempty.some (Quotient.mk_out X)).hom ≫ f.le.some ≫ (Nonempty.some (Quotient.mk_out Y)).inv

Functor from thin skeleton to original category

Informal description

The functor from the thin skeleton of a category $\mathcal{C}$ back to $\mathcal{C}$ is defined by mapping each isomorphism class to a representative object via `Quotient.out`. For morphisms, given two isomorphism classes $x$ and $y$ in the thin skeleton, the functor maps a morphism $f : x \to y$ to a composite morphism in $\mathcal{C}$ constructed using representatives of the isomorphism classes and the morphism $f$.

CategoryTheory.ThinSkeleton.equivalence definition

: ThinSkeleton C ≌ C

Full source

/-- The equivalence between the thin skeleton and the category itself. -/
noncomputable def equivalence : ThinSkeletonThinSkeleton C ≌ C where
  functor := fromThinSkeleton C
  inverse := toThinSkeleton C
  counitIso := NatIso.ofComponents fun X => Nonempty.some (Quotient.mk_out X)
  unitIso := NatIso.ofComponents fun x => Quotient.recOnSubsingleton x fun X =>
    eqToIso (Quotient.sound ⟨(Nonempty.some (Quotient.mk_out X)).symm⟩)

Equivalence between a category and its thin skeleton

Informal description

The equivalence between the thin skeleton of a category $\mathcal{C}$ and $\mathcal{C}$ itself, consisting of: - A functor from the thin skeleton to $\mathcal{C}$ that maps each isomorphism class to a representative object, - A functor from $\mathcal{C}$ to its thin skeleton that maps each object to its isomorphism class, - Natural isomorphisms witnessing that these functors form an equivalence of categories.

CategoryTheory.ThinSkeleton.fromThinSkeleton_isEquivalence instance

: (fromThinSkeleton C).IsEquivalence

Full source

noncomputable instance fromThinSkeleton_isEquivalence : (fromThinSkeleton C).IsEquivalence :=
  (equivalence C).isEquivalence_functor

Equivalence of the Thin Skeleton Functor

Informal description

The functor from the thin skeleton of a category $\mathcal{C}$ back to $\mathcal{C}$ is an equivalence of categories. This means that the functor is full, faithful, and essentially surjective, establishing a categorical equivalence between the thin skeleton and the original category.

CategoryTheory.ThinSkeleton.equiv_of_both_ways theorem

{X Y : C} (f : X ⟶ Y) (g : Y ⟶ X) : X ≈ Y

Full source

theorem equiv_of_both_ways {X Y : C} (f : X ⟶ Y) (g : Y ⟶ X) : X ≈ Y :=
  ⟨iso_of_both_ways f g⟩

Equivalence in Thin Skeleton via Bidirectional Morphisms

Informal description

In a thin category $\mathcal{C}$, given any two objects $X$ and $Y$ and morphisms $f : X \to Y$ and $g : Y \to X$, the objects $X$ and $Y$ are equivalent in the thin skeleton of $\mathcal{C}$, denoted $X \approx Y$.

CategoryTheory.ThinSkeleton.thinSkeletonPartialOrder instance

: PartialOrder (ThinSkeleton C)

Full source

instance thinSkeletonPartialOrder : PartialOrder (ThinSkeleton C) :=
  { CategoryTheory.ThinSkeleton.preorder C with
    le_antisymm :=
      Quotient.ind₂
        (by
          rintro _ _ ⟨f⟩ ⟨g⟩
          apply Quotient.sound (equiv_of_both_ways f g)) }

Partial Order Structure on the Thin Skeleton of a Category

Informal description

The thin skeleton of a category $\mathcal{C}$ carries a canonical partial order structure, where the order relation is induced by the existence of morphisms in $\mathcal{C}$ between representatives of isomorphism classes.

CategoryTheory.ThinSkeleton.skeletal theorem

: Skeletal (ThinSkeleton C)

Full source

theorem skeletal : Skeletal (ThinSkeleton C) := fun X Y =>
  Quotient.inductionOn₂ X Y fun _ _ h => h.elim fun i => i.1.le.antisymm i.2.le

Thin Skeleton is Skeletal

Informal description

The thin skeleton of a category $\mathcal{C}$ is skeletal, meaning that any two isomorphic objects in the thin skeleton are equal. In other words, if $X$ and $Y$ are objects in the thin skeleton of $\mathcal{C}$ such that $X \cong Y$, then $X = Y$.

CategoryTheory.ThinSkeleton.map_comp_eq theorem

(F : E ⥤ D) (G : D ⥤ C) : map (F ⋙ G) = map F ⋙ map G

Full source

theorem map_comp_eq (F : E ⥤ D) (G : D ⥤ C) : map (F ⋙ G) = mapmap F ⋙ map G :=
  Functor.eq_of_iso skeletal <|
    NatIso.ofComponents fun X => Quotient.recOnSubsingleton X fun _ => Iso.refl _

Functoriality of Thin Skeleton Construction: $\text{map}(F \circ G) = \text{map}(F) \circ \text{map}(G)$

Informal description

For any functors $F \colon \mathcal{E} \to \mathcal{D}$ and $G \colon \mathcal{D} \to \mathcal{C}$, the induced functor on thin skeletons satisfies $\text{map}(F \circ G) = \text{map}(F) \circ \text{map}(G)$.

CategoryTheory.ThinSkeleton.map_id_eq theorem

: map (𝟭 C) = 𝟭 (ThinSkeleton C)

Full source

theorem map_id_eq : map (𝟭 C) = 𝟭 (ThinSkeleton C) :=
  Functor.eq_of_iso skeletal <|
    NatIso.ofComponents fun X => Quotient.recOnSubsingleton X fun _ => Iso.refl _

Identity Functor Preserved by Thin Skeleton Construction

Informal description

The functor induced by the identity functor on a category $\mathcal{C}$ is equal to the identity functor on the thin skeleton of $\mathcal{C}$. That is, $\text{map}(1_{\mathcal{C}}) = 1_{\text{ThinSkeleton}(\mathcal{C})}$.

CategoryTheory.ThinSkeleton.map_iso_eq theorem

{F₁ F₂ : D ⥤ C} (h : F₁ ≅ F₂) : map F₁ = map F₂

Full source

theorem map_iso_eq {F₁ F₂ : D ⥤ C} (h : F₁ ≅ F₂) : map F₁ = map F₂ :=
  Functor.eq_of_iso skeletal
    { hom := mapNatTrans h.hom
      inv := mapNatTrans h.inv }

Equality of Induced Functors on Thin Skeletons for Naturally Isomorphic Functors

Informal description

For any two naturally isomorphic functors $F_1, F_2 \colon \mathcal{D} \to \mathcal{C}$, the induced functors on the thin skeletons are equal, i.e., $\text{map}(F_1) = \text{map}(F_2)$.

CategoryTheory.ThinSkeleton.thinSkeleton_isSkeleton theorem

: IsSkeletonOf C (ThinSkeleton C) (fromThinSkeleton C)

Full source

/-- `fromThinSkeleton C` exhibits the thin skeleton as a skeleton. -/
lemma thinSkeleton_isSkeleton : IsSkeletonOf C (ThinSkeleton C) (fromThinSkeleton C) where
  skel := skeletal

Thin Skeleton is a Skeleton of the Original Category

Informal description

The functor $\text{fromThinSkeleton}\, C \colon \text{ThinSkeleton}\, C \to C$ exhibits the thin skeleton of a category $C$ as a skeleton of $C$. That is: 1. The functor is an equivalence of categories. 2. The thin skeleton $\text{ThinSkeleton}\, C$ is skeletal (any two isomorphic objects are equal).

CategoryTheory.ThinSkeleton.isSkeletonOfInhabited instance

: Inhabited (IsSkeletonOf C (ThinSkeleton C) (fromThinSkeleton C))

Full source

instance isSkeletonOfInhabited :
    Inhabited (IsSkeletonOf C (ThinSkeleton C) (fromThinSkeleton C)) :=
  ⟨thinSkeleton_isSkeleton⟩

Existence of a Skeleton via Thin Skeleton Construction

Informal description

For any category $\mathcal{C}$, the thin skeleton $\text{ThinSkeleton}(\mathcal{C})$ equipped with the functor $\text{fromThinSkeleton}(\mathcal{C}) \colon \text{ThinSkeleton}(\mathcal{C}) \to \mathcal{C}$ is a skeleton of $\mathcal{C}$. That is, the functor is an equivalence of categories and the thin skeleton is skeletal (any two isomorphic objects are equal).

CategoryTheory.ThinSkeleton.lowerAdjunction definition

(R : D ⥤ C) (L : C ⥤ D) (h : L ⊣ R) : ThinSkeleton.map L ⊣ ThinSkeleton.map R

Full source

/-- An adjunction between thin categories gives an adjunction between their thin skeletons. -/
def lowerAdjunction (R : D ⥤ C) (L : C ⥤ D) (h : L ⊣ R) :
    ThinSkeleton.mapThinSkeleton.map L ⊣ ThinSkeleton.map R where
  unit :=
    { app := fun X => by
        letI := isIsomorphicSetoid C
        exact Quotient.recOnSubsingleton X fun x => homOfLE ⟨h.unit.app x⟩ }
      -- TODO: make quotient.rec_on_subsingleton' so the letI isn't needed
  counit :=
    { app := fun X => by
        letI := isIsomorphicSetoid D
        exact Quotient.recOnSubsingleton X fun x => homOfLE ⟨h.counit.app x⟩ }

Adjunction between thin skeletons induced by an adjunction between thin categories

Informal description

Given an adjunction $L \dashv R$ between thin categories $\mathcal{C}$ and $\mathcal{D}$, there is an induced adjunction $\text{ThinSkeleton}(L) \dashv \text{ThinSkeleton}(R)$ between their thin skeletons. Here, $\text{ThinSkeleton}(L)$ and $\text{ThinSkeleton}(R)$ are the functors induced by $L$ and $R$ on the thin skeletons, respectively. The unit and counit of the induced adjunction are constructed by applying the original unit and counit to representatives of isomorphism classes.

CategoryTheory.Equivalence.thinSkeletonOrderIso definition

[Quiver.IsThin C] (e : C ≌ α) : ThinSkeleton C ≃o α

Full source

/--
When `e : C ≌ α` is a categorical equivalence from a thin category `C` to some partial order `α`,
the `ThinSkeleton C` is order isomorphic to `α`.
-/
noncomputable def Equivalence.thinSkeletonOrderIso [Quiver.IsThin C] (e : C ≌ α) :
    ThinSkeletonThinSkeleton C ≃o α :=
  ((ThinSkeleton.equivalence C).trans e).toOrderIso

Order isomorphism between thin skeleton and partial order via equivalence

Informal description

Given a thin category $C$ and an equivalence $e \colon C \simeq \alpha$ to a partial order $\alpha$, the thin skeleton $\text{ThinSkeleton}(C)$ is order isomorphic to $\alpha$. More precisely, the composition of the equivalence between $C$ and its thin skeleton with $e$ yields an order isomorphism between $\text{ThinSkeleton}(C)$ and $\alpha$.