pullbackIsoProdSubtype_inv_snd_apply

English

Let f: X -> Z and g: Y -> Z, and x a point of the pullback subtype. The image of x under the inverse iso composed with snd equals the second coordinate of x.

Русский

Пусть f: X → Z, g: Y → Z и x — точка подтипа pullback. Образ x под inv ∘ snd даёт вторую координату пары x.

LaTeX

$$$ pullback.snd\, f\, g\big((pullbackIsoProdSubtype\, f\, g)^{-1} x\big) = (x : X \times Y).snd $$$

Lean4

theorem pullbackIsoProdSubtype_inv_snd_apply (f : X ⟶ Z) (g : Y ⟶ Z) (x : { p : X × Y // f p.1 = g p.2 }) :
    pullback.snd f g ((pullbackIsoProdSubtype f g).inv x) = (x : X × Y).snd :=
  ConcreteCategory.congr_hom (pullbackIsoProdSubtype_inv_snd f g) x

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