isPullback_iff_map_coyoneda_isPullback

English

A square is a pullback iff its coyoneda-map‑images are pullbacks for all objects X.

Русский

Квадрат является pullback тогда и только тогда, когда все изображения через coyoneda являются pullback.

LaTeX

$$$\\text{IsPullback}(sq) \\iff \\forall X, \\; (\\text{sq.map}(\\mathrm{coyoneda.obj} X)).IsPullback.$$$

Lean4

theorem isPullback_iff_map_coyoneda_isPullback : sq.IsPullback ↔ ∀ (X : Cᵒᵖ), (sq.map (coyoneda.obj X)).IsPullback :=
  ⟨fun h _ ↦ h.map _, fun h ↦ IsPullback.mk _ ((sq.pullbackCone.isLimitCoyonedaEquiv).symm (fun X ↦ (h X).isLimit))⟩

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