Mathlib Map

Theorems · Definition · category theory

CategoryTheory.CommSq.coconeUnop

{C : Type u_1} →
  [inst : CategoryTheory.Category.{v_1, u_1} C] →
    {W X Y Z : Cᵒᵖ} →
      {f : W ⟶ X} →
        {g : W ⟶ Y} → {h : X ⟶ Z} → {i : Y ⟶ Z} → (p : CategoryTheory.CommSq f g h i) → p.cocone.unop ≅ ⋯.cone

The pullback cone obtained from the pushout cone associated to a commutative square in the opposite category identifies to the cone associated to the flipped square.

Defined in
Mathlib.CategoryTheory.Limits.Shapes.Opposites.Pullbacks
Cited by
1 results in Mathlib
Foundations
Depth 34 from the axioms · uses propext, Classical.choice, Quot.sound
Assumes
CategoryTheory.Category
Mathlib docsSourceLoogleLeanSearch

Around this declaration

Dashed lines are statement dependencies; solid lines are citations in proofs.

CategoryTheory.IsPushout.unop · cited by 4IsPushout.unopCategoryTheory.Category · cited by 32673CategoryTheory.CategoryQuiver.Hom · cited by 32603Quiver.HomOpposite · cited by 8081OppositeCategoryTheory.Iso · cited by 3963CategoryTheory.IsoOpposite.unop · cited by 2231Opposite.unopCategoryTheory.Limits.WalkingPair · cited by 1319Limits.WalkingPairCategoryTheory.Limits.Cone.pt · cited by 1298Cone.ptQuiver.Hom.unop · cited by 903Hom.unopCategoryTheory.Iso.refl · cited by 727Iso.reflCategoryTheory.Limits.WalkingCospan · cited by 496Limits.WalkingCospanCategoryTheory.Limits.cospan · cited by 467Limits.cospanCategoryTheory.CommSq · cited by 158CategoryTheory.CommSqCategoryTheory.Limits.PullbackCone · cited by 136Limits.PullbackConeCategoryTheory.CommSq.flip · cited by 11CommSq.flipCategoryTheory.Limits.PullbackCone.ext · cited by 6PullbackCone.extCommSq.coconeUnopCITED BYCITES

Cites19

Mathlib declarations this one mentions in its statement or cites explicitly in its proof. Plumbing is filtered out.

Cited by1

Results whose statement or proof uses this declaration.