Homotopy.map_nullHomotopicMap
theorem Homotopy.map_nullHomotopicMap :
∀ {ι : Type u_1} {V : Type u} [inst : CategoryTheory.Category.{v, u} V] [inst_1 : CategoryTheory.Preadditive V]
{c : ComplexShape ι} {C D : HomologicalComplex V c} {W : Type u_2} [inst_2 : CategoryTheory.Category.{u_3, u_2} W]
[inst_3 : CategoryTheory.Preadditive W] (G : CategoryTheory.Functor V W) [inst_4 : G.Additive]
(hom : (i j : ι) → C.X i ⟶ D.X j),
(G.mapHomologicalComplex c).map (Homotopy.nullHomotopicMap hom) =
Homotopy.nullHomotopicMap fun i j => G.map (hom i j)
The theorem `Homotopy.map_nullHomotopicMap` states that for any types `ι`, `V`, and `W`, given categories `V` and `W` with preadditive structures, a complex shape `c`, two homological complexes `C` and `D` over `V` with shape `c`, an additive functor `G` from `V` to `W`, and a family of morphisms `hom` from objects in `C` to objects in `D` indexed by `ι`, the homotopy of the null-homotopic map of `hom` after applying the functor `G` is equal to the null-homotopic map of the functors applied to `hom`. In simpler terms, this theorem states that applying an additive functor to a null-homotopic map preserves the property of being null-homotopic.
More concisely: Given categories `V` and `W` with preadditive structures, an additive functor `G` from `V` to `W`, a complex shape `c`, homological complexes `C` and `D` over `V` with shape `c`, a null-homotopic family of morphisms `hom` from `C` to `D` indexed by `ι`, the null-homotopy of `G(hom)` is equal to `G(null-homotopy(hom))`.
|
Homotopy.nullHomotopicMap'_comp
theorem Homotopy.nullHomotopicMap'_comp :
∀ {ι : Type u_1} {V : Type u} [inst : CategoryTheory.Category.{v, u} V] [inst_1 : CategoryTheory.Preadditive V]
{c : ComplexShape ι} {C D E : HomologicalComplex V c} (hom : (i j : ι) → c.Rel j i → (C.X i ⟶ D.X j)) (g : D ⟶ E),
CategoryTheory.CategoryStruct.comp (Homotopy.nullHomotopicMap' hom) g =
Homotopy.nullHomotopicMap' fun i j hij => CategoryTheory.CategoryStruct.comp (hom i j hij) (g.f j)
The theorem `Homotopy.nullHomotopicMap'_comp` states that, given a category `V` with pre-additive structure, a complex shape `c`, homological complexes `C`, `D`, and `E` over `V` with shape `c`, a function `hom` that assigns a morphism from `C.X i` to `D.X j` for each pair `(i, j)` such that `c.Rel j i` holds, and a morphism `g` from `D` to `E`, the composition of the map produced by `Homotopy.nullHomotopicMap'` applied to `hom` with `g` is equal to the map produced by `Homotopy.nullHomotopicMap'` applied to the function that assigns the composition of the morphism `hom i j hij` with `g.f j` to each pair `(i, j)` with `c.Rel j i`. This theorem captures a compatibility requirement for the function `Homotopy.nullHomotopicMap'` in relation to the composition operation in the category.
More concisely: Given a pre-additive category `V` with complex shapes `C`, `D`, and `E` over `V` with shape `c`, a morphism function `hom` from `C` to `D`, and a morphism `g` from `D` to `E`, the composition of `Homotopy.nullHomotopicMap'` of `hom` with `g` equals `Homotopy.nullHomotopicMap'` of the composition of `hom` with `g` on pairs `(i, j)` with `c.Rel j i`.
|
Homotopy.homologyMap_eq
theorem Homotopy.homologyMap_eq :
∀ {C : Type u_2} [inst : CategoryTheory.Category.{u_4, u_2} C] [inst_1 : CategoryTheory.Preadditive C]
{ι : Type u_3} {c : ComplexShape ι} [inst_2 : DecidableRel c.Rel] {K L : HomologicalComplex C c} {f g : K ⟶ L},
Homotopy f g →
∀ (i : ι) [inst_3 : K.HasHomology i] [inst_4 : L.HasHomology i],
HomologicalComplex.homologyMap f i = HomologicalComplex.homologyMap g i
The theorem `Homotopy.homologyMap_eq` states that for any two homological complexes `K` and `L` in a category `C` with a complex shape `c`, if there exists a homotopy between two chain maps `f` and `g` from `K` to `L`, then for any degree `i` where `K` and `L` both have homology, the homology map of `f` at degree `i` is equal to the homology map of `g` at degree `i`. This theorem demonstrates the invariance of the homology maps under homotopy.
More concisely: If two chain maps between complexes in a category with homology have a homotopy between them, then they have equal homology maps for all degrees where both complexes have homology.
|
homology'_map_eq_of_homotopy
theorem homology'_map_eq_of_homotopy :
∀ {ι : Type u_1} {V : Type u} [inst : CategoryTheory.Category.{v, u} V] [inst_1 : CategoryTheory.Preadditive V]
{c : ComplexShape ι} {C D : HomologicalComplex V c} {f g : C ⟶ D} [inst_2 : CategoryTheory.Limits.HasEqualizers V]
[inst_3 : CategoryTheory.Limits.HasCokernels V] [inst_4 : CategoryTheory.Limits.HasImages V]
[inst_5 : CategoryTheory.Limits.HasImageMaps V],
Homotopy f g → ∀ (i : ι), (homology'Functor V c i).map f = (homology'Functor V c i).map g
This theorem states that if two morphisms (`f` and `g`) between two homological complexes (`C` and `D`) in a category `V` are homotopic, then they induce the same map on homology for any indexing type `ι`. This holds under the conditions that the category `V` is preadditive, has equalizers, cokernels, images, and image maps. In simpler terms, the homology of two homotopic morphisms in a suitable category will be equal.
More concisely: If `f` and `g` are homotopic morphisms between homological complexes `C` and `D` in a preadditive category `V` with equalizers, cokernels, images, and image maps, then they induce equal homology maps for any indexing type `ι`.
|
Homotopy.map_nullHomotopicMap'
theorem Homotopy.map_nullHomotopicMap' :
∀ {ι : Type u_1} {V : Type u} [inst : CategoryTheory.Category.{v, u} V] [inst_1 : CategoryTheory.Preadditive V]
{c : ComplexShape ι} {C D : HomologicalComplex V c} {W : Type u_2} [inst_2 : CategoryTheory.Category.{u_3, u_2} W]
[inst_3 : CategoryTheory.Preadditive W] (G : CategoryTheory.Functor V W) [inst_4 : G.Additive]
(hom : (i j : ι) → c.Rel j i → (C.X i ⟶ D.X j)),
(G.mapHomologicalComplex c).map (Homotopy.nullHomotopicMap' hom) =
Homotopy.nullHomotopicMap' fun i j hij => G.map (hom i j hij)
This theorem, `Homotopy.map_nullHomotopicMap'`, states the compatibility of the function `nullHomotopicMap'` with the application of additive functors. Specifically, given a type `ι`, a category `V` which has a preadditive structure, a complex shape `c`, and two homological complexes `C` and `D` in `V`, along with another category `W` (also preadditive) and a functor `G` from `V` to `W` which is additive, and a function `hom` that maps indices `i` and `j` (where `c.Rel j i` is true) to a morphism from `C.X i` to `D.X j`, the functor `G` applied to the `Homotopy.nullHomotopicMap'` of `hom` is equal to the `Homotopy.nullHomotopicMap'` of the functor `G` applied to `hom`. This means that it preserves the null homotopic maps across categories.
More concisely: Given functors `G: V -> W` between preadditive categories, additive homomorphisms `hom: c.Rel -> Hom(C, D)`, and a nullhomotopic map `H: Homotopy.nullHomotopicMap' hom`, the application of `G` to `H` is equal to `Homotopy.nullHomotopicMap' (G ∘ hom)`.
|
Homotopy.comp_nullHomotopicMap
theorem Homotopy.comp_nullHomotopicMap :
∀ {ι : Type u_1} {V : Type u} [inst : CategoryTheory.Category.{v, u} V] [inst_1 : CategoryTheory.Preadditive V]
{c : ComplexShape ι} {C D E : HomologicalComplex V c} (f : C ⟶ D) (hom : (i j : ι) → D.X i ⟶ E.X j),
CategoryTheory.CategoryStruct.comp f (Homotopy.nullHomotopicMap hom) =
Homotopy.nullHomotopicMap fun i j => CategoryTheory.CategoryStruct.comp (f.f i) (hom i j)
This theorem, named `Homotopy.comp_nullHomotopicMap`, states that for any given category `V` that is Preadditive, and any `ComplexShape` `c` with homological complexes `C`, `D`, and `E`, the composition of a morphism `f` from `C` to `D` and the `nullHomotopicMap` corresponding to a function `hom` mapping pairs `(i, j)` from `ι` to morphisms from `D.X i` to `E.X j`, is equal to the `nullHomotopicMap` defined by the function that maps each pair `(i, j)` from `ι` to the composition of the morphism `f.f i` and the morphism `hom i j`. In other words, the process of precomposing a `nullHomotopicMap` with a morphism is compatible with defining a `nullHomotopicMap` by precomposing each of its constituent morphisms with that morphism.
More concisely: For any preadditive category `V` and complex shapes `c` with homological complexes `C`, `D`, and `E`, the composition of a morphism `f` from `C` to `D` with the `nullHomotopicMap` defined by a function `hom` is equal to the `nullHomotopicMap` defined by the function that maps each pair `(i, j)` to the composition of `f.f i` and `hom i j`.
|
Homotopy.comp_nullHomotopicMap'
theorem Homotopy.comp_nullHomotopicMap' :
∀ {ι : Type u_1} {V : Type u} [inst : CategoryTheory.Category.{v, u} V] [inst_1 : CategoryTheory.Preadditive V]
{c : ComplexShape ι} {C D E : HomologicalComplex V c} (f : C ⟶ D) (hom : (i j : ι) → c.Rel j i → (D.X i ⟶ E.X j)),
CategoryTheory.CategoryStruct.comp f (Homotopy.nullHomotopicMap' hom) =
Homotopy.nullHomotopicMap' fun i j hij => CategoryTheory.CategoryStruct.comp (f.f i) (hom i j hij)
The theorem `Homotopy.comp_nullHomotopicMap'` states that for any types `ι` and `V`, given a category structure and preadditive structure on `V`, a complex shape `c`, and homological complexes `C`, `D`, and `E` over `V` with shape `c`, if we have a morphism `f` from `C` to `D` and a map `hom` from `D` to `E` that is null-homotopic with respect to `c`, then the composition of `f` with the null-homotopic map induced by `hom` is itself a null-homotopic map. This new null-homotopic map is defined for any `i` and `j` in `ι` such that `c.Rel j i` holds, and is given by the composition of the `i`th component of `f` with `hom i j`. In other words, null-homotopic maps are compatible with the composition of morphisms in the category.
More concisely: Given complexes `C`, `D`, and `E` over a preadditive category `V` with shape `c`, if `f: C → D` is a morphism and `hom: D → E` is a null-homotopic map, then the composition `f ∘ hom` is a null-homotopic map with components `(f ∘ hom)(i, j) = f(i)(hom(i, j))` for `i, j` in `ι` with `c.Rel j i`.
|
Homotopy.nullHomotopicMap_comp
theorem Homotopy.nullHomotopicMap_comp :
∀ {ι : Type u_1} {V : Type u} [inst : CategoryTheory.Category.{v, u} V] [inst_1 : CategoryTheory.Preadditive V]
{c : ComplexShape ι} {C D E : HomologicalComplex V c} (hom : (i j : ι) → C.X i ⟶ D.X j) (g : D ⟶ E),
CategoryTheory.CategoryStruct.comp (Homotopy.nullHomotopicMap hom) g =
Homotopy.nullHomotopicMap fun i j => CategoryTheory.CategoryStruct.comp (hom i j) (g.f j)
The theorem `Homotopy.nullHomotopicMap_comp` states that for any category `V` that is preadditive, and given a complex shape `c`, homological complexes `C`, `D`, and `E`, a set of morphisms `hom` between `C` and `D`, and a morphism `g` from `D` to `E`, the composition of the `nullHomotopicMap` constructed using `hom` and the morphism `g` is equal to the `nullHomotopicMap` constructed using the composition of `hom` and `g.f`. In other words, the `nullHomotopicMap` is compatible with postcomposition by a morphism of complexes.
More concisely: For any preadditive category V, complex shapes c, and morphisms hom : C -> D, g : D -> E in homological complexes C, D, and E respectively, the null homotopic maps constructed using hom and g are equal to the null homotopic map constructed using the composition of hom and g.
|