Documentation

Mathlib.CategoryTheory.Skeletal

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.

A category is skeletal if isomorphic objects are equal.

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

    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.

    Instances For

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

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

      Instances For

        The functor from the skeleton of C to C.

        Instances For

          The equivalence between the skeleton and the category itself.

          Instances For

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

            Instances For

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

              Instances For

                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.

                Instances For

                  The functor from a category to its thin skeleton.

                  Instances For

                    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.

                    @[simp]
                    theorem CategoryTheory.ThinSkeleton.map_map {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [CategoryTheory.Category.{v₂, u₂} D] (F : CategoryTheory.Functor C D) {X : CategoryTheory.ThinSkeleton C} {Y : CategoryTheory.ThinSkeleton C} :
                    ∀ (a : X Y), (CategoryTheory.ThinSkeleton.map F).map a = Quotient.recOnSubsingleton₂ (motive := fun x x_1 => (x x_1) → (Quotient.map F.obj (_ : ∀ (X₁ X₂ : C), X₁ X₂(fun x x_2 => x x_2) (F.obj X₁) (F.obj X₂)) x Quotient.map F.obj (_ : ∀ (X₁ X₂ : C), X₁ X₂(fun x x_2 => x x_2) (F.obj X₁) (F.obj X₂)) x_1)) X Y (fun x y k => CategoryTheory.homOfLE (_ : Quotient.map F.obj (_ : ∀ (X₁ X₂ : C), X₁ X₂(fun x x_1 => x x_1) (F.obj X₁) (F.obj X₂)) (Quotient.mk (CategoryTheory.isIsomorphicSetoid C) x) Quotient.map F.obj (_ : ∀ (X₁ X₂ : C), X₁ X₂(fun x x_1 => x x_1) (F.obj X₁) (F.obj X₂)) (Quotient.mk (CategoryTheory.isIsomorphicSetoid C) y))) a
                    @[simp]
                    theorem CategoryTheory.ThinSkeleton.map_obj {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [CategoryTheory.Category.{v₂, u₂} D] (F : CategoryTheory.Functor C D) :
                    ∀ (a : Quotient (CategoryTheory.isIsomorphicSetoid C)), (CategoryTheory.ThinSkeleton.map F).obj a = Quotient.map F.obj (_ : ∀ (X₁ X₂ : C), X₁ X₂(fun x x_1 => x x_1) (F.obj X₁) (F.obj X₂)) a

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

                    Instances For

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

                      Instances For

                        The equivalence between the thin skeleton and the category itself.

                        Instances For

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

                          Instances For

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

                            Instances For