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} :

Zero (C ⟶ D)

Equations

HomologicalComplex.instZeroHomHomologicalComplexPreadditiveHasZeroMorphismsToQuiverToCategoryStructInstCategoryHomologicalComplex = { zero := HomologicalComplex.Hom.mk fun (i : ι) => 0 }

source

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} :

Add (C ⟶ D)

Equations

One or more equations did not get rendered due to their size.

source

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} :

Neg (C ⟶ D)

Equations

One or more equations did not get rendered due to their size.

source

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} :

Sub (C ⟶ D)

Equations

One or more equations did not get rendered due to their size.

source

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} :

SMul ℕ (C ⟶ D)

Equations

HomologicalComplex.hasNatScalar = { smul := fun (n : ℕ) (f : C ⟶ D) => HomologicalComplex.Hom.mk fun (i : ι) => n • f.f i }

source

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} :

SMul ℤ (C ⟶ D)

Equations

HomologicalComplex.hasIntScalar = { smul := fun (n : ℤ) (f : C ⟶ D) => HomologicalComplex.Hom.mk fun (i : ι) => n • f.f i }

source

@[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 : ι) :

0.f i = 0

source

@[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 : ι) :

(f + g).f i = f.f i + g.f i

source

@[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 : ι) :

(-f).f i = -f.f i

source

@[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 : ι) :

(f - g).f i = f.f i - g.f i

source

@[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 : ι) :

(n • f).f i = n • f.f i

source

@[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 : ι) :

(n • f).f i = n • f.f i

source

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)

Equations

One or more equations did not get rendered due to their size.

source

instance HomologicalComplex.instPreadditiveHomologicalComplexPreadditiveHasZeroMorphismsInstCategoryHomologicalComplex {ι : Type u_1} {V : Type u} [CategoryTheory.Category.{v, u} V] [CategoryTheory.Preadditive V] {c : ComplexShape ι} :

CategoryTheory.Preadditive (HomologicalComplex V c)

Equations

HomologicalComplex.instPreadditiveHomologicalComplexPreadditiveHasZeroMorphismsInstCategoryHomologicalComplex = CategoryTheory.Preadditive.mk

source

@[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₂) :

(HomologicalComplex.Hom.fAddMonoidHom i) f = f.f i

source

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₂) →+ (C₁.X i ⟶ C₂.X i)

The i-th component of a chain map, as an additive map from chain maps to morphisms.

Equations

One or more equations did not get rendered due to their size.

Instances For

source

instance HomologicalComplex.eval_additive {ι : Type u_1} {V : Type u} [CategoryTheory.Category.{v, u} V] [CategoryTheory.Preadditive V] {c : ComplexShape ι} (i : ι) :

CategoryTheory.Functor.Additive (HomologicalComplex.eval V c i)

Equations

(_ : CategoryTheory.Functor.Additive (HomologicalComplex.eval V c i)) = (_ : CategoryTheory.Functor.Additive (HomologicalComplex.eval V c i))

source

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] :

CategoryTheory.Functor.Additive (cycles'Functor V c i)

Equations

(_ : CategoryTheory.Functor.Additive (cycles'Functor V c i)) = (_ : CategoryTheory.Functor.Additive (cycles'Functor V c i))

source

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] :

CategoryTheory.Functor.Additive (boundariesFunctor V c i)

Equations

(_ : CategoryTheory.Functor.Additive (boundariesFunctor V c i)) = (_ : CategoryTheory.Functor.Additive (boundariesFunctor V c i))

source

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] :

CategoryTheory.Functor.Additive (homology'Functor V c i)

Equations

(_ : CategoryTheory.Functor.Additive (homology'Functor V c i)) = (_ : CategoryTheory.Functor.Additive (homology'Functor V c i))

source

@[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 : ι), ((CategoryTheory.Functor.mapHomologicalComplex F c).toPrefunctor.map f).f i = F.toPrefunctor.map (f.f i)

source

@[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 : ι) :

((CategoryTheory.Functor.mapHomologicalComplex F c).toPrefunctor.obj C).d i j = F.toPrefunctor.map (C.d i j)

source

@[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 : ι) :

((CategoryTheory.Functor.mapHomologicalComplex F c).toPrefunctor.obj C).X i = F.toPrefunctor.obj (C.X i)

source

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 ι) :

CategoryTheory.Functor (HomologicalComplex V c) (HomologicalComplex W c)

An additive functor induces a functor between homological complexes. This is sometimes called the "prolongation".

Equations

One or more equations did not get rendered due to their size.

Instances For

source

@[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 : ι) :

((CategoryTheory.Functor.mapHomologicalComplexIdIso V c).hom.app X).f i = CategoryTheory.CategoryStruct.id (X.X i)

source

@[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 : ι) :

