Theorems · Definition · category theory
CategoryTheory.Limits.widePushoutShapeOp
(J : Type w) → CategoryTheory.Functor (CategoryTheory.Limits.WidePushoutShape J) (CategoryTheory.Limits.WidePullbackShape J)ᵒᵖ
The obvious functor WidePushoutShape J ⥤ (WidePullbackShape J)ᵒᵖ
- Cited by
- 11 results in Mathlib
- Foundations
- Depth 18 from the axioms · uses propext, Quot.sound
Around this declaration
Dashed lines are statement dependencies; solid lines are citations in proofs.
Cites5
Mathlib declarations this one mentions in its statement or cites explicitly in its proof. Plumbing is filtered out.
- CategoryTheory.Functorstatement · cited by 16,252
- Oppositestatement · cited by 8,081
- CategoryTheory.Limits.WidePullbackShapestatement · cited by 94
- CategoryTheory.Limits.WidePushoutShapestatement and proof · cited by 47
- CategoryTheory.Limits.widePushoutShapeOpMapproof · cited by 4
Cited by15
Results whose statement or proof uses this declaration.
- CategoryTheory.Limits.widePushoutShapeUnopproof · cited by 9
- CategoryTheory.Limits.widePullbackShapeOpEquivproof · cited by 6
- CategoryTheory.Limits.widePullbackShapeOpUnopstatement and proof · cited by 1
- CategoryTheory.Limits.widePushoutShapeUnopOpstatement and proof · cited by 1
- CategoryTheory.Limits.walkingCospanOpEquiv_counitIso_hom_appstatement · cited by 0
- CategoryTheory.Limits.walkingCospanOpEquiv_counitIso_inv_appstatement · cited by 0
- CategoryTheory.Limits.widePullbackShapeOpEquiv_counitIsostatement · cited by 0
- CategoryTheory.Limits.walkingCospanOpEquiv_unitIso_hom_appstatement · cited by 0
- CategoryTheory.Limits.walkingCospanOpEquiv_unitIso_inv_appstatement · cited by 0
- CategoryTheory.Limits.widePullbackShapeOpEquiv_inversestatement · cited by 0
- CategoryTheory.Limits.widePullbackShapeOpEquiv_unitIsostatement · cited by 0
- CategoryTheory.Limits.widePushoutShapeOp_mapstatement and proof · cited by 0