condition — Mathlib

English

Let f: X → Z and g: Y → Z be morphisms in a category, and let t be a pullback cone for f and g with projections fst t : t.pt → X and snd t : t.pt → Y. Then the two legs compose to Z, i.e. fst t; f = snd t; g.

Русский

Пусть f: X → Z и g: Y → Z — морфизмы в категории, и пусть t — пуллбэк-конус к (f, g) с проекциии fst t : t.pt → X и snd t : t.pt → Y. Тогда выполняется тождество fst t ; f = snd t ; g.

LaTeX

$$$fst(t) \\circ f = snd(t) \\circ g$$$

Lean4

@[reassoc]
theorem condition (t : PullbackCone f g) : fst t ≫ f = snd t ≫ g :=
  (t.w inl).trans (t.w inr).symm

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