Theorems · Definition · category theory
CategoryTheory.ShortComplex.f
{C : Type u_1} →
[inst : CategoryTheory.Category.{v_1, u_1} C] →
[inst_1 : CategoryTheory.Limits.HasZeroMorphisms C] → (self : CategoryTheory.ShortComplex C) → self.X₁ ⟶ self.X₂the first morphism of a ShortComplex
- Cited by
- 653 results in Mathlib
- Foundations
- Depth 4 from the axioms, rests on 11 definitions · uses no axioms
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 · cited by 32,603
- CategoryTheory.Limits.HasZeroMorphismsstatement and proof · cited by 3,275
- CategoryTheory.ShortComplexstatement and proof · cited by 1,850
- CategoryTheory.ShortComplex.X₂statement · cited by 1,115
- CategoryTheory.ShortComplex.X₁statement · cited by 889
Cited by820
Results whose statement or proof uses this declaration.
- CategoryTheory.ShortComplex.mapproof · cited by 188
- CategoryTheory.ShortComplex.opproof · cited by 88
- CategoryTheory.ShortComplex.zerostatement · cited by 76
- CategoryTheory.ShortComplex.LeftHomologyData.f'proof · cited by 61
- CategoryTheory.ShortComplex.unopproof · cited by 44
- CategoryTheory.ShortComplex.ShortExact.extClassproof · cited by 36
- CategoryTheory.ShortComplex.isoMkstatement and proof · cited by 30
- CategoryTheory.ShortComplex.ShortExact.singleTriangleproof · cited by 26
- CategoryTheory.ShortComplex.exact_of_g_is_cokernelstatement · cited by 25
- CategoryTheory.ShortComplex.LeftHomologyData.mapproof · cited by 25
- CategoryTheory.ShortComplex.RightHomologyData.mapproof · cited by 23
- CategoryTheory.ShortComplex.ShortExact.map_of_exactproof · cited by 23
Showing the 200 most cited of 820.