hasPullbacks_opposite — Mathlib

English

If C has pushouts, then Opposite C has pullbacks.

Русский

Если в категории C существуют pushouts, то в противоположной категории C есть pullbacks.

LaTeX

$$$${\text{HasPullbacks}(C^{\mathrm{op}}) \,=\, \text{HasPushouts}(C)}.$$$$

Lean4

instance hasPullbacks_opposite [HasPushouts C] : HasPullbacks Cᵒᵖ :=
  by
  haveI : HasColimitsOfShape WalkingCospanᵒᵖ C := hasColimitsOfShape_of_equivalence walkingCospanOpEquiv.symm
  apply hasLimitsOfShape_op_of_hasColimitsOfShape

Похожие утверждения