Theorems · Inductive type · category theory
CategoryTheory.Arrow.RightHomotopy
{V : Type u_1} →
[inst : CategoryTheory.Category.{v_1, u_1} V] →
[CategoryTheory.Preadditive V] → {u v : CategoryTheory.Arrow V} → (u ⟶ v) → (u ⟶ v) → Type v_1A right homotopy on morphisms in the category of arrows of a preadditive category.
- Cited by
- 22 results in Mathlib
- Foundations
- Depth 14 from the axioms · uses no axioms
Around this declaration
Dashed lines are statement dependencies; solid lines are citations in proofs.
Cites4
Mathlib declarations this one mentions in its statement or cites explicitly in its proof. Plumbing is filtered out.
- CategoryTheory.Categorystatement · cited by 32,673
- Quiver.Homstatement · cited by 32,603
- CategoryTheory.Preadditivestatement · cited by 3,309
- CategoryTheory.Arrowstatement · cited by 713
Cited by44
Results whose statement or proof uses this declaration.
- CategoryTheory.Arrow.RightHomotopy.homstatement and proof · cited by 15
- CategoryTheory.Preadditive.RightFreyd.homotopyOfEqstatement · cited by 4
- CategoryTheory.Preadditive.RightFreyd.eq_of_rightHomotopystatement and proof · cited by 3
- CategoryTheory.Preadditive.RightFreyd.Candidate.descstatement and proof · cited by 2
- CategoryTheory.Arrow.rightHomotopicproof · cited by 1
- CategoryTheory.Preadditive.RightFreyd.Candidate.π_descstatement and proof · cited by 1
- CategoryTheory.Arrow.RightHomotopy.addstatement and proof · cited by 1
- CategoryTheory.Arrow.RightHomotopy.commstatement and proof · cited by 1
- CategoryTheory.Arrow.RightHomotopy.compstatement and proof · cited by 1
- CategoryTheory.Arrow.RightHomotopy.compLeftstatement and proof · cited by 1
- CategoryTheory.Arrow.RightHomotopy.compLeftIdstatement and proof · cited by 1
- CategoryTheory.Arrow.RightHomotopy.compRightstatement and proof · cited by 1