hasPullback_of_right — Mathlib

English

If f: X → Z is an open immersion and g: Y → Z is any morphism, then the pullback of g and f exists; i.e., Y ×_Z X exists with projections to Y and X commuting with g and f.

Русский

Если f: X → Z является открытым вложением и g: Y → Z — произвольный морфизм, то существует произведение по основанию g и f; то есть Y ×_Z X существует с проекциями на Y и X, удовлетворяющими коммутативности с g и f.

LaTeX

$$$\text{HasPullback}(g,f)$$$

Lean4

instance hasPullback_of_right : HasPullback g f :=
  hasPullback_symmetry f g

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