Theorems · Theorem · category theory
CategoryTheory.ObjectProperty.limitsOfShape_eq_unop_colimitsOfShape
∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] (P : CategoryTheory.ObjectProperty C) (J : Type u')
[inst_1 : CategoryTheory.Category.{v', u'} J], P.limitsOfShape J = (P.op.colimitsOfShape Jᵒᵖ).unop- Cited by
- 2 results in Mathlib
- Foundations
- Depth 27 from the axioms · uses propext, Classical.choice, Quot.sound
Around this declaration
Dashed lines are statement dependencies; solid lines are citations in proofs.
Cites26
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
- Oppositestatement and proof · cited by 8,081
- Opposite.unopproof · cited by 2,231
- CategoryTheory.Functor.opproof · cited by 997
- CategoryTheory.ObjectPropertystatement and proof · cited by 798
- CategoryTheory.Functor.unopproof · cited by 138
- CategoryTheory.Limits.ColimitPresentation.diagproof · cited by 62
- CategoryTheory.ObjectProperty.opstatement and proof · cited by 42
- CategoryTheory.NatTrans.opproof · cited by 41
- CategoryTheory.ObjectProperty.colimitsOfShapestatement and proof · cited by 35
- CategoryTheory.Limits.ColimitPresentation.ιproof · cited by 33
- CategoryTheory.Limits.LimitPresentation.diagproof · cited by 32
Cited by2
Results whose statement or proof uses this declaration.
- CategoryTheory.ObjectProperty.isClosedUnderLimitsOfShape_iff_opproof · cited by 1
- CategoryTheory.ObjectProperty.colimitsOfShape_opproof · cited by 1