HomologicalComplex.single_obj_d
theorem HomologicalComplex.single_obj_d :
∀ {V : Type u} [inst : CategoryTheory.Category.{v, u} V] [inst_1 : CategoryTheory.Limits.HasZeroMorphisms V]
[inst_2 : CategoryTheory.Limits.HasZeroObject V] {ι : Type u_1} [inst_3 : DecidableEq ι] (c : ComplexShape ι)
(j : ι) (A : V) (k l : ι), ((HomologicalComplex.single V c j).obj A).d k l = 0
This theorem states that for any type `V` that is a category with zero morphisms and zero object, for any `ComplexShape c`, any object `j` of a certain type `ι`, and any `A` of type `V`, the morphism `d` between any two objects `k` and `l` in the homological complex obtained by applying the functor `HomologicalComplex.single V c j` to `A` is the zero morphism. This is assuming that the equality between objects of type `ι` is decidable.
More concisely: For any type `V` that is a category with zero morphisms and zero object, the application of the functor `HomologicalComplex.single V` to any object `A` of type `V`, results in all morphisms in the obtained complex being the zero morphism, given decidable equality of objects of type `ι`.
|
HomologicalComplex.mkHomToSingle_f
theorem HomologicalComplex.mkHomToSingle_f :
∀ {V : Type u} [inst : CategoryTheory.Category.{v, u} V] [inst_1 : CategoryTheory.Limits.HasZeroMorphisms V]
[inst_2 : CategoryTheory.Limits.HasZeroObject V] {ι : Type u_1} [inst_3 : DecidableEq ι] {c : ComplexShape ι}
{K : HomologicalComplex V c} {j : ι} {A : V} (φ : K.X j ⟶ A)
(hφ : ∀ (i : ι), c.Rel i j → CategoryTheory.CategoryStruct.comp (K.d i j) φ = 0),
(HomologicalComplex.mkHomToSingle φ hφ).f j =
CategoryTheory.CategoryStruct.comp φ (HomologicalComplex.singleObjXSelf c j A).inv
This theorem states that for any type `V` given a category structure, having zero morphisms and zero object, a type `ι` with decidable equality, a complex shape `c` over `ι`, a homological complex `K` over `V` and `c`, any element `j` of type `ι`, and any object `A` of `V`, if we have a morphism `φ` from `K.X j` to `A` such that the composition of `K.d i j` and `φ` is zero for all `i` where `c.Rel i j` holds, then the application of function `f` at `j` on `HomologicalComplex.mkHomToSingle φ hφ` is equivalent to the composition of `φ` and the inverse morphism on `HomologicalComplex.singleObjXSelf c j A`. This theorem essentially describes a property of constructing morphisms in a homological complex in the context of category theory.
More concisely: Given a homological complex over a category with zero morphisms and objects, a complex shape, type `ι` with decidable equality, an element `j` of `ι`, and an object `A`, if there exists a morphism `φ` from the complex at `j` to `A` such that the composition of `φ` with each boundary morphism `K.d i j` is zero whenever `c.Rel i j` holds, then `f(HomologicalComplex.mkHomToSingle φ hφ)` is equivalent to the composition of `φ` and the inverse morphism on `HomologicalComplex.singleObjXSelf c j A`.
|
HomologicalComplex.from_single_hom_ext
theorem HomologicalComplex.from_single_hom_ext :
∀ {V : Type u} [inst : CategoryTheory.Category.{v, u} V] [inst_1 : CategoryTheory.Limits.HasZeroMorphisms V]
[inst_2 : CategoryTheory.Limits.HasZeroObject V] {ι : Type u_1} [inst_3 : DecidableEq ι] (c : ComplexShape ι)
{K : HomologicalComplex V c} {j : ι} {A : V} {f g : (HomologicalComplex.single V c j).obj A ⟶ K},
f.f j = g.f j → f = g
The theorem `HomologicalComplex.from_single_hom_ext` states that for any category `V` with zero morphisms and zero object, any complex shape `c`, any homological complex `K` on `V` with shape `c`, any object `j` from a type `ι` with decidable equality, and any object `A` from `V`, if we have two morphisms `f` and `g` from the single-object homological complex at `j` with object `A` to `K`, then if the morphism at `j` in `f` is equal to the morphism at `j` in `g`, it follows that `f` and `g` are equal. This theorem is essential in homological algebra for comparing morphisms between homological complexes.
More concisely: Given a homological complex `K` on a zero object category `V` with decidable equality, two morphisms `f` and `g` from the single-object complex at `j` with object `A` to `K` having equal morphism at `j`, imply `f = g`.
|
ChainComplex.single₀_map_f_zero
theorem ChainComplex.single₀_map_f_zero :
∀ {V : Type u} [inst : CategoryTheory.Category.{v, u} V] [inst_1 : CategoryTheory.Limits.HasZeroMorphisms V]
[inst_2 : CategoryTheory.Limits.HasZeroObject V] {A B : V} (f : A ⟶ B),
((ChainComplex.single₀ V).map f).f 0 = f
This theorem, `ChainComplex.single₀_map_f_zero`, states that for any category `V` that has zero morphisms and a zero object, and for any two objects `A` and `B` in `V` with a morphism `f` from `A` to `B`, the morphism at degree zero (`f 0`) in the chain complex generated by applying the functor `ChainComplex.single₀ V` to `f`, is equal to `f` itself. In other words, the functor `ChainComplex.single₀ V` preserves the original morphism `f` at degree zero when mapping it into a chain complex.
More concisely: For any category with zero morphisms and a zero object, the morphism at degree 0 in the chain complex generated by applying `ChainComplex.single₀` to a morphism is equal to the morphism itself.
|
HomologicalComplex.single_obj_X_self
theorem HomologicalComplex.single_obj_X_self :
∀ {V : Type u} [inst : CategoryTheory.Category.{v, u} V] [inst_1 : CategoryTheory.Limits.HasZeroMorphisms V]
[inst_2 : CategoryTheory.Limits.HasZeroObject V] {ι : Type u_1} [inst_3 : DecidableEq ι] (c : ComplexShape ι)
(j : ι) (A : V), ((HomologicalComplex.single V c j).obj A).X j = A
This theorem, `HomologicalComplex.single_obj_X_self`, states that for any type `V` equipped with a category structure, zero morphisms, and zero object, any type `ι` with decidable equality, a complex shape `c` of type `ι`, an element `j` of type `ι`, and an object `A` of the category `V`, the j-th object of the homological complex obtained by applying the functor `HomologicalComplex.single V c j` to `A` is equal to `A` itself. Here, `HomologicalComplex.single V c j` is a functor that constructs a homological complex with `j` as the only non-zero object.
More concisely: For any category `V` with zero object and zero morphisms, type `ι` with decidable equality, complex shape `c` of type `ι`, and object `A` in `V`, the j-th object of the single-object homological complex `HomologicalComplex.single V c j A` equals `A`.
|
HomologicalComplex.to_single_hom_ext
theorem HomologicalComplex.to_single_hom_ext :
∀ {V : Type u} [inst : CategoryTheory.Category.{v, u} V] [inst_1 : CategoryTheory.Limits.HasZeroMorphisms V]
[inst_2 : CategoryTheory.Limits.HasZeroObject V] {ι : Type u_1} [inst_3 : DecidableEq ι] (c : ComplexShape ι)
{K : HomologicalComplex V c} {j : ι} {A : V} {f g : K ⟶ (HomologicalComplex.single V c j).obj A},
f.f j = g.f j → f = g
This theorem, named `HomologicalComplex.to_single_hom_ext`, states that for any category `V` with zero morphisms and a zero object, given a complex shape `c` indexed by a type `ι` with decidable equality, a homological complex `K` over `V` and `c`, an object `j` of type `ι`, and an object `A` of `V`, if we have two morphisms `f` and `g` from `K` to the single-object homological complex at `A` indexed by `j` and they are the same at the index `j`, then the morphisms `f` and `g` are identical.
More concisely: For any homological complex `K` over a category `V` with zero morphisms and a zero object, two morphisms from `K` to the single-object complex at an object `A` indexed by `j` are equal if and only if they agree at the index `j`.
|
HomologicalComplex.isZero_single_obj_X
theorem HomologicalComplex.isZero_single_obj_X :
∀ {V : Type u} [inst : CategoryTheory.Category.{v, u} V] [inst_1 : CategoryTheory.Limits.HasZeroMorphisms V]
[inst_2 : CategoryTheory.Limits.HasZeroObject V] {ι : Type u_1} [inst_3 : DecidableEq ι] (c : ComplexShape ι)
(j : ι) (A : V) (i : ι), i ≠ j → CategoryTheory.Limits.IsZero (((HomologicalComplex.single V c j).obj A).X i)
This theorem states that for any category `V` with zero morphisms and a zero object, given a `ComplexShape` `c` and objects `j` and `A` of type `ι` and `V` respectively, and another object `i` of type `ι`, if `i` is not equal to `j`, then the object at position `i` of the homological complex obtained by applying the functor `HomologicalComplex.single V c j` to `A` is a zero object in the category. In other words, all objects at positions different from `j` in this homological complex are zero objects.
More concisely: For any category with zero morphisms and a zero object, the homological complex obtained from a `ComplexShape` and an object `A` via `HomologicalComplex.single` has all positions except for the one corresponding to a given object `j` as zero objects.
|
HomologicalComplex.single_map_f_self
theorem HomologicalComplex.single_map_f_self :
∀ {V : Type u} [inst : CategoryTheory.Category.{v, u} V] [inst_1 : CategoryTheory.Limits.HasZeroMorphisms V]
[inst_2 : CategoryTheory.Limits.HasZeroObject V] {ι : Type u_1} [inst_3 : DecidableEq ι] (c : ComplexShape ι)
(j : ι) {A B : V} (f : A ⟶ B),
((HomologicalComplex.single V c j).map f).f j =
CategoryTheory.CategoryStruct.comp (HomologicalComplex.singleObjXSelf c j A).hom
(CategoryTheory.CategoryStruct.comp f (HomologicalComplex.singleObjXSelf c j B).inv)
This theorem states that for any category `V` with zero morphisms and a zero object, given any complex shape `c` and an object `j` in it, if we have a morphism `f` from `A` to `B` where `A` and `B` are objects in `V`, then the morphism at `j` in the image of the homological complex corresponding to `j` under the map induced by `f` is the composition of the morphism from the object at `j` in `A` to itself and the composition of `f` with the inverse of the morphism from the object at `j` in `B` to itself. This theorem is part of the theory of homological algebra and deals with the behaviour of morphisms in homological complexes.
More concisely: Given a category with zero morphisms and a zero object, for any complex and object `j`, the morphism at `j` in the image of the homological complex induced by a morphism `f` from `A` to `B` is equal to the composition of the identity morphism on `j` in `A`, `f`, and the inverse of the identity morphism on `j` in `B`.
|
HomologicalComplex.mkHomFromSingle_f
theorem HomologicalComplex.mkHomFromSingle_f :
∀ {V : Type u} [inst : CategoryTheory.Category.{v, u} V] [inst_1 : CategoryTheory.Limits.HasZeroMorphisms V]
[inst_2 : CategoryTheory.Limits.HasZeroObject V] {ι : Type u_1} [inst_3 : DecidableEq ι] {c : ComplexShape ι}
{K : HomologicalComplex V c} {j : ι} {A : V} (φ : A ⟶ K.X j)
(hφ : ∀ (k : ι), c.Rel j k → CategoryTheory.CategoryStruct.comp φ (K.d j k) = 0),
(HomologicalComplex.mkHomFromSingle φ hφ).f j =
CategoryTheory.CategoryStruct.comp (HomologicalComplex.singleObjXSelf c j A).hom φ
This theorem states that for any category `V` that has zero morphisms and zero objects, given a `HomologicalComplex` `K` indexed by type `ι` with a `ComplexShape` `c`, and an object `j` of type `ι` and another object `A` of the same category `V`, if we have a morphism `φ` from `A` to the `j`-th object of `K`, such that the composition of `φ` with the differential `K.d j k` is zero for any `k` where the relation `c.Rel j k` holds, then the `j`-th morphism of the homological complex constructed from `φ` equals to the composition of the homomorphism from `A` to the `j`-th object in the `HomologicalComplex.singleObjXSelf` (which is a homological complex where all differentials are zero) and `φ`.
More concisely: If `V` is a zero-object and zero-morphism category, for any homological complex `K` and morphism `φ: A → K.object(j)` such that `K.d j k ∘ φ = 0` for all `k` related to `j` in `K`, then the `j`-th morphism of the complex constructed from `φ` equals to `φ` composed with the identity morphism of `K.object(j)` in the homological complex of a single object `K.object(j)` with itself.
|
CochainComplex.single₀_map_f_zero
theorem CochainComplex.single₀_map_f_zero :
∀ {V : Type u} [inst : CategoryTheory.Category.{v, u} V] [inst_1 : CategoryTheory.Limits.HasZeroMorphisms V]
[inst_2 : CategoryTheory.Limits.HasZeroObject V] {A B : V} (f : A ⟶ B),
((CochainComplex.single₀ V).map f).f 0 = f
This theorem states that for any category `V` with zero morphisms and a zero object, given two objects `A` and `B` in `V` and a morphism `f` from `A` to `B`, if we apply the functor `CochainComplex.single₀ V` to the morphism `f` and then apply the morphism function `.f` at degree 0, we obtain the original morphism `f`. In simpler terms, when we map a morphism using the functor that creates a cochain complex supported in degree zero, the morphism at degree zero remains the same in the cochain complex.
More concisely: For any category with zero morphisms and a zero object, the morphism function at degree 0 of the cochain complex created by `CochainComplex.single₀` for a given morphism is equal to the original morphism.
|