Theorems · Definition · category theory
CategoryTheory.MorphismProperty.op
{C : Type u} →
[inst : CategoryTheory.CategoryStruct.{v, u} C] →
CategoryTheory.MorphismProperty C → CategoryTheory.MorphismProperty CᵒᵖThe morphism property in Cᵒᵖ associated to a morphism property in C
- Cited by
- 71 results in Mathlib
- Foundations
- Depth 5 from the axioms · 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.
- Quiver.Homproof · cited by 32,603
- Oppositestatement and proof · cited by 8,081
- Opposite.unopproof · cited by 2,231
- CategoryTheory.MorphismPropertystatement and proof · cited by 2,179
- Quiver.Hom.unopproof · cited by 903
- CategoryTheory.CategoryStructstatement and proof · cited by 343
Cited by85
Results whose statement or proof uses this declaration.
- CategoryTheory.LocalizerMorphism.opstatement · cited by 27
- CategoryTheory.MorphismProperty.RightFraction.opstatement · cited by 8
- CategoryTheory.MorphismProperty.LeftFraction.opstatement · cited by 6
- CategoryTheory.LocalizerMorphism.LeftResolution.opstatement · cited by 6
- CategoryTheory.LocalizerMorphism.RightResolution.unopstatement · cited by 6
- CategoryTheory.Localization.exists_rightFractionproof · cited by 5
- CategoryTheory.MorphismProperty.IsInvertedBy.opstatement and proof · cited by 5
- CategoryTheory.LocalizerMorphism.LeftResolution.opEquivalencestatement · cited by 5
- CategoryTheory.LocalizerMorphism.LeftResolution.opFunctorstatement · cited by 4
- CategoryTheory.LocalizerMorphism.LeftResolution.unopstatement · cited by 4
- CategoryTheory.LocalizerMorphism.RightResolution.opstatement · cited by 4
- CategoryTheory.LocalizerMorphism.RightResolution.unopFunctorstatement · cited by 4