Theorems · Definition · category theory

CategoryTheory.DifferentialObject.objEqToHom

{β : Type u_1} →
  [inst : AddCommGroup β] →
    {b : β} →
      {V : Type u_2} →
        [inst_1 : CategoryTheory.Category.{v_1, u_2} V] →
          [inst_2 : CategoryTheory.Limits.HasZeroMorphisms V] →
            (X : CategoryTheory.DifferentialObject ℤ (CategoryTheory.GradedObjectWithShift b V)) →
              {i j : β} → i = j → (X.obj i ⟶ X.obj j)

Since eqToHom only preserves the fact that X.X i = X.X j but not i = j, this definition is used to aid the simplifier.

Defined in

Mathlib.Algebra.Homology.DifferentialObject

Cited by

8 results in Mathlib

Foundations

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

Assumes

AddCommGroupCategoryTheory.CategoryCategoryTheory.Limits.HasZeroMorphisms