Theorems · Definition · category theory
CategoryTheory.RetractArrow.op
{C : Type u} →
[inst : CategoryTheory.Category.{v, u} C] →
{X Y Z W : C} → {f : X ⟶ Y} → {g : Z ⟶ W} → CategoryTheory.RetractArrow f g → CategoryTheory.RetractArrow f.op g.opIf a morphism f is a retract of g, then f.op is a retract of g.op.
- Defined in
- Mathlib.CategoryTheory.Retract
- Cited by
- 2 results in Mathlib
- Foundations
- Depth 21 from the axioms · uses propext, Quot.sound
- Assumes
- CategoryTheory.Category
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
- Quiver.Hom.opstatement and proof · cited by 1,948
- CategoryTheory.Arrow.Hom.rightproof · cited by 176
- CategoryTheory.Arrow.Hom.leftproof · cited by 160
- CategoryTheory.Arrow.homMkproof · cited by 35
- CategoryTheory.Retract.rproof · cited by 34
- CategoryTheory.Retract.iproof · cited by 34
- CategoryTheory.RetractArrowstatement and proof · cited by 30
Cited by2
Results whose statement or proof uses this declaration.
- CategoryTheory.RetractArrow.op_istatement and proof · cited by 0
- CategoryTheory.RetractArrow.op_rstatement and proof · cited by 0