hasPullbackVertPaste — Mathlib

English

There exists a pullback of f and g'∘g, constructed by vertically pasting pullbacks, assuming appropriate pullbacks exist.

Русский

Существуют пуллбек f и g'∘g, склеенные вертикально через pasting, при условии существования соответствующих пуллбеков.

LaTeX

$$$\\mathrm{HasPullback}(f,\\; g'\\circ g)$$$

Lean4

instance hasPullbackVertPaste : HasPullback f (g' ≫ g) :=
  HasLimit.mk
    { cone := (pullback.cone f g).pasteVert (pullback.cone (pullback.snd f g) g') rfl
      isLimit := pasteVertIsPullback rfl (pullback.isLimit f g) (pullback.isLimit (pullback.snd f g) g') }

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