Skeleton of a category
Define skeletal categories as categories in which any two isomorphic objects are equal.
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 (TODO). In addition, some of the commutative diagrams about the functors commute definitionally on the nose which is convenient in practice.
(TODO): Construct the skeleton of a general category using choice, and show it is a skeleton.
A category is skeletal if isomorphic objects are equal.
Equations
- category_theory.skeletal C = ∀ ⦃X Y : C⦄, category_theory.is_isomorphic X Y → X = Y
structure
category_theory.is_skeleton_of
(C : Type u₁)
[category_theory.category C]
(D : Type u₂)
[category_theory.category D]
(F : D ⥤ C) :
Type (max u₁ u₂ v₁ v₂)
- skel : category_theory.skeletal D
- eqv : category_theory.is_equivalence F
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.
theorem
category_theory.functor.eq_of_iso
{C : Type u₁}
[category_theory.category C]
{D : Type u₂}
[category_theory.category D]
{F₁ F₂ : D ⥤ C}
[∀ (X Y : C), subsingleton (X ⟶ Y)]
(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₁}
[category_theory.category C]
{D : Type u₂}
[category_theory.category D]
[∀ (X Y : C), subsingleton (X ⟶ Y)]
(hC : category_theory.skeletal C) :
category_theory.skeletal (D ⥤ C)
If C is thin and skeletal, D ⥤ C is skeletal.
category_theory.functor_thin shows it is thin also.
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.
Equations
@[instance]
def
category_theory.inhabited_thin_skeleton
(C : Type u₁)
[category_theory.category C]
[inhabited C] :
@[instance]
Equations
- category_theory.thin_skeleton.preorder C = {le := quotient.lift₂ (λ (X Y : C), nonempty (X ⟶ Y)) _, lt := λ (a b : category_theory.thin_skeleton C), quotient.lift₂ (λ (X Y : C), nonempty (X ⟶ Y)) _ a b ∧ ¬quotient.lift₂ (λ (X Y : C), nonempty (X ⟶ Y)) _ b a, le_refl := _, le_trans := _, lt_iff_le_not_le := _}
The functor from a category to its thin skeleton.
Equations
- category_theory.to_thin_skeleton C = {obj := quotient.mk (category_theory.is_isomorphic_setoid C), map := λ (X Y : C) (f : X ⟶ Y), category_theory.hom_of_le _, map_id' := _, map_comp' := _}
@[simp]
theorem
category_theory.to_thin_skeleton_map
(C : Type u₁)
[category_theory.category C]
(X Y : C)
(f : X ⟶ Y) :
@[simp]
theorem
category_theory.to_thin_skeleton_obj
(C : Type u₁)
[category_theory.category C]
(a : C) :
(category_theory.to_thin_skeleton C).obj a = ⟦a⟧
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]
def
category_theory.thin_skeleton.thin
(C : Type u₁)
[category_theory.category C]
{X Y : category_theory.thin_skeleton C} :
subsingleton (X ⟶ Y)
The thin skeleton is thin.
@[simp]
theorem
category_theory.thin_skeleton.map_obj
{C : Type u₁}
[category_theory.category C]
{D : Type u₂}
[category_theory.category D]
(F : C ⥤ D)
(a : quotient (category_theory.is_isomorphic_setoid C)) :
(category_theory.thin_skeleton.map F).obj a = quotient.map F.obj _ a
@[simp]
theorem
category_theory.thin_skeleton.map_map
{C : Type u₁}
[category_theory.category C]
{D : Type u₂}
[category_theory.category D]
(F : C ⥤ D)
(X Y : category_theory.thin_skeleton C) :
(category_theory.thin_skeleton.map F).map = quotient.rec_on_subsingleton₂ X Y (λ (x y : C) (k : ⟦x⟧ ⟶ ⟦y⟧), category_theory.hom_of_le _)
def
category_theory.thin_skeleton.map
{C : Type u₁}
[category_theory.category C]
{D : Type u₂}
[category_theory.category D]
(F : C ⥤ D) :
A functor C ⥤ D computably lowers to a functor thin_skeleton C ⥤ thin_skeleton D.
Equations
- category_theory.thin_skeleton.map F = {obj := quotient.map F.obj _, map := λ (X Y : category_theory.thin_skeleton C), quotient.rec_on_subsingleton₂ X Y (λ (x y : C) (k : ⟦x⟧ ⟶ ⟦y⟧), category_theory.hom_of_le _), map_id' := _, map_comp' := _}
theorem
category_theory.thin_skeleton.comp_to_thin_skeleton
{C : Type u₁}
[category_theory.category C]
{D : Type u₂}
[category_theory.category D]
(F : C ⥤ D) :
def
category_theory.thin_skeleton.map_nat_trans
{C : Type u₁}
[category_theory.category C]
{D : Type u₂}
[category_theory.category D]
{F₁ F₂ : C ⥤ D}
(k : F₁ ⟶ F₂) :
Given a natural transformation F₁ ⟶ F₂, induce a natural transformation map F₁ ⟶ map F₂.
Equations
- category_theory.thin_skeleton.map_nat_trans k = {app := λ (X : category_theory.thin_skeleton C), quotient.rec_on_subsingleton X (λ (x : C), {down := {down := _}}), naturality' := _}
@[simp]
theorem
category_theory.thin_skeleton.map₂_obj_obj
{C : Type u₁}
[category_theory.category C]
{D : Type u₂}
[category_theory.category D]
{E : Type u₃}
[category_theory.category E]
(F : C ⥤ D ⥤ E)
(x : category_theory.thin_skeleton C)
(y : category_theory.thin_skeleton D) :
((category_theory.thin_skeleton.map₂ F).obj x).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₁}
[category_theory.category C]
{D : Type u₂}
[category_theory.category D]
{E : Type u₃}
[category_theory.category E]
(F : C ⥤ D ⥤ E)
(x : category_theory.thin_skeleton C)
(y₁ y₂ : category_theory.thin_skeleton D) :
((category_theory.thin_skeleton.map₂ F).obj x).map = quotient.rec_on_subsingleton x (λ (X : C), quotient.rec_on_subsingleton₂ y₁ y₂ (λ (Y₁ Y₂ : D) (hY : ⟦Y₁⟧ ⟶ ⟦Y₂⟧), category_theory.hom_of_le _))
@[simp]
theorem
category_theory.thin_skeleton.map₂_map
{C : Type u₁}
[category_theory.category C]
{D : Type u₂}
[category_theory.category D]
{E : Type u₃}
[category_theory.category E]
(F : C ⥤ D ⥤ E)
(x₁ x₂ : category_theory.thin_skeleton C) :
(category_theory.thin_skeleton.map₂ F).map = quotient.rec_on_subsingleton₂ x₁ x₂ (λ (X₁ X₂ : C) (f : ⟦X₁⟧ ⟶ ⟦X₂⟧), {app := λ (y : category_theory.thin_skeleton D), quotient.rec_on_subsingleton y (λ (Y : D), category_theory.hom_of_le _), naturality' := _})
def
category_theory.thin_skeleton.map₂
{C : Type u₁}
[category_theory.category C]
{D : Type u₂}
[category_theory.category D]
{E : Type u₃}
[category_theory.category E]
(F : C ⥤ D ⥤ E) :
A functor C ⥤ D ⥤ E computably lowers to a functor
thin_skeleton C ⥤ thin_skeleton D ⥤ thin_skeleton E
Equations
- category_theory.thin_skeleton.map₂ F = {obj := λ (x : category_theory.thin_skeleton C), {obj := λ (y : category_theory.thin_skeleton D), quotient.map₂ (λ (X : C) (Y : D), (F.obj X).obj Y) _ x y, map := λ (y₁ y₂ : category_theory.thin_skeleton D), quotient.rec_on_subsingleton x (λ (X : C), quotient.rec_on_subsingleton₂ y₁ y₂ (λ (Y₁ Y₂ : D) (hY : ⟦Y₁⟧ ⟶ ⟦Y₂⟧), category_theory.hom_of_le _)), map_id' := _, map_comp' := _}, map := λ (x₁ x₂ : category_theory.thin_skeleton C), quotient.rec_on_subsingleton₂ x₁ x₂ (λ (X₁ X₂ : C) (f : ⟦X₁⟧ ⟶ ⟦X₂⟧), {app := λ (y : category_theory.thin_skeleton D), quotient.rec_on_subsingleton y (λ (Y : D), category_theory.hom_of_le _), naturality' := _}), map_id' := _, map_comp' := _}
@[instance]
def
category_theory.thin_skeleton.to_thin_skeleton_faithful
(C : Type u₁)
[category_theory.category C]
[∀ (X Y : C), subsingleton (X ⟶ Y)] :
@[simp]
theorem
category_theory.thin_skeleton.from_thin_skeleton_map
(C : Type u₁)
[category_theory.category C]
[∀ (X Y : C), subsingleton (X ⟶ Y)]
(x y : category_theory.thin_skeleton C) :
(category_theory.thin_skeleton.from_thin_skeleton C).map = quotient.rec_on_subsingleton₂ x y (λ (X Y : C) (f : ⟦X⟧ ⟶ ⟦Y⟧), (nonempty.some _).hom ≫ nonempty.some _ ≫ (nonempty.some _).inv)
def
category_theory.thin_skeleton.from_thin_skeleton
(C : Type u₁)
[category_theory.category C]
[∀ (X Y : C), subsingleton (X ⟶ Y)] :
Use quotient.out to create a functor out of the thin skeleton.
Equations
- category_theory.thin_skeleton.from_thin_skeleton C = {obj := quotient.out (category_theory.is_isomorphic_setoid C), map := λ (x y : category_theory.thin_skeleton C), quotient.rec_on_subsingleton₂ x y (λ (X Y : C) (f : ⟦X⟧ ⟶ ⟦Y⟧), (nonempty.some _).hom ≫ nonempty.some _ ≫ (nonempty.some _).inv), map_id' := _, map_comp' := _}
@[simp]
theorem
category_theory.thin_skeleton.from_thin_skeleton_obj
(C : Type u₁)
[category_theory.category C]
[∀ (X Y : C), subsingleton (X ⟶ Y)]
(a : quotient (category_theory.is_isomorphic_setoid C)) :
@[instance]
def
category_theory.thin_skeleton.from_thin_skeleton_equivalence
(C : Type u₁)
[category_theory.category C]
[∀ (X Y : C), subsingleton (X ⟶ Y)] :
Equations
- category_theory.thin_skeleton.from_thin_skeleton_equivalence C = {inverse := category_theory.to_thin_skeleton C _inst_1, unit_iso := category_theory.nat_iso.of_components (λ (x : category_theory.thin_skeleton C), quotient.rec_on_subsingleton x (λ (X : C), category_theory.eq_to_iso _)) _, counit_iso := category_theory.nat_iso.of_components (λ (X : C), nonempty.some _) _, functor_unit_iso_comp' := _}
theorem
category_theory.thin_skeleton.equiv_of_both_ways
{C : Type u₁}
[category_theory.category C]
[∀ (X Y : C), subsingleton (X ⟶ Y)]
{X Y : C}
(f : X ⟶ Y)
(g : Y ⟶ X) :
X ≈ Y
@[instance]
def
category_theory.thin_skeleton.thin_skeleton_partial_order
{C : Type u₁}
[category_theory.category C]
[∀ (X Y : C), subsingleton (X ⟶ Y)] :
Equations
- category_theory.thin_skeleton.thin_skeleton_partial_order = {le := preorder.le (category_theory.thin_skeleton.preorder C), lt := preorder.lt (category_theory.thin_skeleton.preorder C), le_refl := _, le_trans := _, lt_iff_le_not_le := _, le_antisymm := _}
theorem
category_theory.thin_skeleton.skeletal
{C : Type u₁}
[category_theory.category C]
[∀ (X Y : C), subsingleton (X ⟶ Y)] :
theorem
category_theory.thin_skeleton.map_comp_eq
{C : Type u₁}
[category_theory.category C]
{D : Type u₂}
[category_theory.category D]
{E : Type u₃}
[category_theory.category E]
[∀ (X Y : C), subsingleton (X ⟶ Y)]
(F : E ⥤ D)
(G : D ⥤ C) :
theorem
category_theory.thin_skeleton.map_id_eq
{C : Type u₁}
[category_theory.category C]
[∀ (X Y : C), subsingleton (X ⟶ Y)] :
theorem
category_theory.thin_skeleton.map_iso_eq
{C : Type u₁}
[category_theory.category C]
{D : Type u₂}
[category_theory.category D]
[∀ (X Y : C), subsingleton (X ⟶ Y)]
{F₁ F₂ : D ⥤ C}
(h : F₁ ≅ F₂) :
def
category_theory.thin_skeleton.thin_skeleton_is_skeleton
{C : Type u₁}
[category_theory.category C]
[∀ (X Y : C), subsingleton (X ⟶ Y)] :
from_thin_skeleton C exhibits the thin skeleton as a skeleton.
Equations
- category_theory.thin_skeleton.thin_skeleton_is_skeleton = {skel := _, eqv := category_theory.thin_skeleton.from_thin_skeleton_equivalence C category_theory.thin_skeleton.thin_skeleton_is_skeleton._proof_4}
@[instance]
def
category_theory.thin_skeleton.is_skeleton_of_inhabited
{C : Type u₁}
[category_theory.category C]
[∀ (X Y : C), subsingleton (X ⟶ Y)] :
Equations
- category_theory.thin_skeleton.is_skeleton_of_inhabited = {default := category_theory.thin_skeleton.thin_skeleton_is_skeleton category_theory.thin_skeleton.is_skeleton_of_inhabited._proof_3}