CategoryTheory.Functor.eq_of_iso
theorem CategoryTheory.Functor.eq_of_iso :
∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂}
[inst_1 : CategoryTheory.Category.{v₂, u₂} D] {F₁ F₂ : CategoryTheory.Functor D C} [inst_2 : Quiver.IsThin C],
CategoryTheory.Skeletal C → (F₁ ≅ F₂) → F₁ = F₂
The theorem `CategoryTheory.Functor.eq_of_iso` states that for any given categories `C` and `D`, if `C` is both thin and skeletal, then any two functors `F₁` and `F₂` from `D` to `C` that are naturally isomorphic are in fact equal.
To elaborate, "thin" refers to a quiver (a directed graph that may have multiple arrows between nodes) that has no parallel arrows. In the context of categories, this means there is at most one morphism between any two objects. "Skeletal" refers to a category in which any two isomorphic objects are equal, meaning there are no two distinct objects that have the same structure. The theorem states that under these conditions, naturally isomorphic functors, which are functors with a specific type of correspondence between the structures they map, must be equal.
More concisely: In categories `C` that are both thin and skeletal, any two naturally isomorphic functors from another category to `C` are equal.
|
CategoryTheory.IsSkeletonOf.skel
theorem CategoryTheory.IsSkeletonOf.skel :
∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂}
[inst_1 : CategoryTheory.Category.{v₂, u₂} D] {F : CategoryTheory.Functor D C},
CategoryTheory.IsSkeletonOf C D F → CategoryTheory.Skeletal D
The theorem `CategoryTheory.IsSkeletonOf.skel` states that for any given categories `C` and `D` with a functor `F` from `D` to `C`, if `C` is a skeleton of `D` via the functor `F`, then `D` is a skeletal category. Essentially, in the category `D`, any two objects that are isomorphic are actually identical.
More concisely: If category `C` is a skeleton of category `D` via functor `F`, then `D` is a skeletal category, i.e., any two isomorphic objects in `D` are equal.
|
CategoryTheory.ThinSkeleton.skeletal
theorem CategoryTheory.ThinSkeleton.skeletal :
∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] [inst_1 : Quiver.IsThin C],
CategoryTheory.Skeletal (CategoryTheory.ThinSkeleton C)
This theorem states that for any type `C` that is both a category and a thin quiver (i.e., a category in which there are no parallel arrows), the thin skeleton of `C` is skeletal. Here, a category is said to be skeletal if any two objects in the category that are isomorphic are actually identical. It implies that in the thin skeleton of a thin category, isomorphic objects are necessarily identical.
More concisely: In a thin quiver category `C`, the thin skeleton is a skeletal category, meaning isomorphic objects are identical.
|
CategoryTheory.functor_skeletal
theorem CategoryTheory.functor_skeletal :
∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂}
[inst_1 : CategoryTheory.Category.{v₂, u₂} D] [inst_2 : Quiver.IsThin C],
CategoryTheory.Skeletal C → CategoryTheory.Skeletal (CategoryTheory.Functor D C)
The theorem `CategoryTheory.functor_skeletal` states that if a category `C` is both thin (meaning it has no parallel arrows) and skeletal (meaning that isomorphic objects are equal), then the category of functors from any category `D` to `C` is also skeletal. The statement `CategoryTheory.functor_thin` asserts that this category of functors is also thin.
More concisely: If category `C` is both thin and skeletal, then the category of functors from any category `D` to `C` is both thin and skeletal.
|