((CategoryTheory.Functor.mapHomologicalComplexIdIso V c).inv.app X).f i = CategoryTheory.CategoryStruct.id (X.X i)

source

def CategoryTheory.Functor.mapHomologicalComplexIdIso {ι : Type u_1} (V : Type u) [CategoryTheory.Category.{v, u} V] [CategoryTheory.Preadditive V] (c : ComplexShape ι) :

CategoryTheory.Functor.mapHomologicalComplex (CategoryTheory.Functor.id V) c ≅ CategoryTheory.Functor.id (HomologicalComplex V c)

The functor on homological complexes induced by the identity functor is isomorphic to the identity functor.

Equations

One or more equations did not get rendered due to their size.

Instances For

source

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 ι) :

CategoryTheory.Functor.Additive (CategoryTheory.Functor.mapHomologicalComplex F c)

Equations

(_ : CategoryTheory.Functor.Additive (CategoryTheory.Functor.mapHomologicalComplex F c)) = (_ : CategoryTheory.Functor.Additive (CategoryTheory.Functor.mapHomologicalComplex F c))

source

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 ι) :

CategoryTheory.ReflectsIsomorphisms (CategoryTheory.Functor.mapHomologicalComplex F c)

Equations

(_ : CategoryTheory.ReflectsIsomorphisms (CategoryTheory.Functor.mapHomologicalComplex F c)) = (_ : CategoryTheory.ReflectsIsomorphisms (CategoryTheory.Functor.mapHomologicalComplex F c))

source

@[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 : ι) :

((CategoryTheory.NatTrans.mapHomologicalComplex α c).app C).f i = α.app (C.X i)

source

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 ι) :

CategoryTheory.Functor.mapHomologicalComplex F c ⟶ CategoryTheory.Functor.mapHomologicalComplex G c

A natural transformation between functors induces a natural transformation between those functors applied to homological complexes.

Equations

CategoryTheory.NatTrans.mapHomologicalComplex α c = CategoryTheory.NatTrans.mk fun (C : HomologicalComplex V c) => HomologicalComplex.Hom.mk fun (i : ι) => α.app (C.X i)

Instances For

source

@[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] :

CategoryTheory.NatTrans.mapHomologicalComplex (CategoryTheory.CategoryStruct.id F) c = CategoryTheory.CategoryStruct.id (CategoryTheory.Functor.mapHomologicalComplex F c)

source

@[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) :

CategoryTheory.NatTrans.mapHomologicalComplex (CategoryTheory.CategoryStruct.comp α β) c = CategoryTheory.CategoryStruct.comp (CategoryTheory.NatTrans.mapHomologicalComplex α c) (CategoryTheory.NatTrans.mapHomologicalComplex β c)

source

@[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).toPrefunctor.obj D ⟶ Z) :

CategoryTheory.CategoryStruct.comp ((CategoryTheory.Functor.mapHomologicalComplex F c).toPrefunctor.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).toPrefunctor.map f) h)

source

@[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).toPrefunctor.map f) ((CategoryTheory.NatTrans.mapHomologicalComplex α c).app D) = CategoryTheory.CategoryStruct.comp ((CategoryTheory.NatTrans.mapHomologicalComplex α c).app C) ((CategoryTheory.Functor.mapHomologicalComplex G c).toPrefunctor.map f)

source

@[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 : ι) :

((CategoryTheory.NatIso.mapHomologicalComplex α c).hom.app C).f i = α.hom.app (C.X i)

source

@[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 : ι) :

((CategoryTheory.NatIso.mapHomologicalComplex α c).inv.app C).f i = α.inv.app (C.X i)

source

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 ι) :

CategoryTheory.Functor.mapHomologicalComplex F c ≅ CategoryTheory.Functor.mapHomologicalComplex G c

A natural isomorphism between functors induces a natural isomorphism between those functors applied to homological complexes.

Equations

CategoryTheory.NatIso.mapHomologicalComplex α c = CategoryTheory.Iso.mk (CategoryTheory.NatTrans.mapHomologicalComplex α.hom c) (CategoryTheory.NatTrans.mapHomologicalComplex α.inv c)

Instances For

source

@[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

source

@[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

source

@[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

source

@[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

source

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.

Equations

One or more equations did not get rendered due to their size.

Instances For

source

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 α)).toPrefunctor.obj (ChainComplex.of X d sq) = ChainComplex.of (fun (n : α) => F.toPrefunctor.obj (X n)) (fun (n : α) => F.toPrefunctor.map (d n)) (_ : ∀ (n : α), CategoryTheory.CategoryStruct.comp ((fun (n : α) => F.toPrefunctor.map (d n)) (n + 1)) ((fun (n : α) => F.toPrefunctor.map (d n)) n) = 0)

source