CategoryTheory.Functor.map_nsmul
theorem CategoryTheory.Functor.map_nsmul :
∀ {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] [inst_2 : CategoryTheory.Preadditive C]
[inst_3 : CategoryTheory.Preadditive D] (F : CategoryTheory.Functor C D) [inst_4 : F.Additive] {X Y : C}
{f : X ⟶ Y} {n : ℕ}, F.map (n • f) = n • F.map f
The theorem `CategoryTheory.Functor.map_nsmul` states that for any types `C` and `D`, given a category structure on these types, a preadditive structure (i.e., an Abelian group structure on each hom-set) on these categories, a functor `F` from `C` to `D`, and an additive structure on the functor `F`, then the functor maps the `n`-fold scalar multiplication of a morphism `f` from `X` to `Y` in `C` to the `n`-fold scalar multiplication of the mapped morphism `F.map f` in `D`. In other words, if we consider `n • f` as adding `f` to itself `n` times, then applying the functor `F` and then adding `F.map f` to itself `n` times yields the same result as first adding `f` to itself `n` times and then applying `F`.
More concisely: For any functors F between preadditive categories C and D endowed with additive structures, if F respects the Abelian group structure on hom-sets and scalar multiplication by natural numbers, then F maps the n-fold scalar multiplication of a morphism to the n-fold scalar multiplication of its image under F.
|
CategoryTheory.Functor.map_add
theorem CategoryTheory.Functor.map_add :
∀ {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] [inst_2 : CategoryTheory.Preadditive C]
[inst_3 : CategoryTheory.Preadditive D] (F : CategoryTheory.Functor C D) [inst_4 : F.Additive] {X Y : C}
{f g : X ⟶ Y}, F.map (f + g) = F.map f + F.map g
This theorem states that for any two morphisms `f` and `g` from object `X` to object `Y` in a preadditive category `C`, and a functor `F` from `C` to another preadditive category `D` that preserves binary addition of morphisms, the functor `F` applied to the sum of `f` and `g` (`F.map (f + g)`) is equal to the sum of `F` applied to `f` and `F` applied to `g` (`F.map f + F.map g`). In other words, it demonstrates the distributive property of an additive functor over morphism addition in preadditive categories.
More concisely: For any additive functor F between preadditive categories and any morphisms f, g in a preadditive category, F(f + g) = F(f) + F(g).
|
CategoryTheory.Functor.map_neg
theorem CategoryTheory.Functor.map_neg :
∀ {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] [inst_2 : CategoryTheory.Preadditive C]
[inst_3 : CategoryTheory.Preadditive D] (F : CategoryTheory.Functor C D) [inst_4 : F.Additive] {X Y : C}
{f : X ⟶ Y}, F.map (-f) = -F.map f
This theorem states that for any types `C` and `D` that have category structures and are preadditive (i.e., have an addition operation), if there is an additive functor `F` from `C` to `D`, then for any two objects `X` and `Y` in `C` and a morphism `f` from `X` to `Y`, the functor `F` applied to the negation of `f` is equal to the negation of the functor `F` applied to `f`. This theorem essentially says that the functor `F` preserves the negation operation on morphisms.
More concisely: Given additive categories `C` and `D`, and an additive functor `F` from `C` to `D`, for any objects `X`, `Y` in `C` and morphism `f : X → Y`, we have `F(−f) = −F(f)`.
|
CategoryTheory.Functor.additive_of_preservesBinaryBiproducts
theorem CategoryTheory.Functor.additive_of_preservesBinaryBiproducts :
∀ {C : Type u₁} {D : Type u₂} [inst : CategoryTheory.Category.{v₁, u₁} C]
[inst_1 : CategoryTheory.Category.{v₂, u₂} D] [inst_2 : CategoryTheory.Preadditive C]
[inst_3 : CategoryTheory.Preadditive D] (F : CategoryTheory.Functor C D)
[inst_4 : CategoryTheory.Limits.HasBinaryBiproducts C] [inst_5 : F.PreservesZeroMorphisms]
[inst_6 : CategoryTheory.Limits.PreservesBinaryBiproducts F], F.Additive
This theorem states that for any two types `C` and `D` along with their categorical structures, where `C` is preadditive and has binary biproducts and `D` is preadditive, if a functor `F` from `C` to `D` preserves zero morphisms and binary biproducts, then `F` is additive.
In mathematical terms, this theorem is about the properties of functors between categories in category theory. It states that if we have a functor between two categories that preserves certain structures (zero morphisms and binary biproducts), then that functor has an additional property: it is additive. This is a significant property in category theory because additive functors preserve the additive structure of the categories they map between, allowing for the transfer of more structural information between categories.
More concisely: Given preadditive categories `C` and `D` with binary biproducts, if functor `F` from `C` to `D` preserves zero morphisms and binary biproducts, then `F` is additive.
|
CategoryTheory.Functor.map_zsmul
theorem CategoryTheory.Functor.map_zsmul :
∀ {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] [inst_2 : CategoryTheory.Preadditive C]
[inst_3 : CategoryTheory.Preadditive D] (F : CategoryTheory.Functor C D) [inst_4 : F.Additive] {X Y : C}
{f : X ⟶ Y} {r : ℤ}, F.map (r • f) = r • F.map f
This theorem states that for all categories `C` and `D`, if `C` and `D` are preadditive categories and `F` is an additive functor from `C` to `D`, then for all objects `X` and `Y` in `C` and a morphism `f` from `X` to `Y`, and an integer `r`, the functor `F` applied to the morphism `r` times `f` equals `r` times the functor `F` applied to `f`. This is a property that shows the interplay between functors and scalars in additive categories.
More concisely: For all preadditive categories `C` and `D`, and additive functor `F` from `C` to `D`, given objects `X` and `Y` in `C`, and a morphism `f` from `X` to `Y`, the functor `F` commutes with scalar multiplication, i.e., `F(rf) = r(F(f))`.
|
CategoryTheory.Functor.map_sub
theorem CategoryTheory.Functor.map_sub :
∀ {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] [inst_2 : CategoryTheory.Preadditive C]
[inst_3 : CategoryTheory.Preadditive D] (F : CategoryTheory.Functor C D) [inst_4 : F.Additive] {X Y : C}
{f g : X ⟶ Y}, F.map (f - g) = F.map f - F.map g
This theorem states that for any two morphisms `f` and `g` from `X` to `Y` in a preadditive category `C`, and any additive functor `F` from `C` to another preadditive category `D`, the functor `F` preserves the subtraction of morphisms. That is, applying `F` to the subtraction of `f` and `g` (`f - g`) gives the same result as subtracting the images of `f` and `g` under `F` (`F.map f - F.map g`).
More concisely: For any preadditive functor F between preadditive categories, and morphisms f, g in C, F(f - g) = F(f) - F(g).
|
CategoryTheory.Functor.map_sum
theorem CategoryTheory.Functor.map_sum :
∀ {C : Type u_1} {D : Type u_2} [inst : CategoryTheory.Category.{u_5, u_1} C]
[inst_1 : CategoryTheory.Category.{u_6, u_2} D] [inst_2 : CategoryTheory.Preadditive C]
[inst_3 : CategoryTheory.Preadditive D] (F : CategoryTheory.Functor C D) [inst_4 : F.Additive] {X Y : C}
{α : Type u_4} (f : α → (X ⟶ Y)) (s : Finset α), F.map (s.sum fun a => f a) = s.sum fun a => F.map (f a)
This theorem is stating a property about functors in category theory. Specifically, it's saying that for any category `C` and `D`, both of which are `Preadditive`, and an `Additive` functor `F` from `C` to `D`, the map of the sum of morphisms from `X` to `Y` in `C` (indexed by a finite set `s`), through the functor `F`, is the same as the sum of the individual maps of each morphism through `F`. In other words, for any elements `X` and `Y` of `C`, any function `f` from a type `α` to morphisms from `X` to `Y`, and any finite set `s` of type `α`, the functor `F` distributes over the sum of morphisms, i.e., `F.map (Finset.sum s f) = Finset.sum s (F.map ∘ f)`. This is a type of distributivity property for functors with respect to the operation of summing over morphisms in a category.
More concisely: For any additive categories `C` and `D`, and additive functor `F` from `C` to `D`, the sum of morphisms from `X` to `Y` in `C`, through `F`, equals the sum of the individual morphisms through `F`, for any objects `X` and `Y` in `C`.
|
CategoryTheory.Functor.Additive.map_add
theorem CategoryTheory.Functor.Additive.map_add :
∀ {C : Type u_1} {D : Type u_2} [inst : CategoryTheory.Category.{u_3, u_1} C]
[inst_1 : CategoryTheory.Category.{u_4, u_2} D] [inst_2 : CategoryTheory.Preadditive C]
[inst_3 : CategoryTheory.Preadditive D] {F : CategoryTheory.Functor C D} [self : F.Additive] {X Y : C}
{f g : X ⟶ Y}, F.map (f + g) = F.map f + F.map g
This theorem states that, for any two objects `X` and `Y` in a preadditive category `C`, and for any two morphisms `f` and `g` from `X` to `Y` in `C`, if `C` is mapped to another preadditive category `D` via an additive functor `F`, the image of the sum of `f` and `g` under `F` is equal to the sum of their individual images under `F`. In other words, the functor `F` preserves the addition operation on morphisms.
More concisely: Given any additive functor F from a preadditive category C to another preadditive category D, for all objects X and Y in C and morphisms f, g : X -> Y, F(f + g) = F(f) + F(g).
|