map — Mathlib

English

If h is a pullback in C and F preserves the relevant limit, then the mapped square sq.map F is a pullback in D.

Русский

Если h является квадратом-подобным пределом в C и F сохраняет соответствующий предел, то квадрат sq.map F является квадратом-подобным пределом в D.

LaTeX

$$$\\text{IsPullback}(sq) \\;\n\\land\\; \\text{PreservesLimit}(\\operatorname{cospan} sq.f_{24} sq.f_{34}, F) \\Rightarrow \\text{IsPullback}( (sq.map F) ).$$$

Lean4

theorem map (h : sq.IsPullback) (F : C ⥤ D) [PreservesLimit (cospan sq.f₂₄ sq.f₃₄) F] : (sq.map F).IsPullback :=
  Square.IsPullback.mk _ (isLimitPullbackConeMapOfIsLimit F sq.fac h.isLimit)

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