CategoryTheory.Pretriangulated.Triangle.mor₁_eq_zero_iff_mono₂
theorem CategoryTheory.Pretriangulated.Triangle.mor₁_eq_zero_iff_mono₂ :
∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] [inst_1 : CategoryTheory.Limits.HasZeroObject C]
[inst_2 : CategoryTheory.HasShift C ℤ] [inst_3 : CategoryTheory.Preadditive C]
[inst_4 : ∀ (n : ℤ), (CategoryTheory.shiftFunctor C n).Additive] [hC : CategoryTheory.Pretriangulated C],
∀ T ∈ CategoryTheory.Pretriangulated.distinguishedTriangles, T.mor₁ = 0 ↔ CategoryTheory.Mono T.mor₂
This theorem states that in a pretriangulated category with integer shifts and zero objects, for any triangle that is a part of the distinguished triangles of the category, the first morphism of the triangle being zero is equivalent to the second morphism of the triangle being a monomorphism. Here, a pretriangulated category refers to a category that has a distinguished class of triangles and satisfies some coherency conditions, and a monomorphism is a morphism that is left-cancellable, that is, if it is composed with any other morphism, the resulting morphism is uniquely determined by the other morphism.
More concisely: In a pretriangulated category with integer shifts and zero objects, the first morphism of a distinguished triangle being zero is equivalent to the second morphism being a monomorphism.
|
CategoryTheory.Pretriangulated.distinguished_cocone_triangle₁
theorem CategoryTheory.Pretriangulated.distinguished_cocone_triangle₁ :
∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] [inst_1 : CategoryTheory.Limits.HasZeroObject C]
[inst_2 : CategoryTheory.HasShift C ℤ] [inst_3 : CategoryTheory.Preadditive C]
[inst_4 : ∀ (n : ℤ), (CategoryTheory.shiftFunctor C n).Additive] [hC : CategoryTheory.Pretriangulated C] {Y Z : C}
(g : Y ⟶ Z),
∃ X f h,
CategoryTheory.Pretriangulated.Triangle.mk f g h ∈ CategoryTheory.Pretriangulated.distinguishedTriangles
This theorem states that for any category `C` which possesses the properties of having a zero object, being preadditive, pretriangulated and where every shift functor is additive, any morphism `g : Y ⟶ Z` for objects `Y` and `Z` in `C` is part of a distinguished triangle. This distinguished triangle in the category `C` is defined by an object `X` and morphisms `f : X ⟶ Y` and `h : Z ⟶ X⟦1⟧`, where `X⟦1⟧` refers to the object `X` shifted by 1.
More concisely: In a preadditive, pretriangulated category `C` with a zero object and additive shift functors, every morphism `g : Y ⟶ Z` has a distinguished triangle `X ⟶ Y ⟶ Z ⟶ X⟦1⟧`, where `X` is an object and `f : X ⟶ Y` and `h : Z ⟶ X⟦1⟧` are morphisms.
|
CategoryTheory.Pretriangulated.distinguished_cocone_triangle
theorem CategoryTheory.Pretriangulated.distinguished_cocone_triangle :
∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] [inst_1 : CategoryTheory.Limits.HasZeroObject C]
[inst_2 : CategoryTheory.HasShift C ℤ] [inst_3 : CategoryTheory.Preadditive C]
[inst_4 : ∀ (n : ℤ), (CategoryTheory.shiftFunctor C n).Additive] [self : CategoryTheory.Pretriangulated C]
{X Y : C} (f : X ⟶ Y),
∃ Z g h,
CategoryTheory.Pretriangulated.Triangle.mk f g h ∈ CategoryTheory.Pretriangulated.distinguishedTriangles
The theorem `CategoryTheory.Pretriangulated.distinguished_cocone_triangle` states that for any given category `C` that has zero objects, a shift, is preadditive, and for which the shift functor is additive for any integer `n`, and any objects `X` and `Y` in `C` with a morphism `f` from `X` to `Y`, there exists an object `Z` and morphisms `g` and `h` such that the triangle formed by `X`, `Y`, and `Z` with morphisms `f`, `g`, and `h` respectively is a distinguished triangle in the pretriangulated category `C`. A distinguished triangle is an important concept in homological algebra and is defined by a sequence of morphisms such that certain properties hold. In this context, `f` is a morphism from `X` to `Y`, `g` is a morphism from `Y` to `Z`, and `h` is a morphism from `Z` to `X⟦1⟧`, where `X⟦1⟧` is the object `X` shifted by 1.
More concisely: In a preadditive, zero-object category with additive shift functor, given any morphism between objects, there exists a distinguished triangle.
|
CategoryTheory.Pretriangulated.comp_distTriang_mor_zero₃₁
theorem CategoryTheory.Pretriangulated.comp_distTriang_mor_zero₃₁ :
∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] [inst_1 : CategoryTheory.Limits.HasZeroObject C]
[inst_2 : CategoryTheory.HasShift C ℤ] [inst_3 : CategoryTheory.Preadditive C]
[inst_4 : ∀ (n : ℤ), (CategoryTheory.shiftFunctor C n).Additive] [hC : CategoryTheory.Pretriangulated C],
∀ T ∈ CategoryTheory.Pretriangulated.distinguishedTriangles,
CategoryTheory.CategoryStruct.comp T.mor₃ ((CategoryTheory.shiftFunctor C 1).map T.mor₁) = 0
The theorem `CategoryTheory.Pretriangulated.comp_distTriang_mor_zero₃₁` states that in any pretriangulated category `C` that has a zero object and a shift functor, for any distinguished triangle `T` in `C`, the composition of the third morphism of `T` with the shifted first morphism of `T` is equal to zero. A distinguished triangle in a category `C` is represented by three objects (`X`, `Y`, `Z` in the diagram) and three morphisms (`f`, `g` and `h` in the diagram), with `h` composed with the shifted `f` being zero. This is a fundamental property in the theory of triangulated categories. See [Stacks Project, Tag 0146](https://stacks.math.columbia.edu/tag/0146) for more details about this property.
More concisely: In any pretriangulated category with a shift functor and a zero object, the composition of the third morphism of a distinguished triangle with the shifted first morphism is zero.
|
CategoryTheory.Pretriangulated.rotate_distinguished_triangle
theorem CategoryTheory.Pretriangulated.rotate_distinguished_triangle :
∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] [inst_1 : CategoryTheory.Limits.HasZeroObject C]
[inst_2 : CategoryTheory.HasShift C ℤ] [inst_3 : CategoryTheory.Preadditive C]
[inst_4 : ∀ (n : ℤ), (CategoryTheory.shiftFunctor C n).Additive] [self : CategoryTheory.Pretriangulated C]
(T : CategoryTheory.Pretriangulated.Triangle C),
T ∈ CategoryTheory.Pretriangulated.distinguishedTriangles ↔
T.rotate ∈ CategoryTheory.Pretriangulated.distinguishedTriangles
This theorem states that, given a category `C` with certain properties (it has a zero object, it has a shift functor with integers, it's preadditive, and each shift functor is additive), and for a pretriangulated structure on `C`, a triangle `T` in `C` is distinguished if and only if its rotation (i.e., the triangle obtained by 'rotating' the objects and morphisms of `T`) is also distinguished.
Here, a 'distinguished triangle' refers to a specific configuration of objects and morphisms in the category that satisfy certain conditions, which are important in the theory of triangulated categories. The 'rotation' of a triangle is a specific operation that produces a new triangle from the given one. The theorem is essentially saying that this rotation operation preserves the property of being distinguished.
More concisely: Given a preadditive, pretriangulated category with a shift functor, a triangle is distinguished if and only if its rotation is distinguished.
|
CategoryTheory.Pretriangulated.complete_distinguished_triangle_morphism
theorem CategoryTheory.Pretriangulated.complete_distinguished_triangle_morphism :
∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] [inst_1 : CategoryTheory.Limits.HasZeroObject C]
[inst_2 : CategoryTheory.HasShift C ℤ] [inst_3 : CategoryTheory.Preadditive C]
[inst_4 : ∀ (n : ℤ), (CategoryTheory.shiftFunctor C n).Additive] [self : CategoryTheory.Pretriangulated C]
(T₁ T₂ : CategoryTheory.Pretriangulated.Triangle C),
T₁ ∈ CategoryTheory.Pretriangulated.distinguishedTriangles →
T₂ ∈ CategoryTheory.Pretriangulated.distinguishedTriangles →
∀ (a : T₁.obj₁ ⟶ T₂.obj₁) (b : T₁.obj₂ ⟶ T₂.obj₂),
CategoryTheory.CategoryStruct.comp T₁.mor₁ b = CategoryTheory.CategoryStruct.comp a T₂.mor₁ →
∃ c,
CategoryTheory.CategoryStruct.comp T₁.mor₂ c = CategoryTheory.CategoryStruct.comp b T₂.mor₂ ∧
CategoryTheory.CategoryStruct.comp T₁.mor₃ ((CategoryTheory.shiftFunctor C 1).map a) =
CategoryTheory.CategoryStruct.comp c T₂.mor₃
The theorem `CategoryTheory.Pretriangulated.complete_distinguished_triangle_morphism` states that for any category `C` that has a zero object, a shift functor, is preadditive, and pretriangulated, and for any two distinguished triangles `T₁` and `T₂` in `C`, given a commutative square formed by the morphisms `a` and `b` from `T₁` to `T₂`, there exists a morphism `c` such that the triangles `T₁` and `T₂` form a morphism of triangles, i.e., the diagram commutes. In other words, the composition of `T₁.mor₁` and `b` is equal to the composition of `a` and `T₂.mor₁`, the composition of `T₁.mor₂` and `c` is equal to the composition of `b` and `T₂.mor₂`, and the composition of `T₁.mor₃` and the shifted version of `a` is equal to the composition of `c` and `T₂.mor₃`. This theorem is significant in the study of category theory as it formalizes a key property of distinguished triangles in pretriangulated categories.
More concisely: Given any preadditive, pretriangulated category `C` with a zero object and shift functor, for any commutative square formed by morphisms between distinguished triangles, there exists a morphism making the triangles isomorphic.
|
CategoryTheory.Pretriangulated.complete_distinguished_triangle_morphism₁
theorem CategoryTheory.Pretriangulated.complete_distinguished_triangle_morphism₁ :
∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] [inst_1 : CategoryTheory.Limits.HasZeroObject C]
[inst_2 : CategoryTheory.HasShift C ℤ] [inst_3 : CategoryTheory.Preadditive C]
[inst_4 : ∀ (n : ℤ), (CategoryTheory.shiftFunctor C n).Additive] [hC : CategoryTheory.Pretriangulated C]
(T₁ T₂ : CategoryTheory.Pretriangulated.Triangle C),
T₁ ∈ CategoryTheory.Pretriangulated.distinguishedTriangles →
T₂ ∈ CategoryTheory.Pretriangulated.distinguishedTriangles →
∀ (b : T₁.obj₂ ⟶ T₂.obj₂) (c : T₁.obj₃ ⟶ T₂.obj₃),
CategoryTheory.CategoryStruct.comp T₁.mor₂ c = CategoryTheory.CategoryStruct.comp b T₂.mor₂ →
∃ a,
CategoryTheory.CategoryStruct.comp T₁.mor₁ b = CategoryTheory.CategoryStruct.comp a T₂.mor₁ ∧
CategoryTheory.CategoryStruct.comp T₁.mor₃ ((CategoryTheory.shiftFunctor C 1).map a) =
CategoryTheory.CategoryStruct.comp c T₂.mor₃
This theorem, `CategoryTheory.Pretriangulated.complete_distinguished_triangle_morphism₁`, states that given two distinguished triangles `T₁` and `T₂` in a pretriangulated category `C` with a shift functor and zero object, if we have a commutative square involving morphisms `mor₂` of these triangles, then the square can be extended into a morphism of triangles. Here, the commutative square is defined by the morphisms `b: T₁.obj₂ ⟶ T₂.obj₂` and `c: T₁.obj₃ ⟶ T₂.obj₃` such that `T₁.mor₂` composed with `c` equals `b` composed with `T₂.mor₂`. The theorem guarantees the existence of a morphism `a` such that when `a` is composed with `T₂.mor₁`, it is equal to `T₁.mor₁` composed with `b`, and `T₁.mor₃` composed with the shift functor applied to `a` equals `c` composed with `T₂.mor₃`. This completes the extension of the commutative square into a morphism of triangles.
More concisely: Given two distinguished triangles in a pretriangulated category with a shift functor and zero object, and a commutative square between their morphisms, there exists a morphism extending the commutative square into a morphism of triangles.
|
CategoryTheory.Pretriangulated.Triangle.isZero₁_iff_isIso₂
theorem CategoryTheory.Pretriangulated.Triangle.isZero₁_iff_isIso₂ :
∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] [inst_1 : CategoryTheory.Limits.HasZeroObject C]
[inst_2 : CategoryTheory.HasShift C ℤ] [inst_3 : CategoryTheory.Preadditive C]
[inst_4 : ∀ (n : ℤ), (CategoryTheory.shiftFunctor C n).Additive] [hC : CategoryTheory.Pretriangulated C],
∀ T ∈ CategoryTheory.Pretriangulated.distinguishedTriangles,
CategoryTheory.Limits.IsZero T.obj₁ ↔ CategoryTheory.IsIso T.mor₂
This theorem states that for any given category `C` (which should be a pretriangulated category that has a zero object and a shift functor), if `T` belongs to the distinguished triangles of the pretriangulated category, then the object `T.obj₁` is a zero object if and only if the morphism `T.mor₂` is an isomorphism. This condition applies for all integers `n` for which the shift functor `CategoryTheory.shiftFunctor C n` is additive.
More concisely: In a pretriangulated category `C` with a zero object and additive shift functor, a distinguished triangle `T` has `T.obj₁` as a zero object if and only if `T.mor₂` is an isomorphism.
|
CategoryTheory.Pretriangulated.Triangle.coyoneda_exact₂
theorem CategoryTheory.Pretriangulated.Triangle.coyoneda_exact₂ :
∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] [inst_1 : CategoryTheory.Limits.HasZeroObject C]
[inst_2 : CategoryTheory.HasShift C ℤ] [inst_3 : CategoryTheory.Preadditive C]
[inst_4 : ∀ (n : ℤ), (CategoryTheory.shiftFunctor C n).Additive] [hC : CategoryTheory.Pretriangulated C],
∀ T ∈ CategoryTheory.Pretriangulated.distinguishedTriangles,
∀ {X : C} (f : X ⟶ T.obj₂),
CategoryTheory.CategoryStruct.comp f T.mor₂ = 0 → ∃ g, f = CategoryTheory.CategoryStruct.comp g T.mor₁
This theorem is about the exactness property of a pretriangulated category. Given a pretriangulated category `C`, which is also preadditive and has a zero object and shift functor, for any distinguished triangle `T` in this category, if we have an object `X` in this category and a morphism `f` from `X` to the second object in the triangle `T` such that the composition of `f` and the second morphism in `T` is zero, then there exists another morphism `g` such that `f` is the composition of `g` and the first morphism in `T`. This property is a part of the axioms of a category being triangulated, and the theorem suggests that the coyoneda functor preserves exact sequences.
More concisely: In a pretriangulated category with zero object and shift functor, given a distinguished triangle and a morphism with zero composition, there exists another morphism making the given morphism the composition of the first two morphisms in the triangle.
|
CategoryTheory.Pretriangulated.Triangle.mor₃_eq_zero_iff_epi₂
theorem CategoryTheory.Pretriangulated.Triangle.mor₃_eq_zero_iff_epi₂ :
∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] [inst_1 : CategoryTheory.Limits.HasZeroObject C]
[inst_2 : CategoryTheory.HasShift C ℤ] [inst_3 : CategoryTheory.Preadditive C]
[inst_4 : ∀ (n : ℤ), (CategoryTheory.shiftFunctor C n).Additive] [hC : CategoryTheory.Pretriangulated C],
∀ T ∈ CategoryTheory.Pretriangulated.distinguishedTriangles, T.mor₃ = 0 ↔ CategoryTheory.Epi T.mor₂
The theorem `CategoryTheory.Pretriangulated.Triangle.mor₃_eq_zero_iff_epi₂` states that for any category `C` with a zero object, a shift by integers, additive structure, and pretriangulated structure, for any triangle `T` which belongs to the distinguished triangle category, the third morphism `T.mor₃` in the triangle is equal to zero if and only if the second morphism `T.mor₂` is an epimorphism. Here, epimorphism refers to a morphism for which any two morphisms from its codomain can be made equal by precomposing with it.
More concisely: For any pretriangulated category with additive structure and zero object, the third morphism in a distinguished triangle is zero if and only if the second morphism is an epimorphism.
|
CategoryTheory.Pretriangulated.contractible_distinguished
theorem CategoryTheory.Pretriangulated.contractible_distinguished :
∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] [inst_1 : CategoryTheory.Limits.HasZeroObject C]
[inst_2 : CategoryTheory.HasShift C ℤ] [inst_3 : CategoryTheory.Preadditive C]
[inst_4 : ∀ (n : ℤ), (CategoryTheory.shiftFunctor C n).Additive] [self : CategoryTheory.Pretriangulated C]
(X : C),
CategoryTheory.Pretriangulated.contractibleTriangle X ∈ CategoryTheory.Pretriangulated.distinguishedTriangles
The theorem `CategoryTheory.Pretriangulated.contractible_distinguished` states that for any object `X` in a pretriangulated category `C` that has a zero object, an integer shift functor, and a preadditive structure, the triangle `X ⟶ X ⟶ 0 ⟶ X⟦1⟧`, known as the contractible triangle, is always a distinguished triangle. Here, "distinguished triangle" is a concept in the context of triangulated categories, which are categories equipped with an additive structure, a shift functor, and a class of distinguished triangles satisfying certain axioms. The "contractible triangle" mentioned here is a specific type of distinguished triangle.
More concisely: In a pretriangulated category with a zero object, an integer shift functor, and a preadditive structure, the contractible triangle `X ⟶ X ⟶ 0 ⟶ X[1]` is always a distinguished triangle.
|
CategoryTheory.Pretriangulated.distinguished_cocone_triangle₂
theorem CategoryTheory.Pretriangulated.distinguished_cocone_triangle₂ :
∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] [inst_1 : CategoryTheory.Limits.HasZeroObject C]
[inst_2 : CategoryTheory.HasShift C ℤ] [inst_3 : CategoryTheory.Preadditive C]
[inst_4 : ∀ (n : ℤ), (CategoryTheory.shiftFunctor C n).Additive] [hC : CategoryTheory.Pretriangulated C] {Z X : C}
(h : Z ⟶ (CategoryTheory.shiftFunctor C 1).obj X),
∃ Y f g,
CategoryTheory.Pretriangulated.Triangle.mk f g h ∈ CategoryTheory.Pretriangulated.distinguishedTriangles
This theorem states that in any category `C` which has a zero object, a shift, is preadditive, and is pretriangulated, any given morphism `h` from an object `Z` to the shift of an object `X` by 1, can be completed to a distinguished triangle in the category. More concretely, given `h : Z ⟶ X⟦1⟧`, there exists an object `Y` and morphisms `f` and `g` such that the triangle formed by `f : X ⟶ Y`, `g : Y ⟶ Z`, and `h: Z ⟶ X⟦1⟧` is a distinguished triangle in the category `C`.
More concisely: In a preadditive, pretriangulated category with a zero object, any morphism from an object to the shift of another object can be completed to a distinguished triangle.
|
CategoryTheory.Pretriangulated.comp_distTriang_mor_zero₁₂
theorem CategoryTheory.Pretriangulated.comp_distTriang_mor_zero₁₂ :
∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] [inst_1 : CategoryTheory.Limits.HasZeroObject C]
[inst_2 : CategoryTheory.HasShift C ℤ] [inst_3 : CategoryTheory.Preadditive C]
[inst_4 : ∀ (n : ℤ), (CategoryTheory.shiftFunctor C n).Additive] [hC : CategoryTheory.Pretriangulated C],
∀ T ∈ CategoryTheory.Pretriangulated.distinguishedTriangles,
CategoryTheory.CategoryStruct.comp T.mor₁ T.mor₂ = 0
This theorem states that in any category `C` that has a zero object, supports shifting by integers, is preadditive, and is pretriangulated, for any distinguished triangle in `C` (represented as a diagram with morphisms `f`, `g`, and `h` going from `X` to `Y`, `Y` to `Z`, and `Z` to `X⟦1⟧` respectively), the composition of the first two morphisms `f` and `g` is equal to the zero morphism. This property is a fundamental characteristic of distinguished triangles in pretriangulated categories.
More concisely: In any pretriangulated preadditive category with a zero object, the composition of morphisms in a distinguished triangle is equal to the zero morphism.
|
CategoryTheory.Pretriangulated.contractible_distinguished₂
theorem CategoryTheory.Pretriangulated.contractible_distinguished₂ :
∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] [inst_1 : CategoryTheory.Limits.HasZeroObject C]
[inst_2 : CategoryTheory.HasShift C ℤ] [inst_3 : CategoryTheory.Preadditive C]
[inst_4 : ∀ (n : ℤ), (CategoryTheory.shiftFunctor C n).Additive] [hC : CategoryTheory.Pretriangulated C] (X : C),
CategoryTheory.Pretriangulated.Triangle.mk 0 0
(CategoryTheory.CategoryStruct.id ((CategoryTheory.shiftFunctor C 1).obj X)) ∈
CategoryTheory.Pretriangulated.distinguishedTriangles
The theorem `CategoryTheory.Pretriangulated.contractible_distinguished₂` states that for any category `C` that has a zero object, a shift functor, is preadditive, and is pretriangulated, and for any object `X` in `C`, the triangle `X ⟶ 0 ⟶ X⟦1⟧ ⟶ X⟦1⟧` is a distinguished triangle. Here, the morphisms are the zero morphism and the identity morphism on the shifted object `X⟦1⟧`. A distinguished triangle is a specific configuration of objects and morphisms that plays a key role in the theory of triangulated categories, which are used in various areas of algebra and geometry.
More concisely: In a preadditive, pretriangulated category with a zero object, the triangle formed by the zero morphism to the zero object and the identity morphism on the shift of an object is a distinguished triangle.
|
CategoryTheory.Pretriangulated.Triangle.isZero₂_iff
theorem CategoryTheory.Pretriangulated.Triangle.isZero₂_iff :
∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] [inst_1 : CategoryTheory.Limits.HasZeroObject C]
[inst_2 : CategoryTheory.HasShift C ℤ] [inst_3 : CategoryTheory.Preadditive C]
[inst_4 : ∀ (n : ℤ), (CategoryTheory.shiftFunctor C n).Additive] [hC : CategoryTheory.Pretriangulated C],
∀ T ∈ CategoryTheory.Pretriangulated.distinguishedTriangles,
CategoryTheory.Limits.IsZero T.obj₂ ↔ T.mor₁ = 0 ∧ T.mor₂ = 0
This theorem states that for any category `C` with some specific properties (it must be a category, have a zero object, have a shift operation defined on it, be preadditive, have additive shift functors for all integers, and be pretriangulated) and for any distinguished triangle `T` in `C`, the second object of the triangle `T` is a zero object if and only if the first and the second morphisms of `T` are zero.
Here, a distinguished triangle is a concept in the theory of triangulated categories, which are a kind of category that have been used to investigate a wide range of problems in mathematics. A zero object in a category is an object that is both a initial object and a terminal object. A morphism being zero means that it is the same as the unique morphism to the zero object from the domain of the morphism. Preadditive categories are categories in which the hom-sets are abelian groups and composition of morphisms is bilinear. Shift functors are a kind of functor used in the context of triangulated categories to understand the shifts in the morphisms.
More concisely: In a pretriangulated preadditive category with shift functors and a zero object, a distinguished triangle with zero first and second morphisms has a zero second object.
|
CategoryTheory.Pretriangulated.contractible_distinguished₁
theorem CategoryTheory.Pretriangulated.contractible_distinguished₁ :
∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] [inst_1 : CategoryTheory.Limits.HasZeroObject C]
[inst_2 : CategoryTheory.HasShift C ℤ] [inst_3 : CategoryTheory.Preadditive C]
[inst_4 : ∀ (n : ℤ), (CategoryTheory.shiftFunctor C n).Additive] [hC : CategoryTheory.Pretriangulated C] (X : C),
CategoryTheory.Pretriangulated.Triangle.mk 0 (CategoryTheory.CategoryStruct.id X) 0 ∈
CategoryTheory.Pretriangulated.distinguishedTriangles
The theorem `CategoryTheory.Pretriangulated.contractible_distinguished₁` states that for any pretriangulated category `C` with a zero object and a shift functor, and any object `X` in `C`, the "obvious" triangles formed by going from the zero object to `X` with the identity morphism, then from `X` back to the zero object, are considered distinguished. Here, distinguished triangles are a crucial concept in the theory of triangulated categories, and the 'shift' of an object is a way of moving it 'up' in the category. The triangles are deemed 'obvious' due to their minimalistic nature, involving only the zero object, `X` and identity morphisms.
More concisely: In a pretriangulated category with a zero object and shift functor, the triangles formed by the zero object, an object X, and the identity morphisms between them are distinguished.
|
CategoryTheory.Pretriangulated.complete_distinguished_triangle_morphism₂
theorem CategoryTheory.Pretriangulated.complete_distinguished_triangle_morphism₂ :
∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] [inst_1 : CategoryTheory.Limits.HasZeroObject C]
[inst_2 : CategoryTheory.HasShift C ℤ] [inst_3 : CategoryTheory.Preadditive C]
[inst_4 : ∀ (n : ℤ), (CategoryTheory.shiftFunctor C n).Additive] [hC : CategoryTheory.Pretriangulated C]
(T₁ T₂ : CategoryTheory.Pretriangulated.Triangle C),
T₁ ∈ CategoryTheory.Pretriangulated.distinguishedTriangles →
T₂ ∈ CategoryTheory.Pretriangulated.distinguishedTriangles →
∀ (a : T₁.obj₁ ⟶ T₂.obj₁) (c : T₁.obj₃ ⟶ T₂.obj₃),
CategoryTheory.CategoryStruct.comp T₁.mor₃ ((CategoryTheory.shiftFunctor C 1).map a) =
CategoryTheory.CategoryStruct.comp c T₂.mor₃ →
∃ b,
CategoryTheory.CategoryStruct.comp T₁.mor₁ b = CategoryTheory.CategoryStruct.comp a T₂.mor₁ ∧
CategoryTheory.CategoryStruct.comp T₁.mor₂ c = CategoryTheory.CategoryStruct.comp b T₂.mor₂
This theorem states that given two distinguished triangles `T₁` and `T₂` in a pretriangulated category `C` with integer shifts and zero objects, if there exist morphisms `a` from the first object of `T₁` to the first object of `T₂` and `c` from the third object of `T₁` to the third object of `T₂` such that the composition of the third morphism of `T₁` with the shift of `a` equals the composition of `c` with the third morphism of `T₂`, then there exists a morphism `b` such that the composition of the first morphism of `T₁` with `b` equals the composition of `a` with the first morphism of `T₂`, and similarly for the second morphisms. In other words, given a commutative square involving the third morphisms, we can extend it to a morphism of triangles.
More concisely: Given two distinguished triangles in a pretriangulated category with integer shifts and zero objects, if the third morphisms compose commutatively up to a shift, then there exists a morphism making both triangles commute.
|
CategoryTheory.Pretriangulated.productTriangle_distinguished
theorem CategoryTheory.Pretriangulated.productTriangle_distinguished :
∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] [inst_1 : CategoryTheory.Limits.HasZeroObject C]
[inst_2 : CategoryTheory.HasShift C ℤ] [inst_3 : CategoryTheory.Preadditive C]
[inst_4 : ∀ (n : ℤ), (CategoryTheory.shiftFunctor C n).Additive] [hC : CategoryTheory.Pretriangulated C]
{J : Type u_1} (T : J → CategoryTheory.Pretriangulated.Triangle C),
(∀ (j : J), T j ∈ CategoryTheory.Pretriangulated.distinguishedTriangles) →
∀ [inst_5 : CategoryTheory.Limits.HasProduct fun j => (T j).obj₁]
[inst_6 : CategoryTheory.Limits.HasProduct fun j => (T j).obj₂]
[inst_7 : CategoryTheory.Limits.HasProduct fun j => (T j).obj₃]
[inst_8 : CategoryTheory.Limits.HasProduct fun j => (CategoryTheory.shiftFunctor C 1).obj (T j).obj₁],
CategoryTheory.Pretriangulated.productTriangle T ∈ CategoryTheory.Pretriangulated.distinguishedTriangles
The theorem `CategoryTheory.Pretriangulated.productTriangle_distinguished` states that given a category `C` with a zero object, a shift functor, and preadditive structure, and such that `C` is pretriangulated and the shift functor is additive for all integers `n`, for any type `J` and a function `T` associating each element of `J` to a distinguished triangle in `C`, if every triangle `T j` is distinguished, and if products exist in `C` for the three objects of each `T j` and for the first object of each `T j` shifted by 1, then the product of all these triangles is also a distinguished triangle in `C`.
In simpler terms, it is saying that if you can form a product out of distinguished triangles (which have certain mathematical properties) in a given category, then the resulting product is also a distinguished triangle. This is a property of the structure of certain types of mathematical categories.
More concisely: Given a pretriangulated category with a zero object, shift functor, and additivity for all integers, if every triangle is distinguished and products of three distinguished triangles and their shifts exist, then the product of all these triangles is a distinguished triangle.
|
CategoryTheory.Pretriangulated.isomorphic_distinguished
theorem CategoryTheory.Pretriangulated.isomorphic_distinguished :
∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] [inst_1 : CategoryTheory.Limits.HasZeroObject C]
[inst_2 : CategoryTheory.HasShift C ℤ] [inst_3 : CategoryTheory.Preadditive C]
[inst_4 : ∀ (n : ℤ), (CategoryTheory.shiftFunctor C n).Additive] [self : CategoryTheory.Pretriangulated C],
∀ T₁ ∈ CategoryTheory.Pretriangulated.distinguishedTriangles,
∀ (T₂ : CategoryTheory.Pretriangulated.Triangle C),
(T₂ ≅ T₁) → T₂ ∈ CategoryTheory.Pretriangulated.distinguishedTriangles
The theorem `CategoryTheory.Pretriangulated.isomorphic_distinguished` states that for any category `C` that has a zero object, has a shift with integers, is preadditive, and is pretriangulated, if we have a triangle `T₁` that is distinguished (belongs to the set of distinguished triangles), then any other triangle `T₂` in the same category `C` that is isomorphic to `T₁` is also distinguished (also belongs to the set of distinguished triangles). This is basically saying that the property of being a distinguished triangle is preserved under isomorphism in a pretriangulated category.
More concisely: In a pretriangulated category with a zero object and shift with integers, if two distinguished triangles are isomorphic, then they are equal.
|
CategoryTheory.Pretriangulated.inv_rot_of_distTriang
theorem CategoryTheory.Pretriangulated.inv_rot_of_distTriang :
∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] [inst_1 : CategoryTheory.Limits.HasZeroObject C]
[inst_2 : CategoryTheory.HasShift C ℤ] [inst_3 : CategoryTheory.Preadditive C]
[inst_4 : ∀ (n : ℤ), (CategoryTheory.shiftFunctor C n).Additive] [hC : CategoryTheory.Pretriangulated C],
∀ T ∈ CategoryTheory.Pretriangulated.distinguishedTriangles,
T.invRotate ∈ CategoryTheory.Pretriangulated.distinguishedTriangles
This theorem states that for any category `C` that has a zero object, a shift operation, is preadditive, and pretriangulated, and for any integer `n` where the shift functor is additive, if a triangle `T` is distinguished in the context of category `C`, then the inverse rotation of triangle `T` is also a distinguished triangle in the same category.
In mathematical terms, this theorem concerns the properties of distinguished triangles in pretriangulated categories: specifically, it asserts that the 'inverse rotation' operation (which is a certain transformation applied to the triangle) preserves the property of being distinguished.
More concisely: In a pretriangulated, preadditive category with a zero object and additive shift functor, the inverse rotation of a distinguished triangle is also a distinguished triangle.
|
CategoryTheory.Pretriangulated.rot_of_distTriang
theorem CategoryTheory.Pretriangulated.rot_of_distTriang :
∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] [inst_1 : CategoryTheory.Limits.HasZeroObject C]
[inst_2 : CategoryTheory.HasShift C ℤ] [inst_3 : CategoryTheory.Preadditive C]
[inst_4 : ∀ (n : ℤ), (CategoryTheory.shiftFunctor C n).Additive] [hC : CategoryTheory.Pretriangulated C],
∀ T ∈ CategoryTheory.Pretriangulated.distinguishedTriangles,
T.rotate ∈ CategoryTheory.Pretriangulated.distinguishedTriangles
This theorem states that in a pretriangulated category `C` (a category with extra structure that allows the definition of distinguished triangles), if we have a distinguished triangle `T`, then the rotated version of `T` is also a distinguished triangle. The rotation process is defined by some Functor called `CategoryTheory.shiftFunctor`, which moves objects and morphisms 'up'. This holds for any object `C`, irrespective of whether `C` is a zero object in the category or not. The statement of this theorem applies to an arbitrary additive functor associated with the shift functor.
More concisely: In a pretriangulated category, the rotated version of a distinguished triangle is also a distinguished triangle under the shift functor.
|
CategoryTheory.Pretriangulated.comp_distTriang_mor_zero₂₃
theorem CategoryTheory.Pretriangulated.comp_distTriang_mor_zero₂₃ :
∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] [inst_1 : CategoryTheory.Limits.HasZeroObject C]
[inst_2 : CategoryTheory.HasShift C ℤ] [inst_3 : CategoryTheory.Preadditive C]
[inst_4 : ∀ (n : ℤ), (CategoryTheory.shiftFunctor C n).Additive] [hC : CategoryTheory.Pretriangulated C],
∀ T ∈ CategoryTheory.Pretriangulated.distinguishedTriangles,
CategoryTheory.CategoryStruct.comp T.mor₂ T.mor₃ = 0
The theorem `CategoryTheory.Pretriangulated.comp_distTriang_mor_zero₂₃` states that in any pretriangulated category `C` with a zero object, a shift functor, and a preadditive structure, if we have a distinguished triangle represented by the morphisms `f`, `g`, and `h` from objects `X`, `Y`, and `Z` such that it forms a cycle `X --f--> Y --g--> Z --h--> X⟦1⟧`, then the composition of the morphisms `g` and `h` (represented as `g ≫ h`) is always equal to the zero morphism. This theorem is a property of distinguished triangles in pretriangulated categories. For more context, refer to [Stacks Project](https://stacks.math.columbia.edu/tag/0146).
More concisely: In any pretriangulated category with a zero object, shift functor, and preadditive structure, the composition of morphisms in a distinguished triangle forms a cycle if and only if the composition of the morphisms is the identity on the zero object, i.e., the morphism is zero.
|