Theorems · Definition · category theory

CategoryTheory.SingleFunctors.Hom.comp

{C : Type u_1} →
  {D : Type u_2} →
    [inst : CategoryTheory.Category.{v_1, u_1} C] →
      [inst_1 : CategoryTheory.Category.{v_2, u_2} D] →
        {A : Type u_5} →
          [inst_2 : AddMonoid A] →
            [inst_3 : CategoryTheory.HasShift D A] →
              {F G H : CategoryTheory.SingleFunctors C D A} → F.Hom G → G.Hom H → F.Hom H

The composition of morphisms in SingleFunctors C D A.

Defined in: Mathlib.CategoryTheory.Shift.SingleFunctors
Cited by: 1 results in Mathlib
Foundations: Depth 29 from the axioms · uses propext, Classical.choice, Quot.sound
Assumes: CategoryTheory.Category CategoryTheory.Category AddMonoid CategoryTheory.HasShift

Mathlib docs Source Loogle LeanSearch

Around this declaration

Dashed lines are statement dependencies; solid lines are citations in proofs.

Cites7

Mathlib declarations this one mentions in its statement or cites explicitly in its proof. Plumbing is filtered out.

CategoryTheory.Categorystatement and proof · cited by 32,673
CategoryTheory.CategoryStruct.compproof · cited by 17,999
AddMonoidstatement and proof · cited by 2,864
CategoryTheory.HasShiftstatement and proof · cited by 1,527
CategoryTheory.SingleFunctorsstatement and proof · cited by 65
CategoryTheory.SingleFunctors.Hom.homproof · cited by 38
CategoryTheory.SingleFunctors.Homstatement and proof · cited by 9

Cited by1

Results whose statement or proof uses this declaration.

CategoryTheory.SingleFunctors.Hom.comp_homstatement and proof · cited by 0