CategoryTheory.NonPreadditiveAbelian.sub_zero
theorem CategoryTheory.NonPreadditiveAbelian.sub_zero :
∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] [inst_1 : CategoryTheory.NonPreadditiveAbelian C] {X Y : C}
(a : X ⟶ Y), a - 0 = a
This theorem states that in the context of a non-preadditive Abelian category (denoted by `C`), for any two objects `X` and `Y` in `C`, and any morphism `a` from `X` to `Y`, subtracting the zero morphism from `a` gives `a` again. In other words, in a non-preadditive Abelian category, any morphism minus the zero morphism equals the original morphism.
More concisely: In a non-preadditive Abelian category, for any morphism `a` from object `X` to object `Y`, `a = a + (-a)` holds.
|
CategoryTheory.NonPreadditiveAbelian.sub_def
theorem CategoryTheory.NonPreadditiveAbelian.sub_def :
∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] [inst_1 : CategoryTheory.NonPreadditiveAbelian C] {X Y : C}
(a b : X ⟶ Y),
a - b =
CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.prod.lift a b)
CategoryTheory.NonPreadditiveAbelian.σ
The theorem `CategoryTheory.NonPreadditiveAbelian.sub_def` states that in a non-preadditive Abelian category `C`, for any two morphisms `a` and `b` from object `X` to object `Y`, the difference `a - b` can be defined as the composition of the morphism `prod.lift a b`, which is induced by `a` and `b`, and the morphism `σ` from the category's structure as a non-preadditive Abelian category. In other words, subtraction of morphisms in a non-preadditive Abelian category is defined via composition with the categorical product and a special morphism `σ`.
More concisely: In a non-preadditive Abelian category, morphism difference is defined as composition with the induced morphism from the categorical product and the special morphism `σ`.
|
CategoryTheory.NonPreadditiveAbelian.sub_self
theorem CategoryTheory.NonPreadditiveAbelian.sub_self :
∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] [inst_1 : CategoryTheory.NonPreadditiveAbelian C] {X Y : C}
(a : X ⟶ Y), a - a = 0
This theorem states that for any category `C` that is also a `NonPreadditiveAbelian` category, and for any two objects `X` and `Y` in `C`, if `a` is a morphism from `X` to `Y`, then subtracting `a` from itself results in the zero morphism. This is the analogue in category theory of the algebraic property that any number minus itself equals zero.
More concisely: For any object `X`, `Y` in a `NonPreadditiveAbelian` category `C` and morphism `a` from `X` to `Y`, `a` equals its negative, i.e., `a + (-a) = 0`.
|
CategoryTheory.NonPreadditiveAbelian.neg_def
theorem CategoryTheory.NonPreadditiveAbelian.neg_def :
∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] [inst_1 : CategoryTheory.NonPreadditiveAbelian C] {X Y : C}
(a : X ⟶ Y), -a = 0 - a
This theorem states that for any category `C` that is NonPreadditiveAbelian and for any objects `X` and `Y` in this category, the negation of a morphism `a` from `X` to `Y` is equivalent to subtracting `a` from zero. In other words, `-a` is equal to `0 - a` in the context of this particular category theory.
More concisely: In a NonPreadditiveAbelian category, the negation of a morphism is equivalent to subtracting the morphism from the identity morphism of the zero object.
|
CategoryTheory.NonPreadditiveAbelian.add_def
theorem CategoryTheory.NonPreadditiveAbelian.add_def :
∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] [inst_1 : CategoryTheory.NonPreadditiveAbelian C] {X Y : C}
(a b : X ⟶ Y), a + b = a - -b
This theorem states that in the context of a nonpreadditive Abelian category `C`, for any two morphisms `a` and `b` from object `X` to object `Y`, the sum of `a` and `b` is equal to the difference of `a` and the additive inverse of `b`. This is a mathematical theorem related to category theory, which deals with abstract structures in mathematics.
More concisely: In a nonpreadditive Abelian category, for any two morphisms `a` and `b` from object `X` to object `Y`, `a + b = a - (-b)`.
|
CategoryTheory.NonPreadditiveAbelian.sub_sub_sub
theorem CategoryTheory.NonPreadditiveAbelian.sub_sub_sub :
∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] [inst_1 : CategoryTheory.NonPreadditiveAbelian C] {X Y : C}
(a b c d : X ⟶ Y), a - c - (b - d) = a - b - (c - d)
This theorem states that in any category `C` of a certain type `u`, which has a structure of a NonPreadditiveAbelian category, given four morphisms `a`, `b`, `c`, and `d` from object `X` to object `Y`, the equality `a - c - (b - d) = a - b - (c - d)` holds. In mathematical terms, this corresponds to the property that subtraction of morphisms in a NonPreadditiveAbelian category is associative and satisfies the specific rearrangement of terms specified by the equation.
More concisely: In any NonPreadditive Abelian category, the subtraction of morphisms is associative: `a - c - (b - d) = a - b - (c - d)`.
|
CategoryTheory.NonPreadditiveAbelian.add_neg
theorem CategoryTheory.NonPreadditiveAbelian.add_neg :
∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] [inst_1 : CategoryTheory.NonPreadditiveAbelian C] {X Y : C}
(a b : X ⟶ Y), a + -b = a - b
This theorem is stated in the context of a category theory in Lean 4 and asserts that for any category `C` that is "non-preadditive abelian" and for any objects `X` and `Y` in `C`, the morphism `a` from `X` to `Y` added to the negation of morphism `b` from `X` to `Y` is equal to the morphism `a` subtracted by morphism `b`. In simpler terms, it establishes that adding a negated element is the same as subtraction in the context of morphisms in a non-preadditive abelian category.
More concisely: In a non-preadditive abelian category, for any objects X and Y and morphisms a and b, a + (-b) = a - b.
|
CategoryTheory.NonPreadditiveAbelian.σ_comp
theorem CategoryTheory.NonPreadditiveAbelian.σ_comp :
∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] [inst_1 : CategoryTheory.NonPreadditiveAbelian C] {X Y : C}
(f : X ⟶ Y),
CategoryTheory.CategoryStruct.comp CategoryTheory.NonPreadditiveAbelian.σ f =
CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.prod.map f f)
CategoryTheory.NonPreadditiveAbelian.σ
This theorem states that for any category `C` of Type `u`, which has the structure of a non-preadditive Abelian category, and for any objects `X` and `Y` in this category, the composition of the morphism `σ` (from the non-preadditive Abelian structure) with any morphism `f` from `X` to `Y` is equal to the composition of the morphism resulting from mapping `f` across the product with the morphism `σ`. This is a key identity satisfied by the morphism `σ` in a non-preadditive Abelian category. In other words, the theorem states that `σ` composed with `f` equals the composition of `(f,f)` mapped on the product with `σ`.
More concisely: In a non-preadditive Abelian category, for any object `X`, object `Y`, and morphism `f` from `X` to `Y`, the composition of `σ` with `f` equals the composition of `(f, f)` mapped on the product with `σ`.
|