Theorems · Theorem · category theory
CategoryTheory.Preadditive.sub_comp
∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] [inst_1 : CategoryTheory.Preadditive C] {P Q R : C}
(f f' : P ⟶ Q) (g : Q ⟶ R),
CategoryTheory.CategoryStruct.comp (f - f') g =
CategoryTheory.CategoryStruct.comp f g - CategoryTheory.CategoryStruct.comp f' g- Defined in
- Mathlib.CategoryTheory.Preadditive.Basic
- Cited by
- 34 results in Mathlib
- Foundations
- Depth 16 from the axioms · uses propext, Classical.choice, Quot.sound
Around this declaration
Dashed lines are statement dependencies; solid lines are citations in proofs.
Cites6
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
- Quiver.Homstatement and proof · cited by 32,603
- CategoryTheory.CategoryStruct.compstatement · cited by 17,999
- CategoryTheory.Preadditivestatement and proof · cited by 3,309
- map_subproof · cited by 565
- CategoryTheory.Preadditive.rightCompproof · cited by 6
Cited by34
Results whose statement or proof uses this declaration.
- CategoryTheory.Triangulated.TStructure.to_truncLT_obj_extproof · cited by 6
- CategoryTheory.ShortComplex.SnakeInput.L₁'_exactproof · cited by 4
- CategoryTheory.Adjunction.isTriangulated_rightAdjointproof · cited by 3
- CategoryTheory.Abelian.epi_of_epi_of_epi_of_mono'proof · cited by 3
- CategoryTheory.Pretriangulated.isIso₂_of_isIso₁₃proof · cited by 3
- CategoryTheory.SimplicialObject.Splitting.PInfty_comp_πSummand_idproof · cited by 2
- AlgebraicTopology.DoldKan.QInfty_f_comp_PInfty_fproof · cited by 2
- CategoryTheory.Abelian.SpectralObject.cokernelSequenceE_exactproof · cited by 2
- AlgebraicTopology.DoldKan.Q_f_naturalityproof · cited by 2
- CategoryTheory.ShortComplex.Splitting.s_rproof · cited by 2
- CategoryTheory.Idempotents.idem_of_id_sub_idemproof · cited by 2
- CochainComplex.Lifting.coe_cocycle₁'_v_comp_eq_zeroproof · cited by 2