CategoryTheory.Preadditive.hasEqualizers_of_hasKernels
theorem CategoryTheory.Preadditive.hasEqualizers_of_hasKernels :
∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] [inst_1 : CategoryTheory.Preadditive C]
[inst_2 : CategoryTheory.Limits.HasKernels C], CategoryTheory.Limits.HasEqualizers C
The theorem `CategoryTheory.Preadditive.hasEqualizers_of_hasKernels` states that for any type `C`, given that `C` forms a category and is preadditive, and assuming that this category `C` has all kernels (which are a sort of limit in category theory), then this category `C` also has all equalizers. In the language of category theory, an equalizer is another specific type of limit, so this theorem connects the existence of two types of limits in a preadditive category.
More concisely: In a preadditive category with all kernels, equalizers exist.
|
CategoryTheory.Preadditive.sum_comp
theorem CategoryTheory.Preadditive.sum_comp :
∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] [inst_1 : CategoryTheory.Preadditive C] {P Q R : C}
{J : Type u_1} (s : Finset J) (f : J → (P ⟶ Q)) (g : Q ⟶ R),
CategoryTheory.CategoryStruct.comp (s.sum fun j => f j) g =
s.sum fun j => CategoryTheory.CategoryStruct.comp (f j) g
This theorem, named `CategoryTheory.Preadditive.sum_comp`, is related to the theory of categories and preadditive categories. Specifically, it states that for any category `C` that is also preadditive, given three objects `P`, `Q`, and `R` in `C`, a finite set `s` of type `J`, a function `f` mapping each element of `s` to a morphism from `P` to `Q`, and a morphism `g` from `Q` to `R`, the composition of the sum of the morphisms `f j` (where `j` ranges over all elements of `s`) with `g` is equal to the sum (taken over all `j` in `s`) of the compositions of `f j` with `g`. In other words, the sum of compositions is the same as the composition of sums in this context. This is an application of the distributivity property in preadditive categories.
More concisely: For any preadditive category `C`, given objects `P`, `Q`, `R`, a set `s`, a function `f : s -> Hom(P, Q)`, and a morphism `g : Hom(Q, R)`, the sum of `f j` over `j` in `s` and `g` is equal to the sum of `g ∘ f j` over `j` in `s`.
|
CategoryTheory.Preadditive.epi_of_cokernel_zero
theorem CategoryTheory.Preadditive.epi_of_cokernel_zero :
∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] [inst_1 : CategoryTheory.Preadditive C] {X Y : C}
{f : X ⟶ Y} [inst_2 : CategoryTheory.Limits.HasColimit (CategoryTheory.Limits.parallelPair f 0)],
CategoryTheory.Limits.cokernel.π f = 0 → CategoryTheory.Epi f
This theorem states that for any Category `C` that is preadditive (i.e., has binary products and coproducts, and for which the hom sets between objects form an abelian group), if `f` is a morphism from an object `X` to an object `Y` in `C`, and if `C` has a colimit for the parallel pair `f` and the zero morphism, then if the morphism from `Y` to the cokernel of `f` is the zero morphism, it follows that `f` is an epimorphism (i.e., a right cancellable morphism). In other words, if the cokernel of `f` is trivial, then `f` must be an epimorphism.
More concisely: In a preadditive category with binary products, coproducts, and abelian hom sets, if a morphism has a trivial cokernel and the category has a colimit for the parallel pair of the morphism and the zero morphism, then the morphism is an epimorphism.
|
CategoryTheory.Preadditive.comp_zsmul
theorem CategoryTheory.Preadditive.comp_zsmul :
∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] [inst_1 : CategoryTheory.Preadditive C] {P Q R : C}
(f : P ⟶ Q) (g : Q ⟶ R) (n : ℤ),
CategoryTheory.CategoryStruct.comp f (n • g) = n • CategoryTheory.CategoryStruct.comp f g
This theorem, `CategoryTheory.Preadditive.comp_zsmul`, states that for any category `C` that is preadditive (meaning it has a binary operation compatible with the category structure), given three objects `P`, `Q`, and `R` in `C` and two morphisms `f : P ⟶ Q` and `g : Q ⟶ R`, and an integer `n`, the composition of `f` with the `n`-fold scalar multiplication of `g` is the same as the `n`-fold scalar multiplication of the composition of `f` and `g`. In simpler terms, it says that scalar multiplication commutes with morphism composition in a preadditive category.
More concisely: In a preadditive category, for any object $P, Q, R$ and morphisms $f: P \to Q$ and $g: Q \to R$, the scalar multiplication of $g$ by an integer $n$ and the composition of $f$ and $g$ are equal to the composition of $f$ and the scalar multiplication of $g$ by $n$.
|
CategoryTheory.Preadditive.comp_sub
theorem CategoryTheory.Preadditive.comp_sub :
∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] [inst_1 : CategoryTheory.Preadditive C] {P Q R : C}
(f : P ⟶ Q) (g g' : Q ⟶ R),
CategoryTheory.CategoryStruct.comp f (g - g') =
CategoryTheory.CategoryStruct.comp f g - CategoryTheory.CategoryStruct.comp f g'
The theorem `CategoryTheory.Preadditive.comp_sub` states that in any preadditive category `C`, for any three objects `P`, `Q`, and `R` in `C`, and for any morphisms `f : P ⟶ Q` and `g, g' : Q ⟶ R`, the composition of `f` with the difference of `g` and `g'` (denoted `g - g'`) is equivalent to the difference of the composition of `f` with `g` and the composition of `f` with `g'`. This property essentially shows the compatibility of the composition operation with the subtraction operation in a preadditive category.
More concisely: In any preadditive category, for all objects P, Q, R and morphisms f : P ⟶ Q, g, g' : Q ⟶ R, the composition of f with g - g' is equivalent to f * g - f * g'.
|
CategoryTheory.Preadditive.hasCoequalizer_of_hasCokernel
theorem CategoryTheory.Preadditive.hasCoequalizer_of_hasCokernel :
∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] [inst_1 : CategoryTheory.Preadditive C] {X Y : C}
(f g : X ⟶ Y) [inst_2 : CategoryTheory.Limits.HasCokernel (f - g)], CategoryTheory.Limits.HasCoequalizer f g
This theorem states that in a preadditive category, if there exists a cokernel for the morphism obtained by subtracting the morphism `g` from `f`, then a coequalizer for the morphisms `f` and `g` also exists. In other words, the existence of a cokernel for the difference of two morphisms implies the existence of a coequalizer for the original two morphisms in a preadditive category.
More concisely: In a preadditive category, if the difference of two morphisms has a cokernel, then the two morphisms have a coequalizer.
|
CategoryTheory.Preadditive.mono_of_isZero_kernel'
theorem CategoryTheory.Preadditive.mono_of_isZero_kernel' :
∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] [inst_1 : CategoryTheory.Preadditive C] {X Y : C}
{f : X ⟶ Y} (c : CategoryTheory.Limits.KernelFork f),
CategoryTheory.Limits.IsLimit c → CategoryTheory.Limits.IsZero c.pt → CategoryTheory.Mono f
The theorem `CategoryTheory.Preadditive.mono_of_isZero_kernel'` states that for any category `C` that is preadditive (which means it's a category equipped with a bifunctorial binary operation "+"), if we have morphism `f` from object `X` to object `Y` such that there exists a kernel fork `c` of `f` which is a limit (meaning it represents the "best" or "universal" solution to a particular diagram in the category) and the source `pt` of `c` is a zero object (which means it's both a terminal and initial object in the category), then the morphism `f` is a monomorphism. In a nutshell, a monomorphism in a preadditive category is determined by its kernel being a zero object.
More concisely: If in a preadditive category, a morphism has a kernel that is a limit with a zero object as source, then the morphism is a monomorphism.
|
CategoryTheory.Preadditive.comp_sum
theorem CategoryTheory.Preadditive.comp_sum :
∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] [inst_1 : CategoryTheory.Preadditive C] {P Q R : C}
{J : Type u_1} (s : Finset J) (f : P ⟶ Q) (g : J → (Q ⟶ R)),
CategoryTheory.CategoryStruct.comp f (s.sum fun j => g j) =
s.sum fun j => CategoryTheory.CategoryStruct.comp f (g j)
This theorem, `CategoryTheory.Preadditive.comp_sum`, is about composition and summation in the context of category theory. It states that for any category `C` which is preadditive (meaning it has a bifunctorial binary operation compatible with the category structure), and for any objects `P`, `Q`, `R` in `C`, any finite set `s`, a morphism `f` from `P` to `Q`, and a family of morphisms `g` from `Q` to `R` indexed by `s`, the composition of `f` with the sum of the `g`s (i.e., `f ≫ (∑ g)`) is equal to the sum of the compositions of `f` with each `g` (i.e., `∑ (f ≫ g)`). This expresses a kind of distributivity property for composition over summation in preadditive categories.
More concisely: In a preadditive category, for any object `P`, objects `Q`, `R`, morphism `f : P -> Q`, and family of morphisms `g_i : Q -> R` indexed by a finite set `s`, the commutativity of `f` with the sum of the `g_i` implies the equality of `f ≫ (∑ g_i)` and `∑ (f ≫ g_i)`.
|
CategoryTheory.Preadditive.comp_neg
theorem CategoryTheory.Preadditive.comp_neg :
∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] [inst_1 : CategoryTheory.Preadditive C] {P Q R : C}
(f : P ⟶ Q) (g : Q ⟶ R), CategoryTheory.CategoryStruct.comp f (-g) = -CategoryTheory.CategoryStruct.comp f g
The theorem `CategoryTheory.Preadditive.comp_neg` states that for any three objects `P`, `Q`, and `R` in a preadditive category `C`, and any two morphisms `f` from `P` to `Q`, and `g` from `Q` to `R`, the composition of `f` with the negation of `g` is equal to the negation of the composition of `f` and `g`. Here, a preadditive category is a category that has a zero object, and every hom-set has the structure of an abelian group. This theorem captures a key property of negative morphisms in preadditive categories.
More concisely: In a preadditive category, for any objects P, Q, and R, and morphisms f : P -> Q and g : Q -> R, the negation of (f \* g) is equal to g^(-1) \* f^(-1). (Here, \* denotes composition, and ^(-1) denotes the inverse in the abelian group structure of hom-sets.)
|
CategoryTheory.Preadditive.hasCokernel_of_hasCoequalizer
theorem CategoryTheory.Preadditive.hasCokernel_of_hasCoequalizer :
∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] [inst_1 : CategoryTheory.Preadditive C] {X Y : C}
(f g : X ⟶ Y) [inst_2 : CategoryTheory.Limits.HasCoequalizer f g], CategoryTheory.Limits.HasCokernel (f - g)
The theorem `CategoryTheory.Preadditive.hasCokernel_of_hasCoequalizer` states that in a preadditive category, if a pair of morphisms `f` and `g` from object `X` to object `Y` has a coequalizer, then the morphism resulting from the difference `f - g` has a cokernel. Here, a preadditive category is a category in which every hom-set has the structure of an abelian group. A coequalizer of two morphisms is an object that serves as the "best" way to map from the codomain of those morphisms in such a way that the two morphisms become equal when composed with this map. A cokernel of a morphism is a sort of "best" object that fits into a particular type of diagram involving that morphism.
More concisely: In a preadditive category, if morphisms `f` and `g` from object `X` to object `Y` have a coequalizer, then the morphism `f - g` has a cokernel.
|
CategoryTheory.Preadditive.hasCoequalizers_of_hasCokernels
theorem CategoryTheory.Preadditive.hasCoequalizers_of_hasCokernels :
∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] [inst_1 : CategoryTheory.Preadditive C]
[inst_2 : CategoryTheory.Limits.HasCokernels C], CategoryTheory.Limits.HasCoequalizers C
This theorem states that in the context of category theory, if a preadditive category (a category that has a binary operation that is compatible with the composition of morphisms) has all cokernels (the categorical dual of kernels), then it also has all coequalizers. Coequalizers are a specific kind of colimit in a category, and can be intuitively understood as a way to "balance" or "equalize" a pair of morphisms.
More concisely: In a preadditive category with all cokernels, every pair of morphisms has a coequalizer.
|
CategoryTheory.Preadditive.comp_nsmul
theorem CategoryTheory.Preadditive.comp_nsmul :
∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] [inst_1 : CategoryTheory.Preadditive C] {P Q R : C}
(f : P ⟶ Q) (g : Q ⟶ R) (n : ℕ),
CategoryTheory.CategoryStruct.comp f (n • g) = n • CategoryTheory.CategoryStruct.comp f g
The theorem `CategoryTheory.Preadditive.comp_nsmul` states that for any preadditive category `C` and any three objects `P`, `Q`, and `R` in `C`, given a morphism `f` from `P` to `Q` and a morphism `g` from `Q` to `R`, and an integer `n`, the composition of `f` and `n` times `g` (denoted by `CategoryTheory.CategoryStruct.comp f (n • g)`) is equal to `n` times the composition of `f` and `g` (denoted by `n • CategoryTheory.CategoryStruct.comp f g`). Here, composition of morphisms is defined as per the structure of the category and `n • g` denotes scalar multiplication of the morphism `g` by `n` as per the preadditive structure on `C`.
More concisely: For any preadditive category `C`, for all objects `P`, `Q`, `R`, morphisms `f: P -> Q`, `g: Q -> R`, and integers `n`, the scalar multiplication of the composition `n • (f ∘ g)` is equal to the composition of scalar multiplications `n • f ∘ g`.
|
CategoryTheory.Preadditive.sub_comp
theorem CategoryTheory.Preadditive.sub_comp :
∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] [inst_1 : CategoryTheory.Preadditive C] {P Q R : C}
(f f' : P ⟶ Q) (g : Q ⟶ R),
CategoryTheory.CategoryStruct.comp (f - f') g =
CategoryTheory.CategoryStruct.comp f g - CategoryTheory.CategoryStruct.comp f' g
The theorem `CategoryTheory.Preadditive.sub_comp` states that for any category `C` that is also a preadditive category, and any three objects `P`, `Q`, `R` in `C`, with morphisms `f`, `f'` from `P` to `Q` and a morphism `g` from `Q` to `R`, the composition of the difference of the morphisms `f` and `f'` with `g` is equal to the difference of the compositions of `f` and `g`, and `f'` and `g` respectively. In mathematical terms, for all `(f-f')` and `g`, `(f - f') ≫ g = f ≫ g - f' ≫ g`, where `≫` denotes the composition of morphisms. This theorem essentially states the distributive property of composition over subtraction in the context of preadditive categories.
More concisely: In a preadditive category, for morphisms `f, f', g`, the composition `(f - f') ≫ g` equals `f ≫ g - f' ≫ g`.
|
CategoryTheory.Preadditive.nsmul_comp
theorem CategoryTheory.Preadditive.nsmul_comp :
∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] [inst_1 : CategoryTheory.Preadditive C] {P Q R : C}
(f : P ⟶ Q) (g : Q ⟶ R) (n : ℕ),
CategoryTheory.CategoryStruct.comp (n • f) g = n • CategoryTheory.CategoryStruct.comp f g
The theorem `CategoryTheory.Preadditive.nsmul_comp` states that for any category `C` that is preadditive (meaning it's enriched over the category of Abelian groups), for all objects `P`, `Q`, and `R` in `C`, and for all morphisms `f` from `P` to `Q` and `g` from `Q` to `R`, and for any natural number `n`, the composition of the `n`-fold scalar multiple of `f` with `g` is equal to the `n`-fold scalar multiple of the composition of `f` and `g`. In mathematical terms, this is the statement that `(n • f) ≫ g = n • (f ≫ g)`.
More concisely: For any preadditive category C and objects P, Q, R with morphisms f: P → Q and g: Q → R, and natural number n, the scalar multiplication of the composition of f and g by n is equal to the composition of the scalar multiplication of f by n and g. That is, (n • f) ≫ g = n • (f ≫ g).
|
CategoryTheory.Preadditive.hasEqualizer_of_hasKernel
theorem CategoryTheory.Preadditive.hasEqualizer_of_hasKernel :
∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] [inst_1 : CategoryTheory.Preadditive C] {X Y : C}
(f g : X ⟶ Y) [inst_2 : CategoryTheory.Limits.HasKernel (f - g)], CategoryTheory.Limits.HasEqualizer f g
The theorem `CategoryTheory.Preadditive.hasEqualizer_of_hasKernel` states that for any preadditive category `C` with objects `X` and `Y` and morphisms `f` and `g` from `X` to `Y`, if the category has a kernel for the morphism `f - g`, then it also has an equalizer for the morphisms `f` and `g`. Here, a preadditive category is a category in which every hom-set has the structure of an abelian group and composition of morphisms is bilinear, a kernel is a limit of a parallel pair consisting of a given morphism and a zero morphism, and an equalizer is a limit of a parallel pair of two given morphisms.
More concisely: If a preadditive category has a kernel for the difference of two morphisms, then it has an equalizer for those morphisms.
|
CategoryTheory.Preadditive.epi_of_cancel_zero
theorem CategoryTheory.Preadditive.epi_of_cancel_zero :
∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] [inst_1 : CategoryTheory.Preadditive C] {P Q : C}
(f : P ⟶ Q), (∀ {R : C} (g : Q ⟶ R), CategoryTheory.CategoryStruct.comp f g = 0 → g = 0) → CategoryTheory.Epi f
The theorem `CategoryTheory.Preadditive.epi_of_cancel_zero` states that: for any Category `C` that is preadditive (i.e., for which the collection of all morphisms has a structure of an abelian group, and composition of morphisms is bilinear), and for any objects `P` and `Q` in `C` with a morphism `f` from `P` to `Q`, if for all objects `R` in `C`, any morphism `g` from `Q` to `R` that makes the composition `f ≫ g` equal to zero implies `g` is zero, then `f` is an epimorphism. In other words, in a preadditive category, if the composition of a morphism `f` with any other morphism `g` is zero only when `g` is the zero morphism, then `f` is an epimorphism.
More concisely: In a preadditive category, a morphism is an epimorphism if and only if the composition of the morphism with any zero morphism results in the zero morphism.
|
CategoryTheory.Preadditive.add_comp
theorem CategoryTheory.Preadditive.add_comp :
∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] [self : CategoryTheory.Preadditive C] (P Q R : C)
(f f' : P ⟶ Q) (g : Q ⟶ R),
CategoryTheory.CategoryStruct.comp (f + f') g =
CategoryTheory.CategoryStruct.comp f g + CategoryTheory.CategoryStruct.comp f' g
The theorem `CategoryTheory.Preadditive.add_comp` states that for any category `C` which is preadditive (a property that means the set of all morphisms from an object `P` to an object `Q` forms an abelian group and the composition of morphisms is linear in both arguments), given three objects `P`, `Q`, `R` in `C`, two morphisms `f` and `f'` from `P` to `Q`, and a morphism `g` from `Q` to `R`, the composition of the sum of `f` and `f'` with `g` (denoted `(f + f') ≫ g`) is equal to the sum of the composition of `f` with `g` and the composition of `f'` with `g` (denoted `f ≫ g + f' ≫ g`). This theorem basically asserts the distributive property of morphism composition over addition in a preadditive category.
More concisely: In a preadditive category, the composition of a morphism with the sum of two other morphisms is equal to the sum of their compositions with that morphism.
|
CategoryTheory.Preadditive.mono_of_cancel_zero
theorem CategoryTheory.Preadditive.mono_of_cancel_zero :
∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] [inst_1 : CategoryTheory.Preadditive C] {Q R : C}
(f : Q ⟶ R),
(∀ {P : C} (g : P ⟶ Q), CategoryTheory.CategoryStruct.comp g f = 0 → g = 0) → CategoryTheory.Mono f
The theorem `CategoryTheory.Preadditive.mono_of_cancel_zero` states that for any category `C` with preadditive structure (i.e., such that the hom-sets have an abelian group structure compatible with composition), given any two objects `Q` and `R` in `C` and a morphism `f` from `Q` to `R`, if for every object `P` in `C` and morphism `g` from `P` to `Q`, the composition `g ≫ f` being zero implies that `g` is zero, then `f` is a monomorphism. This theorem is about the cancellation property of morphisms in preadditive categories.
More concisely: In a preadditive category, if every morphism with zero composition with a given morphism is the zero morphism, then the given morphism is a monomorphism.
|
CategoryTheory.Preadditive.hasKernel_of_hasEqualizer
theorem CategoryTheory.Preadditive.hasKernel_of_hasEqualizer :
∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] [inst_1 : CategoryTheory.Preadditive C] {X Y : C}
(f g : X ⟶ Y) [inst_2 : CategoryTheory.Limits.HasEqualizer f g], CategoryTheory.Limits.HasKernel (f - g)
The theorem `CategoryTheory.Preadditive.hasKernel_of_hasEqualizer` states that for any preadditive category `C` with objects `X` and `Y`, and morphisms `f` and `g` from `X` to `Y`, if the category has an equalizer for `f` and `g`, then it also has a kernel for the morphism `f - g`. Here, an equalizer for `f` and `g` is a specific choice of limiting cone for the parallel pair of morphisms `f` and `g`, and a kernel for a morphism `f` is a limit of the functor `ParallelPair f 0`. The preadditive category provides the context for the subtraction operation used in `f - g`.
More concisely: If preadditive category `C` has an equalizer for morphisms `f` and `g` from object `X` to `Y`, then `f - g` has a kernel, which is the equalizer of `f` and `g`.
|
CategoryTheory.Preadditive.mono_of_kernel_zero
theorem CategoryTheory.Preadditive.mono_of_kernel_zero :
∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] [inst_1 : CategoryTheory.Preadditive C] {X Y : C}
{f : X ⟶ Y} [inst_2 : CategoryTheory.Limits.HasLimit (CategoryTheory.Limits.parallelPair f 0)],
CategoryTheory.Limits.kernel.ι f = 0 → CategoryTheory.Mono f
This theorem, `CategoryTheory.Preadditive.mono_of_kernel_zero`, states that in any category `C` of type `u`, where `C` is equipped with both a category structure and a preadditive structure, for any objects `X` and `Y` in `C` and any morphism `f` from `X` to `Y`, if `C` has a limit of the parallel pair `f` and `0`, and if the kernel of `f` is `0`, then `f` is a monomorphism.
In terms of category theory, this is asserting that if the kernel of a morphism in a preadditive category is zero, then that morphism is a monomorphism, which is a generalization of a property from the category of abelian groups.
More concisely: In a preadditive category, if the kernel of a morphism is the zero object, then the morphism is a monomorphism.
|
CategoryTheory.Preadditive.comp_add
theorem CategoryTheory.Preadditive.comp_add :
∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] [self : CategoryTheory.Preadditive C] (P Q R : C)
(f : P ⟶ Q) (g g' : Q ⟶ R),
CategoryTheory.CategoryStruct.comp f (g + g') =
CategoryTheory.CategoryStruct.comp f g + CategoryTheory.CategoryStruct.comp f g'
The theorem `CategoryTheory.Preadditive.comp_add` states that for any category that is preadditive, which means that the hom-set `P ⟶ Q` forms an abelian group and composition of morphisms is bilinear, given three objects `P`, `Q`, and `R` in the category, and two morphisms `g` and `g'` from `Q` to `R`, the composition of a morphism `f` from `P` to `Q` with the sum of `g` and `g'` is equal to the sum of the composition of `f` with `g` and the composition of `f` with `g'`. This is essentially asserting the property of distributivity of composition over addition in the context of preadditive categories.
More concisely: For any preadditive category, the composition of a morphism with the sum of two other morphisms is equal to the sum of their compositions.
|
CategoryTheory.Preadditive.zsmul_comp
theorem CategoryTheory.Preadditive.zsmul_comp :
∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] [inst_1 : CategoryTheory.Preadditive C] {P Q R : C}
(f : P ⟶ Q) (g : Q ⟶ R) (n : ℤ),
CategoryTheory.CategoryStruct.comp (n • f) g = n • CategoryTheory.CategoryStruct.comp f g
The theorem `CategoryTheory.Preadditive.zsmul_comp` states that for any three objects `P`, `Q`, and `R` in a preadditive category `C`, and for any two morphisms `f` from `P` to `Q` and `g` from `Q` to `R`, and for any integer `n`, the composition of `n` times the morphism `f` with the morphism `g` is equal to `n` times the composition of the morphisms `f` and `g`. In mathematical terms, it states that `(n • f) ≫ g = n • (f ≫ g)`, where `≫` represents composition of morphisms, and `•` represents scaling by an integer.
More concisely: For any integer `n` and morphisms `f` and `g` in a preadditive category, `n * (f ∘ g) = (n * f) ∘ g`.
|
CategoryTheory.Preadditive.neg_comp
theorem CategoryTheory.Preadditive.neg_comp :
∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] [inst_1 : CategoryTheory.Preadditive C] {P Q R : C}
(f : P ⟶ Q) (g : Q ⟶ R), CategoryTheory.CategoryStruct.comp (-f) g = -CategoryTheory.CategoryStruct.comp f g
The theorem `CategoryTheory.Preadditive.neg_comp` states that in any preadditive category `C`, for any three objects `P`, `Q`, and `R` in `C`, and for any two morphisms `f` from `P` to `Q` and `g` from `Q` to `R`, the composition of the negation of `f` and `g` is equal to the negation of the composition of `f` and `g`. In mathematical expressions, this can be written as `(-f) ⋅ g = -(f ⋅ g)`. A preadditive category is a category where every homset is an abelian group and the composition of morphisms distributes over the group operation.
More concisely: In a preadditive category, the negation of the composition of two morphisms is equal to the composition of their negations.
|