Documentation

Mathlib.Algebra.Homology.Additive

Homology is an additive functor #

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

Equations
  • HomologicalComplex.instZeroHom_1 = { zero := { f := fun (i : ι) => 0, comm' := } }
Equations
  • HomologicalComplex.instAddHom = { add := fun (f g : C D) => { f := fun (i : ι) => f.f i + g.f i, comm' := } }
Equations
  • HomologicalComplex.instNegHom = { neg := fun (f : C D) => { f := fun (i : ι) => -f.f i, comm' := } }
Equations
  • HomologicalComplex.instSubHom = { sub := fun (f g : C D) => { f := fun (i : ι) => f.f i - g.f i, comm' := } }
Equations
  • HomologicalComplex.hasNatScalar = { smul := fun (n : ) (f : C D) => { f := fun (i : ι) => n f.f i, comm' := } }
Equations
  • HomologicalComplex.hasIntScalar = { smul := fun (n : ) (f : C D) => { f := fun (i : ι) => n f.f i, comm' := } }
@[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
@[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
@[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
@[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
@[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
Equations
Equations
  • HomologicalComplex.instPreadditive = { homGroup := inferInstance, add_comp := , comp_add := }
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
Instances For
    Equations
    • =
    @[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₂) [F.PreservesZeroMorphisms] (c : ComplexShape ι) (C : HomologicalComplex W₁ c) (i : ι) :
    ((F.mapHomologicalComplex c).obj C).X i = F.obj (C.X i)
    @[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₂) [F.PreservesZeroMorphisms] (c : ComplexShape ι) :
    ∀ {X Y : HomologicalComplex W₁ c} (f : X Y) (i : ι), ((F.mapHomologicalComplex c).map f).f i = F.map (f.f i)
    @[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₂) [F.PreservesZeroMorphisms] (c : ComplexShape ι) (C : HomologicalComplex W₁ c) (i : ι) (j : ι) :
    ((F.mapHomologicalComplex c).obj C).d i j = F.map (C.d i j)

    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
      instance CategoryTheory.instPreservesZeroMorphismsHomologicalComplexMapHomologicalComplex {ι : 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₂) [F.PreservesZeroMorphisms] (c : ComplexShape ι) :
      (F.mapHomologicalComplex c).PreservesZeroMorphisms
      Equations
      • =
      Equations
      • =

      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
        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₂) [F.PreservesZeroMorphisms] [F.ReflectsIsomorphisms] (c : ComplexShape ι) :
        (F.mapHomologicalComplex c).ReflectsIsomorphisms
        Equations
        • =
        @[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₂} [F.PreservesZeroMorphisms] [G.PreservesZeroMorphisms] (α : F G) (c : ComplexShape ι) (C : HomologicalComplex W₁ c) (i : ι) :
        ((CategoryTheory.NatTrans.mapHomologicalComplex α c).app C).f i = α.app (C.X i)
        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₂} [F.PreservesZeroMorphisms] [G.PreservesZeroMorphisms] (α : F G) (c : ComplexShape ι) :
        F.mapHomologicalComplex c G.mapHomologicalComplex c

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

        Equations
        Instances For
          @[simp]
          theorem CategoryTheory.NatTrans.mapHomologicalComplex_naturality_assoc {ι : 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₂] {c : ComplexShape ι} {F : CategoryTheory.Functor W₁ W₂} {G : CategoryTheory.Functor W₁ W₂} [F.PreservesZeroMorphisms] [G.PreservesZeroMorphisms] (α : F G) {C : HomologicalComplex W₁ c} {D : HomologicalComplex W₁ c} (f : C D) {Z : HomologicalComplex W₂ c} (h : (G.mapHomologicalComplex c).obj D Z) :
          @[simp]
          theorem CategoryTheory.NatTrans.mapHomologicalComplex_naturality {ι : 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₂] {c : ComplexShape ι} {F : CategoryTheory.Functor W₁ W₂} {G : CategoryTheory.Functor W₁ W₂} [F.PreservesZeroMorphisms] [G.PreservesZeroMorphisms] (α : F G) {C : HomologicalComplex W₁ c} {D : HomologicalComplex W₁ c} (f : C D) :
          CategoryTheory.CategoryStruct.comp ((F.mapHomologicalComplex c).map f) ((CategoryTheory.NatTrans.mapHomologicalComplex α c).app D) = CategoryTheory.CategoryStruct.comp ((CategoryTheory.NatTrans.mapHomologicalComplex α c).app C) ((G.mapHomologicalComplex c).map f)
          @[simp]
          theorem CategoryTheory.NatIso.mapHomologicalComplex_hom_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₂} [F.PreservesZeroMorphisms] [G.PreservesZeroMorphisms] (α : F G) (c : ComplexShape ι) (C : HomologicalComplex W₁ c) (i : ι) :
          ((CategoryTheory.NatIso.mapHomologicalComplex α c).hom.app C).f i = α.hom.app (C.X i)
          @[simp]
          theorem CategoryTheory.NatIso.mapHomologicalComplex_inv_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₂} [F.PreservesZeroMorphisms] [G.PreservesZeroMorphisms] (α : F G) (c : ComplexShape ι) (C : HomologicalComplex W₁ c) (i : ι) :
          ((CategoryTheory.NatIso.mapHomologicalComplex α c).inv.app C).f i = α.inv.app (C.X i)
          def CategoryTheory.NatIso.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₂} [F.PreservesZeroMorphisms] [G.PreservesZeroMorphisms] (α : F G) (c : ComplexShape ι) :
          F.mapHomologicalComplex c G.mapHomologicalComplex c

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

          Equations
          • One or more equations did not get rendered due to their size.
          Instances For
            @[simp]
            theorem CategoryTheory.Equivalence.mapHomologicalComplex_unitIso {ι : 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₂] (e : W₁ W₂) [e.functor.PreservesZeroMorphisms] (c : ComplexShape ι) :
            (e.mapHomologicalComplex c).unitIso = (CategoryTheory.Functor.mapHomologicalComplexIdIso W₁ c).symm.trans (CategoryTheory.NatIso.mapHomologicalComplex e.unitIso c)
            @[simp]
            theorem CategoryTheory.Equivalence.mapHomologicalComplex_functor {ι : 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₂] (e : W₁ W₂) [e.functor.PreservesZeroMorphisms] (c : ComplexShape ι) :
            (e.mapHomologicalComplex c).functor = e.functor.mapHomologicalComplex c
            @[simp]
            theorem CategoryTheory.Equivalence.mapHomologicalComplex_counitIso {ι : 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₂] (e : W₁ W₂) [e.functor.PreservesZeroMorphisms] (c : ComplexShape ι) :
            (e.mapHomologicalComplex c).counitIso = (CategoryTheory.NatIso.mapHomologicalComplex e.counitIso c).trans (CategoryTheory.Functor.mapHomologicalComplexIdIso W₂ c)
            @[simp]
            theorem CategoryTheory.Equivalence.mapHomologicalComplex_inverse {ι : 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₂] (e : W₁ W₂) [e.functor.PreservesZeroMorphisms] (c : ComplexShape ι) :
            (e.mapHomologicalComplex c).inverse = e.inverse.mapHomologicalComplex 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
              theorem ChainComplex.map_chain_complex_of {W₁ : Type u_3} {W₂ : Type u_4} [CategoryTheory.Category.{u_6, u_3} W₁] [CategoryTheory.Category.{u_7, u_4} W₂] [CategoryTheory.Limits.HasZeroMorphisms W₁] [CategoryTheory.Limits.HasZeroMorphisms W₂] {α : Type u_5} [AddRightCancelSemigroup α] [One α] [DecidableEq α] (F : CategoryTheory.Functor W₁ W₂) [F.PreservesZeroMorphisms] (X : αW₁) (d : (n : α) → X (n + 1) X n) (sq : ∀ (n : α), CategoryTheory.CategoryStruct.comp (d (n + 1)) (d n) = 0) :
              (F.mapHomologicalComplex (ComplexShape.down α)).obj (ChainComplex.of X d sq) = ChainComplex.of (fun (n : α) => F.obj (X n)) (fun (n : α) => F.map (d n))

              Turning an object into a complex supported at j then applying a functor is the same as applying the functor then forming the complex.

              Equations
              • One or more equations did not get rendered due to their size.
              Instances For