Mathlib.CategoryTheory.Idempotents.FunctorExtension._auxLemma.1
theorem Mathlib.CategoryTheory.Idempotents.FunctorExtension._auxLemma.1 :
∀ {C : Type u_1} [inst : CategoryTheory.Category.{u_2, u_1} C] {P Q : CategoryTheory.Idempotents.Karoubi C}
{f g : P ⟶ Q}, (f = g) = (f.f = g.f)
This theorem states that in the context of category theory, for any category `C` and any two objects `P` and `Q` in the Karoubi envelope of `C`, if `f` and `g` are morphisms from `P` to `Q`, then `f` is equal to `g` if and only if the underlying morphisms `f.f` and `g.f` are equal. The Karoubi envelope is a construction in category theory that encapsulates the concept of idempotents.
More concisely: In the category theory of Karoubi envelopes, two morphisms from the same object to another have equal underlying morphisms if and only if they represent the same morphism.
|
CategoryTheory.Idempotents.natTrans_eq
theorem CategoryTheory.Idempotents.natTrans_eq :
∀ {C : Type u_1} {D : Type u_2} [inst : CategoryTheory.Category.{u_4, u_1} C]
[inst_1 : CategoryTheory.Category.{u_5, u_2} D]
{F G : CategoryTheory.Functor (CategoryTheory.Idempotents.Karoubi C) D} (φ : F ⟶ G)
(P : CategoryTheory.Idempotents.Karoubi C),
φ.app P =
CategoryTheory.CategoryStruct.comp (F.map P.decompId_i)
(CategoryTheory.CategoryStruct.comp (φ.app { X := P.X, p := CategoryTheory.CategoryStruct.id P.X, idem := ⋯ })
(G.map P.decompId_p))
This theorem states that for any categories `C` and `D`, and any functors `F` and `G` from the karoubization of `C` to `D`, a natural transformation `φ` between `F` and `G` is determined by its value on objects in `C`. More specifically, the application of `φ` to an object `P` in the karoubization of `C` is equal to the composition of three morphisms: the application of the `F` functor to the identity morphism of `P` decomposed, the application of `φ` to `P` with identity morphism and some idempotency condition, and the application of the `G` functor to the projection of the decomposition of `P`. This theorem essentially describes a specific property of natural transformations in the context of category theory and karoubi envelopes.
More concisely: Given categories `C` and `D`, functors `F` and `G` from the karoubization of `C` to `D`, and a natural transformation `φ` between `F` and `G`, the value of `φ` on an object `P` in the karoubization of `C` is equal to the composition of `F(id_P)`, `φ(P)`, and the idempotent projection of `P`.
|