pullbackFst — Mathlib

English

The first projection from the pullback object pb(f,g) is the morphism induced by the map on underlying pairs to the first coordinate.

Русский

Первая проекция из множества-подобъекта pullback pb(f,g) задаётся отображением, возвращающим первую координату пары.

LaTeX

$$$\\mathrm{pullbackFst}(f,g) : \\mathrm{TopCat.of}\\{ p:(X×Y)\\mid f p.1 = g p.2\\} \\to X$$$

Lean4

/-- The first projection from the pullback. -/
abbrev pullbackFst (f : X ⟶ Z) (g : Y ⟶ Z) : TopCat.of { p : X × Y // f p.1 = g p.2 } ⟶ X :=
  ofHom ⟨Prod.fst ∘ Subtype.val, by fun_prop⟩

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