CategoryTheory.Grpd.hom_to_functor
theorem CategoryTheory.Grpd.hom_to_functor :
∀ {C D E : CategoryTheory.Grpd} (f : C ⟶ D) (g : D ⟶ E),
CategoryTheory.CategoryStruct.comp f g = CategoryTheory.Functor.comp f g
This theorem is about the conversion of arrows in the category of groupoids to functors. Specifically, it states that for any three groupoids `C`, `D`, and `E` and any two morphisms `f` from `C` to `D` and `g` from `D` to `E` in the category of groupoids, the composition of `f` and `g` under the category structure is equal to the composition of `f` and `g` as functors. This conversion can often be useful in applying simplification lemmas.
More concisely: For any groupoids `C`, `D`, and `E`, and morphisms `f : C -> D` and `g : D -> E` in the category of groupoids, the functor composition `g ∘ f` is equal to the category composition `g (f X)` for any object `X` in `C`.
|
CategoryTheory.Grpd.id_to_functor
theorem CategoryTheory.Grpd.id_to_functor :
∀ {C : CategoryTheory.Grpd}, CategoryTheory.Functor.id ↑C = CategoryTheory.CategoryStruct.id C
This theorem states that for any groupoid `C` in the category of groupoids, the identity functor on `C` is the same as the identity morphism on `C`. The identity functor maps each object and morphism in the groupoid to itself, while the identity morphism is a morphism that serves as an identity element in morphism composition. In other words, the identity for a groupoid in the category of groupoids is the same whether we consider it as a functor or as a morphism.
More concisely: In the category of groupoids, the identity functor and identity morphism on a groupoid `C` coincide, that is, the identity functor is the endofunctor that maps each object and morphism in `C` to itself.
|