Homology is an additive functor #

When V is preadditive, HomologicalComplex V c is also preadditive, and homologyFunctor is additive.

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 := { f := fun (i : ι) => 0, comm' := ⋯ } }

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) => { f := fun (i : ι) => n • f.f i, comm' := ⋯ } }

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) => { f := fun (i : ι) => n • f.f i, comm' := ⋯ } }

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 = { homGroup := inferInstance, add_comp := ⋯, comp_add := ⋯ }

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

HomologicalComplex.Hom.fAddMonoidHom i = AddMonoidHom.mk' (fun (f : C₁ ⟶ C₂) => f.f i) ⋯

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

⋯ = ⋯

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

⋯ = ⋯

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

⋯ = ⋯

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

⋯ = ⋯

source

@[simp]

theorem CategoryTheory.Functor.mapHomologicalComplex_obj_X {ι : Type u_1} {W₁ : Type u_3} {W₂ : Type u_4} [CategoryTheory.Category.{u_5, u_3} W₁] [CategoryTheory.Category.{u_6, u_4} W₂] [CategoryTheory.Limits.HasZeroMorphisms W₁] [CategoryTheory.Limits.HasZeroMorphisms W₂] (F : CategoryTheory.Functor W₁ W₂) [CategoryTheory.Functor.PreservesZeroMorphisms F] (c : ComplexShape ι) (C : HomologicalComplex W₁ c) (i : ι) :

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

source

@[simp]

theorem CategoryTheory.Functor.mapHomologicalComplex_map_f {ι : Type u_1} {W₁ : Type u_3} {W₂ : Type u_4} [CategoryTheory.Category.{u_5, u_3} W₁] [CategoryTheory.Category.{u_6, u_4} W₂] [CategoryTheory.Limits.HasZeroMorphisms W₁] [CategoryTheory.Limits.HasZeroMorphisms W₂] (F : CategoryTheory.Functor W₁ W₂) [CategoryTheory.Functor.PreservesZeroMorphisms F] (c : ComplexShape ι) :

∀ {X Y : HomologicalComplex W₁ c} (f : X ⟶ Y) (i : ι), ((CategoryTheory.Functor.mapHomologicalComplex F c).map f).f i = F.map (f.f i)

source

@[simp]

theorem CategoryTheory.Functor.mapHomologicalComplex_obj_d {ι : Type u_1} {W₁ : Type u_3} {W₂ : Type u_4} [CategoryTheory.Category.{u_5, u_3} W₁] [CategoryTheory.Category.{u_6, u_4} W₂] [CategoryTheory.Limits.HasZeroMorphisms W₁] [CategoryTheory.Limits.HasZeroMorphisms W₂] (F : CategoryTheory.Functor W₁ W₂) [CategoryTheory.Functor.PreservesZeroMorphisms F] (c : ComplexShape ι) (C : HomologicalComplex W₁ c) (i : ι) (j : ι) :

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

source

def CategoryTheory.Functor.mapHomologicalComplex {ι : Type u_1} {W₁ : Type u_3} {W₂ : Type u_4} [CategoryTheory.Category.{u_5, u_3} W₁] [CategoryTheory.Category.{u_6, u_4} W₂] [CategoryTheory.Limits.HasZeroMorphisms W₁] [CategoryTheory.Limits.HasZeroMorphisms W₂] (F : CategoryTheory.Functor W₁ W₂) [CategoryTheory.Functor.PreservesZeroMorphisms F] (c : ComplexShape ι) :

CategoryTheory.Functor (HomologicalComplex W₁ 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

instance CategoryTheory.instPreservesZeroMorphismsHomologicalComplexInstCategoryHomologicalComplexHomologicalComplexInstCategoryHomologicalComplexInstHasZeroMorphismsHomologicalComplexInstCategoryHomologicalComplexInstHasZeroMorphismsHomologicalComplexInstCategoryHomologicalComplexMapHomologicalComplex {ι : Type u_1} {W₁ : Type u_3} {W₂ : Type u_4} [CategoryTheory.Category.{u_5, u_3} W₁] [CategoryTheory.Category.{u_6, u_4} W₂] [CategoryTheory.Limits.HasZeroMorphisms W₁] [CategoryTheory.Limits.HasZeroMorphisms W₂] (F : CategoryTheory.Functor W₁ W₂) [CategoryTheory.Functor.PreservesZeroMorphisms F] (c : ComplexShape ι) :

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

Equations

⋯ = ⋯

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_5, 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

⋯ = ⋯

source

@[simp]

theorem CategoryTheory.Functor.mapHomologicalComplexIdIso_inv_app_f {ι : Type u_1} (W₁ : Type u_3) [CategoryTheory.Category.{u_5, u_3} W₁] [CategoryTheory.Limits.HasZeroMorphisms W₁] (c : ComplexShape ι) (X : HomologicalComplex W₁ c) (i : ι) :

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

source

@[simp]

theorem CategoryTheory.Functor.mapHomologicalComplexIdIso_hom_app_f {ι : Type u_1} (W₁ : Type u_3) [CategoryTheory.Category.{u_5, u_3} W₁] [CategoryTheory.Limits.HasZeroMorphisms W₁] (c : ComplexShape ι) (X : HomologicalComplex W₁ c) (i : ι) :

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

source

def CategoryTheory.Functor.mapHomologicalComplexIdIso {ι : Type u_1} (W₁ : Type u_3) [CategoryTheory.Category.{u_5, u_3} W₁] [CategoryTheory.Limits.HasZeroMorphisms W₁] (c : ComplexShape ι) :

CategoryTheory.Functor.mapHomologicalComplex (CategoryTheory.Functor.id W₁) c ≅ CategoryTheory.Functor.id (HomologicalComplex W₁ 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.mapHomologicalComplex_reflects_iso {ι : Type u_1} (W₁ : Type u_3) {W₂ : Type u_4} [CategoryTheory.Category.{u_5, u_3} W₁] [CategoryTheory.Category.{u_6, u_4} W₂] [CategoryTheory.Limits.HasZeroMorphisms W₁] [CategoryTheory.Limits.HasZeroMorphisms W₂] (F : CategoryTheory.Functor W₁ W₂) [CategoryTheory.Functor.PreservesZeroMorphisms F] [CategoryTheory.Functor.ReflectsIsomorphisms F] (c : ComplexShape ι) :

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

Equations

⋯ = ⋯

source

@[simp]

theorem CategoryTheory.NatTrans.mapHomologicalComplex_app_f {ι : Type u_1} {W₁ : Type u_3} {W₂ : Type u_4} [CategoryTheory.Category.{u_5, u_3} W₁] [CategoryTheory.Category.{u_6, u_4} W₂] [CategoryTheory.Limits.HasZeroMorphisms W₁] [CategoryTheory.Limits.HasZeroMorphisms W₂] {F : CategoryTheory.Functor W₁ W₂} {G : CategoryTheory.Functor W₁ W₂} [CategoryTheory.Functor.PreservesZeroMorphisms F] [CategoryTheory.Functor.PreservesZeroMorphisms G] (α : F ⟶ G) (c : ComplexShape ι) (C : HomologicalComplex W₁ c) (i : ι) :

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

source

def CategoryTheory.NatTrans.mapHomologicalComplex {ι : Type u_1} {W₁ : Type u_3} {W₂ : Type u_4} [CategoryTheory.Category.{u_5, u_3} W₁] [CategoryTheory.Category.{u_6, u_4} W₂] [CategoryTheory.Limits.HasZeroMorphisms W₁] [CategoryTheory.Limits.HasZeroMorphisms W₂] {F : CategoryTheory.Functor W₁ W₂} {G : CategoryTheory.Functor W₁ W₂} [CategoryTheory.Functor.PreservesZeroMorphisms F] [CategoryTheory.Functor.PreservesZeroMorphisms 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 = { app := fun (C : HomologicalComplex W₁ c) => { f := fun (i : ι) => α.app (C.X i), comm' := ⋯ }, naturality := ⋯ }