pullbackIsoProdSubtype_inv_fst_apply

English

Let f: X -> Z and g: Y -> Z. For any x in the subtype of X × Y with f(x₁) = g(x₂), the first projection of the inverse image along the iso yields the first component of x.

Русский

Пусть f: X → Z и g: Y → Z. Для любого элемента x в подтипе X × Y с условием f(x₁) = g(x₂) проекция fst применённая к инверсии изопары возвращает первую компоненту пары x.

LaTeX

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

Lean4

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

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