CategoryTheory.Functor.preservesZeroMorphisms_of_map_zero_object
theorem CategoryTheory.Functor.preservesZeroMorphisms_of_map_zero_object :
∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂}
[inst_1 : CategoryTheory.Category.{v₂, u₂} D] [inst_2 : CategoryTheory.Limits.HasZeroObject C]
[inst_3 : CategoryTheory.Limits.HasZeroObject D] [inst_4 : CategoryTheory.Limits.HasZeroMorphisms C]
[inst_5 : CategoryTheory.Limits.HasZeroMorphisms D] {F : CategoryTheory.Functor C D},
(F.obj 0 ≅ 0) → F.PreservesZeroMorphisms
This theorem states that for any two categories `C` and `D` such that they both have zero objects and zero morphisms, if we have a functor `F` from `C` to `D` that maps the zero object in `C` to the zero object in `D` (denoted as `F.obj 0 ≅ 0`), then this functor `F` preserves zero morphisms. In other words, applying the functor `F` to a zero morphism in `C` results in a zero morphism in `D`.
More concisely: Given any functors F from category C to D with zero objects and zero morphisms, if F maps the zero object of C to the zero object of D and preserves the identity morphism of the zero object, then F preserves zero morphisms.
|
CategoryTheory.Functor.map_zero
theorem CategoryTheory.Functor.map_zero :
∀ {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)
[inst_4 : F.PreservesZeroMorphisms] (X Y : C), F.map 0 = 0
This theorem states that for any category `C` and category `D` which both have zero morphisms, and any functor `F` from `C` to `D` that preserves zero morphisms, the image of the zero morphism under `F` is the zero morphism in `D`. In simpler terms, applying the functor `F` to the zero morphism in `C` gives the zero morphism in `D`.
More concisely: For any functor F between categories with zero morphisms, if F preserves zero morphisms then F(0) = 0, where 0 denotes the zero morphism in the respective categories.
|
CategoryTheory.Functor.PreservesZeroMorphisms.map_zero
theorem CategoryTheory.Functor.PreservesZeroMorphisms.map_zero :
∀ {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}
[self : F.PreservesZeroMorphisms] (X Y : C), F.map 0 = 0
This theorem states that for any pair of objects `X` and `Y` in category `C`, if a Functor `F` preserves zero morphisms and the categories `C` and `D` have zero morphisms, the image of the zero morphism from `X` to `Y` under `F` is the zero morphism in `D`. To put it another way, mapping the zero morphism of `C` via the functor `F` results in the zero morphism of `D`. This affirms the fact that certain properties, in this case, zero-morphisms, are preserved under a functor.
More concisely: Given any functor `F` that preserves zero morphisms between categories `C` and `D` with zero morphisms, the image of the zero morphism from object `X` in `C` to object `Y` in `C` under `F` is the zero morphism from `F(X)` to `F(Y)` in `D`.
|