Theorems · Definition · category theory

CategoryTheory.ShortComplex.RightHomologyMapData.ofIsLimitKernelFork

{C : Type u_1} →
  [inst : CategoryTheory.Category.{v_1, u_1} C] →
    [inst_1 : CategoryTheory.Limits.HasZeroMorphisms C] →
      {S₁ S₂ : CategoryTheory.ShortComplex C} →
        (φ : S₁ ⟶ S₂) →
          (hf₁ : S₁.f = 0) →
            (c₁ : CategoryTheory.Limits.KernelFork S₁.g) →
              (hc₁ : CategoryTheory.Limits.IsLimit c₁) →
                (hf₂ : S₂.f = 0) →
                  (c₂ : CategoryTheory.Limits.KernelFork S₂.g) →
                    (hc₂ : CategoryTheory.Limits.IsLimit c₂) →
                      (f : c₁.pt ⟶ c₂.pt) →
                        CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.Fork.ι c₁) φ.τ₂ =
                            CategoryTheory.CategoryStruct.comp f (CategoryTheory.Limits.Fork.ι c₂) →
                          CategoryTheory.ShortComplex.RightHomologyMapData φ
                            (CategoryTheory.ShortComplex.RightHomologyData.ofIsLimitKernelFork S₁ hf₁ c₁ hc₁)
                            (CategoryTheory.ShortComplex.RightHomologyData.ofIsLimitKernelFork S₂ hf₂ c₂ hc₂)

When S₁.f and S₂.f are zero and we have chosen limit kernel forks c₁ and c₂ for S₁.g and S₂.g respectively, the action on right homology of a morphism φ : S₁ ⟶ S₂ of short complexes is given by the unique morphism f : c₁.pt ⟶ c₂.pt such that c₁.ι ≫ φ.τ₂ = f ≫ c₂.ι.

Defined in

Mathlib.Algebra.Homology.ShortComplex.RightHomology

Cited by

3 results in Mathlib

Foundations

Depth 37 from the axioms · uses propext, Classical.choice, Quot.sound

Assumes

CategoryTheory.CategoryCategoryTheory.Limits.HasZeroMorphisms