CategoryTheory.Functor.biproductComparison'_comp_biproductComparison
theorem CategoryTheory.Functor.biproductComparison'_comp_biproductComparison :
∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂}
[inst_1 : CategoryTheory.Category.{v₂, u₂} D] [inst_2 : CategoryTheory.Limits.HasZeroMorphisms C]
[inst_3 : CategoryTheory.Limits.HasZeroMorphisms D] {J : Type w₁} (F : CategoryTheory.Functor C D) (f : J → C)
[inst_4 : CategoryTheory.Limits.HasBiproduct f] [inst_5 : CategoryTheory.Limits.HasBiproduct (F.obj ∘ f)]
[inst_6 : F.PreservesZeroMorphisms],
CategoryTheory.CategoryStruct.comp (F.biproductComparison' f) (F.biproductComparison f) =
CategoryTheory.CategoryStruct.id (⨁ F.obj ∘ f)
This theorem states that for any categories `C` and `D` with zero morphisms, a functor `F` from `C` to `D`, and a function `f` from some type `J` to `C` where `C` has a biproduct of `f` and `D` has a biproduct of `F.obj ∘ f`, the composition of `F.biproductComparison' f` and `F.biproductComparison f` is equal to the identity on the biproduct of `F.obj ∘ f` if and only if `F` preserves the biproduct. This is essentially a round-trip property in the context of category theory, asserting that the functor `F` preserves the structure of the biproducts in `C` when mapped to `D`.
More concisely: For functors F from category C to category D with zero morphisms, F preserves the biproduct structure if and only if the composition of F.biproductComparison' at a function f from J to C and F.biproductComparison at f is equal to the identity on the biproduct of F.obj ∘ f.
|
CategoryTheory.Functor.biprodComparison'_comp_biprodComparison
theorem CategoryTheory.Functor.biprodComparison'_comp_biprodComparison :
∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂}
[inst_1 : CategoryTheory.Category.{v₂, u₂} D] [inst_2 : CategoryTheory.Limits.HasZeroMorphisms C]
[inst_3 : CategoryTheory.Limits.HasZeroMorphisms D] (F : CategoryTheory.Functor C D) (X Y : C)
[inst_4 : CategoryTheory.Limits.HasBinaryBiproduct X Y]
[inst_5 : CategoryTheory.Limits.HasBinaryBiproduct (F.obj X) (F.obj Y)] [inst_6 : F.PreservesZeroMorphisms],
CategoryTheory.CategoryStruct.comp (F.biprodComparison' X Y) (F.biprodComparison X Y) =
CategoryTheory.CategoryStruct.id (F.obj X ⊞ F.obj Y)
This theorem states that for any categories `C` and `D` with zero morphisms, and any functor `F` from `C` to `D` that preserves zero morphisms, given two objects `X` and `Y` in `C` that form a binary biproduct and whose images under `F` also form a binary biproduct in `D`, the composition of `F`'s biproduct comparison morphisms `F.biprodComparison' X Y` and `F.biprodComparison X Y` is equal to the identity morphism on the biproduct of `F.obj X` and `F.obj Y` in `D`. In layman's terms, if you first apply `F.biprodComparison' X Y` and then apply `F.biprodComparison X Y`, it is the same as doing nothing to the biproduct of `F.obj X` and `F.obj Y`. This is true if and only if the functor `F` preserves the biproduct structure, as described in `preservesBinaryBiproduct_of_monoBiprodComparison`.
More concisely: Given functors F from category C to D with zero morphisms, if F preserves binary biproducts and X and Y are objects in C forming a binary biproduct with biproduct comparison morphisms φ and ψ respectively, then F(φ) * F(ψ) = id(F(X) ⊕ F(Y)).
|