Homology is an additive functor #
When V is preadditive, HomologicalComplex V c is also preadditive,
and homologyFunctor is additive.
TODO: similarly for R-linear.
instance
HomologicalComplex.instZeroHomHomologicalComplexPreadditiveHasZeroMorphismsToQuiverToCategoryStructInstCategoryHomologicalComplex
{ι : Type u_1}
{V : Type u}
[CategoryTheory.Category.{v, u} V]
[CategoryTheory.Preadditive V]
{c : ComplexShape ι}
{C : HomologicalComplex V c}
{D : HomologicalComplex V c}
:
instance
HomologicalComplex.instAddHomHomologicalComplexPreadditiveHasZeroMorphismsToQuiverToCategoryStructInstCategoryHomologicalComplex
{ι : Type u_1}
{V : Type u}
[CategoryTheory.Category.{v, u} V]
[CategoryTheory.Preadditive V]
{c : ComplexShape ι}
{C : HomologicalComplex V c}
{D : HomologicalComplex V c}
:
instance
HomologicalComplex.instNegHomHomologicalComplexPreadditiveHasZeroMorphismsToQuiverToCategoryStructInstCategoryHomologicalComplex
{ι : Type u_1}
{V : Type u}
[CategoryTheory.Category.{v, u} V]
[CategoryTheory.Preadditive V]
{c : ComplexShape ι}
{C : HomologicalComplex V c}
{D : HomologicalComplex V c}
:
instance
HomologicalComplex.instSubHomHomologicalComplexPreadditiveHasZeroMorphismsToQuiverToCategoryStructInstCategoryHomologicalComplex
{ι : Type u_1}
{V : Type u}
[CategoryTheory.Category.{v, u} V]
[CategoryTheory.Preadditive V]
{c : ComplexShape ι}
{C : HomologicalComplex V c}
{D : HomologicalComplex V c}
:
instance
HomologicalComplex.hasNatScalar
{ι : Type u_1}
{V : Type u}
[CategoryTheory.Category.{v, u} V]
[CategoryTheory.Preadditive V]
{c : ComplexShape ι}
{C : HomologicalComplex V c}
{D : HomologicalComplex V c}
:
instance
HomologicalComplex.hasIntScalar
{ι : Type u_1}
{V : Type u}
[CategoryTheory.Category.{v, u} V]
[CategoryTheory.Preadditive V]
{c : ComplexShape ι}
{C : HomologicalComplex V c}
{D : HomologicalComplex V c}
:
@[simp]
theorem
HomologicalComplex.zero_f_apply
{ι : Type u_1}
{V : Type u}
[CategoryTheory.Category.{v, u} V]
[CategoryTheory.Preadditive V]
{c : ComplexShape ι}
{C : HomologicalComplex V c}
{D : HomologicalComplex V c}
(i : ι)
:
HomologicalComplex.Hom.f 0 i = 0
@[simp]
theorem
HomologicalComplex.add_f_apply
{ι : Type u_1}
{V : Type u}
[CategoryTheory.Category.{v, u} V]
[CategoryTheory.Preadditive V]
{c : ComplexShape ι}
{C : HomologicalComplex V c}
{D : HomologicalComplex V c}
(f : C ⟶ D)
(g : C ⟶ D)
(i : ι)
:
HomologicalComplex.Hom.f (f + g) i = HomologicalComplex.Hom.f f i + HomologicalComplex.Hom.f g i
@[simp]
theorem
HomologicalComplex.neg_f_apply
{ι : Type u_1}
{V : Type u}
[CategoryTheory.Category.{v, u} V]
[CategoryTheory.Preadditive V]
{c : ComplexShape ι}
{C : HomologicalComplex V c}
{D : HomologicalComplex V c}
(f : C ⟶ D)
(i : ι)
:
@[simp]
theorem
HomologicalComplex.sub_f_apply
{ι : Type u_1}
{V : Type u}
[CategoryTheory.Category.{v, u} V]
[CategoryTheory.Preadditive V]
{c : ComplexShape ι}
{C : HomologicalComplex V c}
{D : HomologicalComplex V c}
(f : C ⟶ D)
(g : C ⟶ D)
(i : ι)
:
HomologicalComplex.Hom.f (f - g) i = HomologicalComplex.Hom.f f i - HomologicalComplex.Hom.f g i
@[simp]
theorem
HomologicalComplex.nsmul_f_apply
{ι : Type u_1}
{V : Type u}
[CategoryTheory.Category.{v, u} V]
[CategoryTheory.Preadditive V]
{c : ComplexShape ι}
{C : HomologicalComplex V c}
{D : HomologicalComplex V c}
(n : ℕ)
(f : C ⟶ D)
(i : ι)
:
HomologicalComplex.Hom.f (n • f) i = n • HomologicalComplex.Hom.f f i
@[simp]
theorem
HomologicalComplex.zsmul_f_apply
{ι : Type u_1}
{V : Type u}
[CategoryTheory.Category.{v, u} V]
[CategoryTheory.Preadditive V]
{c : ComplexShape ι}
{C : HomologicalComplex V c}
{D : HomologicalComplex V c}
(n : ℤ)
(f : C ⟶ D)
(i : ι)
:
HomologicalComplex.Hom.f (n • f) i = n • HomologicalComplex.Hom.f f i
instance
HomologicalComplex.instAddCommGroupHomHomologicalComplexPreadditiveHasZeroMorphismsToQuiverToCategoryStructInstCategoryHomologicalComplex
{ι : Type u_1}
{V : Type u}
[CategoryTheory.Category.{v, u} V]
[CategoryTheory.Preadditive V]
{c : ComplexShape ι}
{C : HomologicalComplex V c}
{D : HomologicalComplex V c}
:
AddCommGroup (C ⟶ D)
@[simp]
theorem
HomologicalComplex.Hom.fAddMonoidHom_apply
{ι : Type u_1}
{V : Type u}
[CategoryTheory.Category.{v, u} V]
[CategoryTheory.Preadditive V]
{c : ComplexShape ι}
{C₁ : HomologicalComplex V c}
{C₂ : HomologicalComplex V c}
(i : ι)
(f : C₁ ⟶ C₂)
:
def
HomologicalComplex.Hom.fAddMonoidHom
{ι : Type u_1}
{V : Type u}
[CategoryTheory.Category.{v, u} V]
[CategoryTheory.Preadditive V]
{c : ComplexShape ι}
{C₁ : HomologicalComplex V c}
{C₂ : HomologicalComplex V c}
(i : ι)
:
(C₁ ⟶ C₂) →+ (HomologicalComplex.X C₁ i ⟶ HomologicalComplex.X C₂ i)
The i-th component of a chain map, as an additive map from chain maps to morphisms.
Instances For
instance
HomologicalComplex.eval_additive
{ι : Type u_1}
{V : Type u}
[CategoryTheory.Category.{v, u} V]
[CategoryTheory.Preadditive V]
{c : ComplexShape ι}
(i : ι)
:
instance
HomologicalComplex.cycles_additive
{ι : Type u_1}
{V : Type u}
[CategoryTheory.Category.{v, u} V]
[CategoryTheory.Preadditive V]
{c : ComplexShape ι}
(i : ι)
[CategoryTheory.Limits.HasEqualizers V]
:
instance
HomologicalComplex.boundaries_additive
{ι : Type u_1}
{V : Type u}
[CategoryTheory.Category.{v, u} V]
[CategoryTheory.Preadditive V]
{c : ComplexShape ι}
(i : ι)
[CategoryTheory.Limits.HasImages V]
[CategoryTheory.Limits.HasImageMaps V]
:
instance
HomologicalComplex.homology_additive
{ι : Type u_1}
{V : Type u}
[CategoryTheory.Category.{v, u} V]
[CategoryTheory.Preadditive V]
{c : ComplexShape ι}
(i : ι)
[CategoryTheory.Limits.HasImages V]
[CategoryTheory.Limits.HasImageMaps V]
[CategoryTheory.Limits.HasEqualizers V]
[CategoryTheory.Limits.HasCokernels V]
:
@[simp]
theorem
CategoryTheory.Functor.mapHomologicalComplex_obj_d
{ι : Type u_1}
{V : Type u}
[CategoryTheory.Category.{v, u} V]
[CategoryTheory.Preadditive V]
{W : Type u_2}
[CategoryTheory.Category.{u_3, u_2} W]
[CategoryTheory.Preadditive W]
(F : CategoryTheory.Functor V W)
[CategoryTheory.Functor.Additive F]
(c : ComplexShape ι)
(C : HomologicalComplex V c)
(i : ι)
(j : ι)
:
HomologicalComplex.d ((CategoryTheory.Functor.mapHomologicalComplex F c).obj C) i j = F.map (HomologicalComplex.d C i j)
@[simp]
theorem
CategoryTheory.Functor.mapHomologicalComplex_map_f
{ι : Type u_1}
{V : Type u}
[CategoryTheory.Category.{v, u} V]
[CategoryTheory.Preadditive V]
{W : Type u_2}
[CategoryTheory.Category.{u_3, u_2} W]
[CategoryTheory.Preadditive W]
(F : CategoryTheory.Functor V W)
[CategoryTheory.Functor.Additive F]
(c : ComplexShape ι)
:
∀ {X Y : HomologicalComplex V c} (f : X ⟶ Y) (i : ι),
HomologicalComplex.Hom.f ((CategoryTheory.Functor.mapHomologicalComplex F c).map f) i = F.map (HomologicalComplex.Hom.f f i)
@[simp]
theorem
CategoryTheory.Functor.mapHomologicalComplex_obj_X
{ι : Type u_1}
{V : Type u}
[CategoryTheory.Category.{v, u} V]
[CategoryTheory.Preadditive V]
{W : Type u_2}
[CategoryTheory.Category.{u_3, u_2} W]
[CategoryTheory.Preadditive W]
(F : CategoryTheory.Functor V W)
[CategoryTheory.Functor.Additive F]
(c : ComplexShape ι)
(C : HomologicalComplex V c)
(i : ι)
:
HomologicalComplex.X ((CategoryTheory.Functor.mapHomologicalComplex F c).obj C) i = F.obj (HomologicalComplex.X C i)
def
CategoryTheory.Functor.mapHomologicalComplex
{ι : Type u_1}
{V : Type u}
[CategoryTheory.Category.{v, u} V]
[CategoryTheory.Preadditive V]
{W : Type u_2}
[CategoryTheory.Category.{u_3, u_2} W]
[CategoryTheory.Preadditive W]
(F : CategoryTheory.Functor V W)
[CategoryTheory.Functor.Additive F]
(c : ComplexShape ι)
:
An additive functor induces a functor between homological complexes. This is sometimes called the "prolongation".
Instances For
@[simp]
theorem
CategoryTheory.Functor.mapHomologicalComplexIdIso_inv_app_f
{ι : Type u_1}
(V : Type u)
[CategoryTheory.Category.{v, u} V]
[CategoryTheory.Preadditive V]
(c : ComplexShape ι)
(X : HomologicalComplex V c)
(i : ι)
:
@[simp]
theorem
CategoryTheory.Functor.mapHomologicalComplexIdIso_hom_app_f
{ι : Type u_1}
(V : Type u)
[CategoryTheory.Category.{v, u} V]
[CategoryTheory.Preadditive V]
(c : ComplexShape ι)
(X : HomologicalComplex V c)
(i : ι)
:
def
CategoryTheory.Functor.mapHomologicalComplexIdIso
{ι : Type u_1}
(V : Type u)
[CategoryTheory.Category.{v, u} V]
[CategoryTheory.Preadditive V]
(c : ComplexShape ι)
:
The functor on homological complexes induced by the identity functor is isomorphic to the identity functor.
Instances For
instance
CategoryTheory.Functor.map_homogical_complex_additive
{ι : Type u_1}
{V : Type u}
[CategoryTheory.Category.{v, u} V]
[CategoryTheory.Preadditive V]
{W : Type u_2}
[CategoryTheory.Category.{u_3, u_2} W]
[CategoryTheory.Preadditive W]
(F : CategoryTheory.Functor V W)
[CategoryTheory.Functor.Additive F]
(c : ComplexShape ι)
:
instance
CategoryTheory.Functor.mapHomologicalComplex_reflects_iso
{ι : Type u_1}
{V : Type u}
[CategoryTheory.Category.{v, u} V]
[CategoryTheory.Preadditive V]
{W : Type u_2}
[CategoryTheory.Category.{u_3, u_2} W]
[CategoryTheory.Preadditive W]
(F : CategoryTheory.Functor V W)
[CategoryTheory.Functor.Additive F]
[CategoryTheory.ReflectsIsomorphisms F]
(c : ComplexShape ι)
:
@[simp]
theorem
CategoryTheory.NatTrans.mapHomologicalComplex_app_f
{ι : Type u_1}
{V : Type u}
[CategoryTheory.Category.{v, u} V]
[CategoryTheory.Preadditive V]
{W : Type u_2}
[CategoryTheory.Category.{u_3, u_2} W]
[CategoryTheory.Preadditive W]
{F : CategoryTheory.Functor V W}
{G : CategoryTheory.Functor V W}
[CategoryTheory.Functor.Additive F]
[CategoryTheory.Functor.Additive G]
(α : F ⟶ G)
(c : ComplexShape ι)
(C : HomologicalComplex V c)
(i : ι)
:
HomologicalComplex.Hom.f ((CategoryTheory.NatTrans.mapHomologicalComplex α c).app C) i = α.app (HomologicalComplex.X C i)
def
CategoryTheory.NatTrans.mapHomologicalComplex
{ι : Type u_1}
{V : Type u}
[CategoryTheory.Category.{v, u} V]
[CategoryTheory.Preadditive V]
{W : Type u_2}
[CategoryTheory.Category.{u_3, u_2} W]
[CategoryTheory.Preadditive W]
{F : CategoryTheory.Functor V W}
{G : CategoryTheory.Functor V W}
[CategoryTheory.Functor.Additive F]
[CategoryTheory.Functor.Additive G]
(α : F ⟶ G)
(c : ComplexShape ι)
:
A natural transformation between functors induces a natural transformation between those functors applied to homological complexes.
Instances For
@[simp]
theorem
CategoryTheory.NatTrans.mapHomologicalComplex_id
{ι : Type u_1}
{V : Type u}
[CategoryTheory.Category.{v, u} V]
[CategoryTheory.Preadditive V]
{W : Type u_2}
[CategoryTheory.Category.{u_3, u_2} W]
[CategoryTheory.Preadditive W]
(c : ComplexShape ι)
(F : CategoryTheory.Functor V W)
[CategoryTheory.Functor.Additive F]
:
@[simp]
theorem
CategoryTheory.NatTrans.mapHomologicalComplex_comp
{ι : Type u_1}
{V : Type u}
[CategoryTheory.Category.{v, u} V]
[CategoryTheory.Preadditive V]
{W : Type u_2}
[CategoryTheory.Category.{u_3, u_2} W]
[CategoryTheory.Preadditive W]
(c : ComplexShape ι)
{F : CategoryTheory.Functor V W}
{G : CategoryTheory.Functor V W}
{H : CategoryTheory.Functor V W}
[CategoryTheory.Functor.Additive F]
[CategoryTheory.Functor.Additive G]
[CategoryTheory.Functor.Additive H]
(α : F ⟶ G)
(β : G ⟶ H)
:
@[simp]
theorem
CategoryTheory.NatTrans.mapHomologicalComplex_naturality_assoc
{ι : Type u_1}
{V : Type u}
[CategoryTheory.Category.{v, u} V]
[CategoryTheory.Preadditive V]
{W : Type u_2}
[CategoryTheory.Category.{u_3, u_2} W]
[CategoryTheory.Preadditive W]
{c : ComplexShape ι}
{F : CategoryTheory.Functor V W}
{G : CategoryTheory.Functor V W}
[CategoryTheory.Functor.Additive F]
[CategoryTheory.Functor.Additive G]
(α : F ⟶ G)
{C : HomologicalComplex V c}
{D : HomologicalComplex V c}
(f : C ⟶ D)
{Z : HomologicalComplex W c}
(h : (CategoryTheory.Functor.mapHomologicalComplex G c).obj D ⟶ Z)
:
CategoryTheory.CategoryStruct.comp ((CategoryTheory.Functor.mapHomologicalComplex F c).map f)
(CategoryTheory.CategoryStruct.comp ((CategoryTheory.NatTrans.mapHomologicalComplex α c).app D) h) = CategoryTheory.CategoryStruct.comp ((CategoryTheory.NatTrans.mapHomologicalComplex α c).app C)
(CategoryTheory.CategoryStruct.comp ((CategoryTheory.Functor.mapHomologicalComplex G c).map f) h)
@[simp]
theorem
CategoryTheory.NatTrans.mapHomologicalComplex_naturality
{ι : Type u_1}
{V : Type u}
[CategoryTheory.Category.{v, u} V]
[CategoryTheory.Preadditive V]
{W : Type u_2}
[CategoryTheory.Category.{u_3, u_2} W]
[CategoryTheory.Preadditive W]
{c : ComplexShape ι}
{F : CategoryTheory.Functor V W}
{G : CategoryTheory.Functor V W}
[CategoryTheory.Functor.Additive F]
[CategoryTheory.Functor.Additive G]
(α : F ⟶ G)
{C : HomologicalComplex V c}
{D : HomologicalComplex V c}
(f : C ⟶ D)
:
CategoryTheory.CategoryStruct.comp ((CategoryTheory.Functor.mapHomologicalComplex F c).map f)
((CategoryTheory.NatTrans.mapHomologicalComplex α c).app D) = CategoryTheory.CategoryStruct.comp ((CategoryTheory.NatTrans.mapHomologicalComplex α c).app C)
((CategoryTheory.Functor.mapHomologicalComplex G c).map f)
@[simp]
theorem
CategoryTheory.NatIso.mapHomologicalComplex_hom_app_f
{ι : Type u_1}
{V : Type u}
[CategoryTheory.Category.{v, u} V]
[CategoryTheory.Preadditive V]
{W : Type u_2}
[CategoryTheory.Category.{u_3, u_2} W]
[CategoryTheory.Preadditive W]
{F : CategoryTheory.Functor V W}
{G : CategoryTheory.Functor V W}
[CategoryTheory.Functor.Additive F]
[CategoryTheory.Functor.Additive G]
(α : F ≅ G)
(c : ComplexShape ι)
(C : HomologicalComplex V c)
(i : ι)
:
HomologicalComplex.Hom.f ((CategoryTheory.NatIso.mapHomologicalComplex α c).hom.app C) i = α.hom.app (HomologicalComplex.X C i)
@[simp]
theorem
CategoryTheory.NatIso.mapHomologicalComplex_inv_app_f
{ι : Type u_1}
{V : Type u}
[CategoryTheory.Category.{v, u} V]
[CategoryTheory.Preadditive V]
{W : Type u_2}
[CategoryTheory.Category.{u_3, u_2} W]
[CategoryTheory.Preadditive W]
{F : CategoryTheory.Functor V W}
{G : CategoryTheory.Functor V W}
[CategoryTheory.Functor.Additive F]
[CategoryTheory.Functor.Additive G]
(α : F ≅ G)
(c : ComplexShape ι)
(C : HomologicalComplex V c)
(i : ι)
:
HomologicalComplex.Hom.f ((CategoryTheory.NatIso.mapHomologicalComplex α c).inv.app C) i = α.inv.app (HomologicalComplex.X C i)
def
CategoryTheory.NatIso.mapHomologicalComplex
{ι : Type u_1}
{V : Type u}
[CategoryTheory.Category.{v, u} V]
[CategoryTheory.Preadditive V]
{W : Type u_2}
[CategoryTheory.Category.{u_3, u_2} W]
[CategoryTheory.Preadditive W]
{F : CategoryTheory.Functor V W}
{G : CategoryTheory.Functor V W}
[CategoryTheory.Functor.Additive F]
[CategoryTheory.Functor.Additive G]
(α : F ≅ G)
(c : ComplexShape ι)
:
A natural isomorphism between functors induces a natural isomorphism between those functors applied to homological complexes.
Instances For
@[simp]
theorem
CategoryTheory.Equivalence.mapHomologicalComplex_inverse
{ι : Type u_1}
{V : Type u}
[CategoryTheory.Category.{v, u} V]
[CategoryTheory.Preadditive V]
{W : Type u_2}
[CategoryTheory.Category.{u_3, u_2} W]
[CategoryTheory.Preadditive W]
(e : V ≌ W)
[CategoryTheory.Functor.Additive e.functor]
(c : ComplexShape ι)
:
(CategoryTheory.Equivalence.mapHomologicalComplex e c).inverse = CategoryTheory.Functor.mapHomologicalComplex e.inverse c
@[simp]
theorem
CategoryTheory.Equivalence.mapHomologicalComplex_functor
{ι : Type u_1}
{V : Type u}
[CategoryTheory.Category.{v, u} V]
[CategoryTheory.Preadditive V]
{W : Type u_2}
[CategoryTheory.Category.{u_3, u_2} W]
[CategoryTheory.Preadditive W]
(e : V ≌ W)
[CategoryTheory.Functor.Additive e.functor]
(c : ComplexShape ι)
:
(CategoryTheory.Equivalence.mapHomologicalComplex e c).functor = CategoryTheory.Functor.mapHomologicalComplex e.functor c
@[simp]
theorem
CategoryTheory.Equivalence.mapHomologicalComplex_unitIso
{ι : Type u_1}
{V : Type u}
[CategoryTheory.Category.{v, u} V]
[CategoryTheory.Preadditive V]
{W : Type u_2}
[CategoryTheory.Category.{u_3, u_2} W]
[CategoryTheory.Preadditive W]
(e : V ≌ W)
[CategoryTheory.Functor.Additive e.functor]
(c : ComplexShape ι)
:
(CategoryTheory.Equivalence.mapHomologicalComplex e c).unitIso = (CategoryTheory.Functor.mapHomologicalComplexIdIso V c).symm ≪≫ CategoryTheory.NatIso.mapHomologicalComplex e.unitIso c
@[simp]
theorem
CategoryTheory.Equivalence.mapHomologicalComplex_counitIso
{ι : Type u_1}
{V : Type u}
[CategoryTheory.Category.{v, u} V]
[CategoryTheory.Preadditive V]
{W : Type u_2}
[CategoryTheory.Category.{u_3, u_2} W]
[CategoryTheory.Preadditive W]
(e : V ≌ W)
[CategoryTheory.Functor.Additive e.functor]
(c : ComplexShape ι)
:
(CategoryTheory.Equivalence.mapHomologicalComplex e c).counitIso = CategoryTheory.NatIso.mapHomologicalComplex e.counitIso c ≪≫ CategoryTheory.Functor.mapHomologicalComplexIdIso W c
def
CategoryTheory.Equivalence.mapHomologicalComplex
{ι : Type u_1}
{V : Type u}
[CategoryTheory.Category.{v, u} V]
[CategoryTheory.Preadditive V]
{W : Type u_2}
[CategoryTheory.Category.{u_3, u_2} W]
[CategoryTheory.Preadditive W]
(e : V ≌ W)
[CategoryTheory.Functor.Additive e.functor]
(c : ComplexShape ι)
:
HomologicalComplex V c ≌ HomologicalComplex W c
An equivalence of categories induces an equivalences between the respective categories of homological complex.
Instances For
theorem
ChainComplex.map_chain_complex_of
{V : Type u}
[CategoryTheory.Category.{v, u} V]
[CategoryTheory.Preadditive V]
{W : Type u_2}
[CategoryTheory.Category.{u_4, u_2} W]
[CategoryTheory.Preadditive W]
{α : Type u_3}
[AddRightCancelSemigroup α]
[One α]
[DecidableEq α]
(F : CategoryTheory.Functor V W)
[CategoryTheory.Functor.Additive F]
(X : α → V)
(d : (n : α) → X (n + 1) ⟶ X n)
(sq : ∀ (n : α), CategoryTheory.CategoryStruct.comp (d (n + 1)) (d n) = 0)
:
(CategoryTheory.Functor.mapHomologicalComplex F (ComplexShape.down α)).obj (ChainComplex.of X d sq) = ChainComplex.of (fun n => F.obj (X n)) (fun n => F.map (d n))
(_ : ∀ (n : α), CategoryTheory.CategoryStruct.comp ((fun n => F.map (d n)) (n + 1)) ((fun n => F.map (d n)) n) = 0)
def
HomologicalComplex.singleMapHomologicalComplex
{ι : Type u_1}
{V : Type u}
[CategoryTheory.Category.{v, u} V]
[CategoryTheory.Preadditive V]
[CategoryTheory.Limits.HasZeroObject V]
{W : Type u_2}
[CategoryTheory.Category.{u_3, u_2} W]
[CategoryTheory.Preadditive W]
[CategoryTheory.Limits.HasZeroObject W]
(F : CategoryTheory.Functor V W)
[CategoryTheory.Functor.Additive F]
(c : ComplexShape ι)
(j : ι)
:
Turning an object into a complex supported at j then applying a functor is
the same as applying the functor then forming the complex.
Instances For
@[simp]
theorem
HomologicalComplex.singleMapHomologicalComplex_hom_app_self
{ι : Type u_1}
{V : Type u}
[CategoryTheory.Category.{v, u} V]
[CategoryTheory.Preadditive V]
(c : ComplexShape ι)
[CategoryTheory.Limits.HasZeroObject V]
{W : Type u_2}
[CategoryTheory.Category.{u_3, u_2} W]
[CategoryTheory.Preadditive W]
[CategoryTheory.Limits.HasZeroObject W]
(F : CategoryTheory.Functor V W)
[CategoryTheory.Functor.Additive F]
(j : ι)
(X : V)
:
HomologicalComplex.Hom.f ((HomologicalComplex.singleMapHomologicalComplex F c j).hom.app X) j = CategoryTheory.eqToHom (_ : F.obj (if j = j then X else 0) = if j = j then F.obj X else 0)
@[simp]
theorem
HomologicalComplex.singleMapHomologicalComplex_hom_app_ne
{ι : Type u_1}
{V : Type u}
[CategoryTheory.Category.{v, u} V]
[CategoryTheory.Preadditive V]
(c : ComplexShape ι)
[CategoryTheory.Limits.HasZeroObject V]
{W : Type u_2}
[CategoryTheory.Category.{u_3, u_2} W]
[CategoryTheory.Preadditive W]
[CategoryTheory.Limits.HasZeroObject W]
(F : CategoryTheory.Functor V W)
[CategoryTheory.Functor.Additive F]
{i : ι}
{j : ι}
(h : i ≠ j)
(X : V)
:
HomologicalComplex.Hom.f ((HomologicalComplex.singleMapHomologicalComplex F c j).hom.app X) i = 0
@[simp]
theorem
HomologicalComplex.singleMapHomologicalComplex_inv_app_self
{ι : Type u_1}
{V : Type u}
[CategoryTheory.Category.{v, u} V]
[CategoryTheory.Preadditive V]
(c : ComplexShape ι)
[CategoryTheory.Limits.HasZeroObject V]
{W : Type u_2}
[CategoryTheory.Category.{u_3, u_2} W]
[CategoryTheory.Preadditive W]
[CategoryTheory.Limits.HasZeroObject W]
(F : CategoryTheory.Functor V W)
[CategoryTheory.Functor.Additive F]
(j : ι)
(X : V)
:
HomologicalComplex.Hom.f ((HomologicalComplex.singleMapHomologicalComplex F c j).inv.app X) j = CategoryTheory.eqToHom (_ : (if j = j then F.obj X else 0) = F.obj (if j = j then X else 0))
@[simp]
theorem
HomologicalComplex.singleMapHomologicalComplex_inv_app_ne
{ι : Type u_1}
{V : Type u}
[CategoryTheory.Category.{v, u} V]
[CategoryTheory.Preadditive V]
(c : ComplexShape ι)
[CategoryTheory.Limits.HasZeroObject V]
{W : Type u_2}
[CategoryTheory.Category.{u_3, u_2} W]
[CategoryTheory.Preadditive W]
[CategoryTheory.Limits.HasZeroObject W]
(F : CategoryTheory.Functor V W)
[CategoryTheory.Functor.Additive F]
{i : ι}
{j : ι}
(h : i ≠ j)
(X : V)
:
HomologicalComplex.Hom.f ((HomologicalComplex.singleMapHomologicalComplex F c j).inv.app X) i = 0
def
ChainComplex.single₀MapHomologicalComplex
{V : Type u}
[CategoryTheory.Category.{v, u} V]
[CategoryTheory.Preadditive V]
[CategoryTheory.Limits.HasZeroObject V]
{W : Type u_2}
[CategoryTheory.Category.{u_3, u_2} W]
[CategoryTheory.Preadditive W]
[CategoryTheory.Limits.HasZeroObject W]
(F : CategoryTheory.Functor V W)
[CategoryTheory.Functor.Additive F]
:
Turning an object into a chain complex supported at zero then applying a functor is the same as applying the functor then forming the complex.
Instances For
@[simp]
theorem
ChainComplex.single₀MapHomologicalComplex_hom_app_zero
{V : Type u}
[CategoryTheory.Category.{v, u} V]
[CategoryTheory.Preadditive V]
[CategoryTheory.Limits.HasZeroObject V]
{W : Type u_2}
[CategoryTheory.Category.{u_3, u_2} W]
[CategoryTheory.Preadditive W]
[CategoryTheory.Limits.HasZeroObject W]
(F : CategoryTheory.Functor V W)
[CategoryTheory.Functor.Additive F]
(X : V)
:
@[simp]
theorem
ChainComplex.single₀MapHomologicalComplex_hom_app_succ
{V : Type u}
[CategoryTheory.Category.{v, u} V]
[CategoryTheory.Preadditive V]
[CategoryTheory.Limits.HasZeroObject V]
{W : Type u_2}
[CategoryTheory.Category.{u_3, u_2} W]
[CategoryTheory.Preadditive W]
[CategoryTheory.Limits.HasZeroObject W]
(F : CategoryTheory.Functor V W)
[CategoryTheory.Functor.Additive F]
(X : V)
(n : ℕ)
:
HomologicalComplex.Hom.f ((ChainComplex.single₀MapHomologicalComplex F).hom.app X) (n + 1) = 0
@[simp]
theorem
ChainComplex.single₀MapHomologicalComplex_inv_app_zero
{V : Type u}
[CategoryTheory.Category.{v, u} V]
[CategoryTheory.Preadditive V]
[CategoryTheory.Limits.HasZeroObject V]
{W : Type u_2}
[CategoryTheory.Category.{u_3, u_2} W]
[CategoryTheory.Preadditive W]
[CategoryTheory.Limits.HasZeroObject W]
(F : CategoryTheory.Functor V W)
[CategoryTheory.Functor.Additive F]
(X : V)
:
HomologicalComplex.Hom.f ((ChainComplex.single₀MapHomologicalComplex F).inv.app X) 0 = CategoryTheory.CategoryStruct.id
(HomologicalComplex.X ((CategoryTheory.Functor.comp F (ChainComplex.single₀ W)).obj X) 0)
@[simp]
theorem
ChainComplex.single₀MapHomologicalComplex_inv_app_succ
{V : Type u}
[CategoryTheory.Category.{v, u} V]
[CategoryTheory.Preadditive V]
[CategoryTheory.Limits.HasZeroObject V]
{W : Type u_2}
[CategoryTheory.Category.{u_3, u_2} W]
[CategoryTheory.Preadditive W]
[CategoryTheory.Limits.HasZeroObject W]
(F : CategoryTheory.Functor V W)
[CategoryTheory.Functor.Additive F]
(X : V)
(n : ℕ)
:
HomologicalComplex.Hom.f ((ChainComplex.single₀MapHomologicalComplex F).inv.app X) (n + 1) = 0
def
CochainComplex.single₀MapHomologicalComplex
{V : Type u}
[CategoryTheory.Category.{v, u} V]
[CategoryTheory.Preadditive V]
[CategoryTheory.Limits.HasZeroObject V]
{W : Type u_2}
[CategoryTheory.Category.{u_3, u_2} W]
[CategoryTheory.Preadditive W]
[CategoryTheory.Limits.HasZeroObject W]
(F : CategoryTheory.Functor V W)
[CategoryTheory.Functor.Additive F]
:
Turning an object into a cochain complex supported at zero then applying a functor is the same as applying the functor then forming the cochain complex.
Instances For
@[simp]
theorem
CochainComplex.single₀MapHomologicalComplex_hom_app_zero
{V : Type u}
[CategoryTheory.Category.{v, u} V]
[CategoryTheory.Preadditive V]
[CategoryTheory.Limits.HasZeroObject V]
{W : Type u_2}
[CategoryTheory.Category.{u_3, u_2} W]
[CategoryTheory.Preadditive W]
[CategoryTheory.Limits.HasZeroObject W]
(F : CategoryTheory.Functor V W)
[CategoryTheory.Functor.Additive F]
(X : V)
:
@[simp]
theorem
CochainComplex.single₀MapHomologicalComplex_hom_app_succ
{V : Type u}
[CategoryTheory.Category.{v, u} V]
[CategoryTheory.Preadditive V]
[CategoryTheory.Limits.HasZeroObject V]
{W : Type u_2}
[CategoryTheory.Category.{u_3, u_2} W]
[CategoryTheory.Preadditive W]
[CategoryTheory.Limits.HasZeroObject W]
(F : CategoryTheory.Functor V W)
[CategoryTheory.Functor.Additive F]
(X : V)
(n : ℕ)
:
HomologicalComplex.Hom.f ((CochainComplex.single₀MapHomologicalComplex F).hom.app X) (n + 1) = 0
@[simp]
theorem
CochainComplex.single₀MapHomologicalComplex_inv_app_zero
{V : Type u}
[CategoryTheory.Category.{v, u} V]
[CategoryTheory.Preadditive V]
[CategoryTheory.Limits.HasZeroObject V]
{W : Type u_2}
[CategoryTheory.Category.{u_3, u_2} W]
[CategoryTheory.Preadditive W]
[CategoryTheory.Limits.HasZeroObject W]
(F : CategoryTheory.Functor V W)
[CategoryTheory.Functor.Additive F]
(X : V)
:
HomologicalComplex.Hom.f ((CochainComplex.single₀MapHomologicalComplex F).inv.app X) 0 = CategoryTheory.CategoryStruct.id
(HomologicalComplex.X ((CategoryTheory.Functor.comp F (CochainComplex.single₀ W)).obj X) 0)
@[simp]
theorem
CochainComplex.single₀MapHomologicalComplex_inv_app_succ
{V : Type u}
[CategoryTheory.Category.{v, u} V]
[CategoryTheory.Preadditive V]
[CategoryTheory.Limits.HasZeroObject V]
{W : Type u_2}
[CategoryTheory.Category.{u_3, u_2} W]
[CategoryTheory.Preadditive W]
[CategoryTheory.Limits.HasZeroObject W]
(F : CategoryTheory.Functor V W)
[CategoryTheory.Functor.Additive F]
(X : V)
(n : ℕ)
:
HomologicalComplex.Hom.f ((CochainComplex.single₀MapHomologicalComplex F).inv.app X) (n + 1) = 0