Theorems · Definition · category theory
CategoryTheory.MorphismProperty.MapFactorizationData.op
{C : Type u_1} →
[inst : CategoryTheory.Category.{v_1, u_1} C] →
(W₁ W₂ : CategoryTheory.MorphismProperty C) →
{X Y : C} → {f : X ⟶ Y} → W₁.MapFactorizationData W₂ f → W₂.op.MapFactorizationData W₁.op f.opThe opposite of a factorization.
- Cited by
- 4 results in Mathlib
- Foundations
- Depth 13 from the axioms · uses propext
- Assumes
- CategoryTheory.Category
Around this declaration
Dashed lines are statement dependencies; solid lines are citations in proofs.
Cites12
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.MorphismPropertystatement and proof · cited by 2,179
- Quiver.Hom.opstatement and proof · cited by 1,948
- CategoryTheory.MorphismProperty.opstatement · cited by 71
- CategoryTheory.MorphismProperty.MapFactorizationData.Zproof · cited by 63
- CategoryTheory.MorphismProperty.MapFactorizationDatastatement and proof · cited by 63
- CategoryTheory.MorphismProperty.MapFactorizationData.iproof · cited by 36
- CategoryTheory.MorphismProperty.MapFactorizationData.pproof · cited by 36
- CategoryTheory.MorphismProperty.MapFactorizationData.hiproof · cited by 7
- CategoryTheory.MorphismProperty.MapFactorizationData.hpproof · cited by 7
Cited by5
Results whose statement or proof uses this declaration.
- CategoryTheory.MorphismProperty.MapFactorizationData.opEquivproof · cited by 2
- CategoryTheory.MorphismProperty.MapFactorizationData.opEquiv_applystatement · cited by 0
- CategoryTheory.MorphismProperty.MapFactorizationData.op_Zstatement and proof · cited by 0
- CategoryTheory.MorphismProperty.MapFactorizationData.op_istatement and proof · cited by 0
- CategoryTheory.MorphismProperty.MapFactorizationData.op_pstatement and proof · cited by 0