Theorems · Definition · category theory
CategoryTheory.ShortComplex.opMap
{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₂) → (S₂.op ⟶ S₁.op)The opposite morphism in ShortComplex Cᵒᵖ associated to a morphism in ShortComplex C
- Cited by
- 42 results in Mathlib
- Foundations
- Depth 17 from the axioms · uses propext, Quot.sound
Around this declaration
Dashed lines are statement dependencies; solid lines are citations in proofs.
Cites10
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
- Oppositestatement · cited by 8,081
- CategoryTheory.Limits.HasZeroMorphismsstatement and proof · cited by 3,275
- Quiver.Hom.opproof · cited by 1,948
- CategoryTheory.ShortComplexstatement and proof · cited by 1,850
- CategoryTheory.ShortComplex.Hom.τ₂proof · cited by 243
- CategoryTheory.ShortComplex.Hom.τ₃proof · cited by 197
- CategoryTheory.ShortComplex.Hom.τ₁proof · cited by 194
- CategoryTheory.ShortComplex.opstatement · cited by 88
Cited by50
Results whose statement or proof uses this declaration.
- CategoryTheory.ShortComplex.SnakeInput.opproof · cited by 10
- CategoryTheory.ShortComplex.RightHomologyData.ofEpiOfIsIsoOfMonoproof · cited by 9
- CategoryTheory.ShortComplex.RightHomologyData.ofEpiOfIsIsoOfMono'proof · cited by 9
- CategoryTheory.ShortComplex.opFunctorproof · cited by 8
- CategoryTheory.ShortComplex.quasiIso_opMap_iffstatement and proof · cited by 4
- CategoryTheory.ShortComplex.LeftHomologyMapData.opstatement · cited by 4
- CategoryTheory.ShortComplex.HomologyMapData.opstatement · cited by 4
- CategoryTheory.ShortComplex.Homotopy.opstatement · cited by 4
- CategoryTheory.ShortComplex.RightHomologyMapData.opstatement · cited by 4
- CategoryTheory.ShortComplex.cyclesOpIso_inv_naturalitystatement and proof · cited by 3
- CategoryTheory.ShortComplex.cyclesOpIso_hom_naturalitystatement and proof · cited by 2
- CategoryTheory.ShortComplex.opMap_τ₂statement and proof · cited by 2