Theorems · Definition · category theory

CategoryTheory.Limits.PullbackCone.isLimitEquivIsColimitUnop

{C : Type u₁} →
  [inst : CategoryTheory.Category.{v₁, u₁} C] →
    {X Y Z : Cᵒᵖ} →
      {f : X ⟶ Z} →
        {g : Y ⟶ Z} →
          (c : CategoryTheory.Limits.PullbackCone f g) →
            CategoryTheory.Limits.IsLimit c ≃ CategoryTheory.Limits.IsColimit c.unop

A pullback cone is a limit cone in Cᵒᵖ if and only if the corresponding pushout cocone in C is a colimit cocone.

Defined in

Mathlib.CategoryTheory.Limits.Shapes.Opposites.Pullbacks

Cited by

3 results in Mathlib

Foundations

Depth 38 from the axioms · uses propext, Classical.choice, Quot.sound

Assumes

CategoryTheory.Category