CategoryTheory.Pretriangulated.TriangleMorphism.comm₁
theorem CategoryTheory.Pretriangulated.TriangleMorphism.comm₁ :
∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] [inst_1 : CategoryTheory.HasShift C ℤ]
{T₁ T₂ : CategoryTheory.Pretriangulated.Triangle C}
(self : CategoryTheory.Pretriangulated.TriangleMorphism T₁ T₂),
CategoryTheory.CategoryStruct.comp T₁.mor₁ self.hom₂ = CategoryTheory.CategoryStruct.comp self.hom₁ T₂.mor₁
The theorem `CategoryTheory.Pretriangulated.TriangleMorphism.comm₁` states the first commutative property of a triangle morphism in pretriangulated categories. For any pretriangulated categories `C` with a shift functor indexed by integers, and any two pretriangulated triangles `T₁` and `T₂` in `C`, if there exists a triangle morphism `self` from `T₁` to `T₂`, then the composition of the morphism `mor₁` of `T₁` followed by the homomorphism `hom₂` of `self` is equal to the composition of the homomorphism `hom₁` of `self` followed by the morphism `mor₁` of `T₂`. This is essentially saying that the diagram commutes for these specific morphisms within the triangles.
More concisely: In a pretriangulated category with shift functor, given two pretriangulated triangles and a triangle morphism between them, the diagram commuting for their corresponding morphisms holds.
|
CategoryTheory.Pretriangulated.comp_hom₂
theorem CategoryTheory.Pretriangulated.comp_hom₂ :
∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] [inst_1 : CategoryTheory.HasShift C ℤ]
{X Y Z : CategoryTheory.Pretriangulated.Triangle C} (f : X ⟶ Y) (g : Y ⟶ Z),
(CategoryTheory.CategoryStruct.comp f g).hom₂ = CategoryTheory.CategoryStruct.comp f.hom₂ g.hom₂
This theorem, `CategoryTheory.Pretriangulated.comp_hom₂`, says that for any category `C` with a shift and any three pretriangulated triangles `X`, `Y`, and `Z` in `C`, given morphisms `f` from `X` to `Y` and `g` from `Y` to `Z`, the `hom₂` component of the composition of `f` and `g` is equal to the composition of the `hom₂` components of `f` and `g`. In other words, within the context of pretriangulated categories, composition of morphisms preserves the `hom₂` component.
More concisely: For any pretriangulated category with a shift, the `hom₂` component of the composition of two morphisms between pretriangulated triangles is equal to the composition of their `hom₂` components.
|
CategoryTheory.Pretriangulated.comp_hom₃
theorem CategoryTheory.Pretriangulated.comp_hom₃ :
∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] [inst_1 : CategoryTheory.HasShift C ℤ]
{X Y Z : CategoryTheory.Pretriangulated.Triangle C} (f : X ⟶ Y) (g : Y ⟶ Z),
(CategoryTheory.CategoryStruct.comp f g).hom₃ = CategoryTheory.CategoryStruct.comp f.hom₃ g.hom₃
The theorem `CategoryTheory.Pretriangulated.comp_hom₃` states that for any type `C` that is a category with a shift, and any `X`, `Y`, and `Z` that are pretriangulated triangles in the category `C`, given morphisms `f` from `X` to `Y` and `g` from `Y` to `Z`, the third homomorphism of the composition of `f` and `g` is equal to the composition of the third homomorphisms of `f` and `g`. In other words, it guarantees the compatibility of the composition operation with the third homomorphism in the context of pretriangulated categories.
More concisely: For any pretriangulated categories `C` with a shift, and pretriangulated triangles `X → Y → Z` in `C`, the composition of third homomorphisms of morphisms `X → Y` and `Y → Z` equals the third homomorphism of their composition.
|
CategoryTheory.Pretriangulated.Triangle.hom_ext
theorem CategoryTheory.Pretriangulated.Triangle.hom_ext :
∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] [inst_1 : CategoryTheory.HasShift C ℤ]
{A B : CategoryTheory.Pretriangulated.Triangle C} (f g : A ⟶ B),
f.hom₁ = g.hom₁ → f.hom₂ = g.hom₂ → f.hom₃ = g.hom₃ → f = g
This theorem is about categories in mathematics and particularly about the pre-triangulated category. It states that for any given category `C` of type `u` (where `C` has a shifting operation defined on it), for any two pre-triangulated triangles `A` and `B` in `C`, and for any two morphisms `f` and `g` from `A` to `B`, if the first, second, and third morphisms of `f` and `g` are equal respectively, then `f` and `g` are the same. Basically, it establishes the uniqueness of a morphism in a pre-triangulated triangle, based on the equality of its constituent homomorphisms.
More concisely: In a pre-triangulated category `C`, if two morphisms between pre-triangulated triangles have equal constituent homomorphisms, then they are equal.
|
CategoryTheory.Pretriangulated.TriangleMorphism.comm₃
theorem CategoryTheory.Pretriangulated.TriangleMorphism.comm₃ :
∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] [inst_1 : CategoryTheory.HasShift C ℤ]
{T₁ T₂ : CategoryTheory.Pretriangulated.Triangle C}
(self : CategoryTheory.Pretriangulated.TriangleMorphism T₁ T₂),
CategoryTheory.CategoryStruct.comp T₁.mor₃ ((CategoryTheory.shiftFunctor C 1).map self.hom₁) =
CategoryTheory.CategoryStruct.comp self.hom₃ T₂.mor₃
This theorem, known as the third commutative square of a triangle morphism, states that for any category `C` with a shift functor to the integers, given two pretriangulated triangles `T₁` and `T₂` in `C` and a triangle morphism `self` from `T₁` to `T₂`, the composition of the third morphism of `T₁` and the shift of the first morphism of `self` is equal to the composition of the third morphism of `self` and the third morphism of `T₂`. This is essentially a condition ensuring that the triangles and the morphism between them maintain a certain commutative property, a fundamental concept in category theory.
More concisely: Given two pretriangulated triangles and a triangle morphism in a category with a shift functor, the composition of the third morphism of the first triangle and the shift of the first morphism of the morphism is equal to the composition of the third morphism of the morphism and the third morphism of the second triangle.
|
CategoryTheory.Pretriangulated.TriangleMorphism.ext
theorem CategoryTheory.Pretriangulated.TriangleMorphism.ext :
∀ {C : Type u} {inst : CategoryTheory.Category.{v, u} C} {inst_1 : CategoryTheory.HasShift C ℤ}
{T₁ T₂ : CategoryTheory.Pretriangulated.Triangle C} (x y : CategoryTheory.Pretriangulated.TriangleMorphism T₁ T₂),
x.hom₁ = y.hom₁ → x.hom₂ = y.hom₂ → x.hom₃ = y.hom₃ → x = y
The theorem `CategoryTheory.Pretriangulated.TriangleMorphism.ext` states that for any given category `C` of type `u`, which has a shift in the integers, and any two Pretriangulated Triangles `T₁` and `T₂` in `C`, any two morphisms `x` and `y` from `T₁` to `T₂` are equal if and only if their corresponding components, `hom₁`, `hom₂`, and `hom₃`, are also equal.
More concisely: given two Pretriangulated Triangles `T₁` and `T₂` in a category `C` with shift and any morphisms `x : hom₁(T₁) (T₂[1])` and `y : hom₂(T₁) (T₂)`, `x = y` if and only if `hom₃(T₁) (T₂[1])(i) = hom₂(T₁[1]) (T₂) (i)` for all objects `i` in `C`.
|
CategoryTheory.Pretriangulated.TriangleMorphism.comm₂
theorem CategoryTheory.Pretriangulated.TriangleMorphism.comm₂ :
∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] [inst_1 : CategoryTheory.HasShift C ℤ]
{T₁ T₂ : CategoryTheory.Pretriangulated.Triangle C}
(self : CategoryTheory.Pretriangulated.TriangleMorphism T₁ T₂),
CategoryTheory.CategoryStruct.comp T₁.mor₂ self.hom₃ = CategoryTheory.CategoryStruct.comp self.hom₂ T₂.mor₂
The theorem `CategoryTheory.Pretriangulated.TriangleMorphism.comm₂` states that for any category `C` with a shift operation, and any two pretriangular triangles `T₁` and `T₂` in `C`, for any triangle morphism between `T₁` and `T₂`, the composition of the second morphism of `T₁` and the third morphism of the triangle morphism is the same as the composition of the second morphism of the triangle morphism and the second morphism of `T₂`. This condition is often termed as the second commutative square of a triangle morphism. It is one of the key properties that morphisms must satisfy in the theory of Pretriangulated categories, a concept in Category Theory in Mathematics.
More concisely: For any pretriangular categories C with a shift operation, given two pretriangular triangles T₁ and T₂ and a triangle morphism between them, the second composition of the morphisms is commutative: (T₁.2)∘(μ.2) = (μ.2)∘(T₂.2).
|
CategoryTheory.Pretriangulated.comp_hom₁
theorem CategoryTheory.Pretriangulated.comp_hom₁ :
∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] [inst_1 : CategoryTheory.HasShift C ℤ]
{X Y Z : CategoryTheory.Pretriangulated.Triangle C} (f : X ⟶ Y) (g : Y ⟶ Z),
(CategoryTheory.CategoryStruct.comp f g).hom₁ = CategoryTheory.CategoryStruct.comp f.hom₁ g.hom₁
The theorem `CategoryTheory.Pretriangulated.comp_hom₁` states that for any category `C` with a shift, given three objects `X`, `Y`, and `Z` in the pretriangulated triangle of `C`, and morphisms `f` from `X` to `Y` and `g` from `Y` to `Z`, the composite of `f` and `g` via `CategoryTheory.CategoryStruct.comp` (denoted `f ≫ g`), when projected to its first component (denoted as `.hom₁`) is the same as the composite of the first components of `f` and `g`. In other words, the operation of taking the first component of a morphism commutes with the composition of morphisms.
More concisely: For any pretriangulated category `C` with a shift, the composition of morphisms `f: X ⟶ Y` and `g: Y ⟶ Z` in `C` agrees with the composition of their first components when composing morphisms in `C` and taking the first component of the resulting morphism. In other words, `(f ≫ g).hom₁ = f.hom₁ ≫ g.hom₁`.
|
CategoryTheory.Pretriangulated.id_hom₁
theorem CategoryTheory.Pretriangulated.id_hom₁ :
∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] [inst_1 : CategoryTheory.HasShift C ℤ]
(A : CategoryTheory.Pretriangulated.Triangle C),
(CategoryTheory.CategoryStruct.id A).hom₁ = CategoryTheory.CategoryStruct.id A.obj₁
This theorem, `CategoryTheory.Pretriangulated.id_hom₁`, states that for any category `C` with a shift and any pretriangulated triangle `A` in that category, the first morphism (`hom₁`) of the identity morphism on `A` is equal to the identity morphism on the first object (`obj₁`) of `A`. In other words, in the context of pretriangulated categories, the identity morphism on a triangle preserves the identity of the first object of the triangle.
More concisely: In a pretriangulated category with shift, the identity morphism on a triangle maps the first object to itself.
|
CategoryTheory.Pretriangulated.id_hom₃
theorem CategoryTheory.Pretriangulated.id_hom₃ :
∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] [inst_1 : CategoryTheory.HasShift C ℤ]
(A : CategoryTheory.Pretriangulated.Triangle C),
(CategoryTheory.CategoryStruct.id A).hom₃ = CategoryTheory.CategoryStruct.id A.obj₃
This theorem, `CategoryTheory.Pretriangulated.id_hom₃`, states that for every pre-triangulated category `C` (of any type `u`) that also has an integer (ℤ) shift, and for any given triangle `A` in this category, the third morphism `hom₃` of the identity morphism on `A` is equal to the identity morphism on the third object `obj₃` of `A`. In essence, this theorem ensures that the identity operation is preserved when applying the third morphism in a triangle in a pre-triangulated category.
More concisely: In a pre-triangulated category with integer shifts, the third morphism of the identity on an object equals the identity morphism on the third object in any triangle.
|
CategoryTheory.Pretriangulated.id_hom₂
theorem CategoryTheory.Pretriangulated.id_hom₂ :
∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] [inst_1 : CategoryTheory.HasShift C ℤ]
(A : CategoryTheory.Pretriangulated.Triangle C),
(CategoryTheory.CategoryStruct.id A).hom₂ = CategoryTheory.CategoryStruct.id A.obj₂
The theorem `CategoryTheory.Pretriangulated.id_hom₂` states that for any category `C` of a certain type, given that `C` has a shift structure over the integers (`ℤ`), for any pretriangulated triangle `A` in `C`, the `hom₂` (second homomorphism) of the identity of `A` is equal to the identity of the object `obj₂` of `A`. In other words, applying the identity morphism of the triangle to the second homomorphism results in the same object as applying the identity morphism to the second object of the triangle.
More concisely: For any pretriangulated category `C` with shift structure over `ℤ`, the identity morphism of a triangle in `C` equals the second homomorphism on the identity morphism of the second object of the triangle.
|