lift_fst — Mathlib

English

Let W, X, Y be objects in a category with binary product X × Y. For any morphisms f: W → X and g: W → Y, the product morphism ⟨f,g⟩: W → X × Y satisfies π1 ∘ ⟨f,g⟩ = f, i.e., the first projection composed with the lift yields f.

Русский

Пусть W, X, Y — объекты в категории с бинарным произведением X × Y. Для любых морофизмов f: W → X и g: W → Y выполняется π1 ∘ ⟨f,g⟩ = f, т.е. первая проекция, после подъёма, даёт f.

LaTeX

$$$\\\\pi_1 \\\\\\circ \\\\langle f,g \rangle = f$$$

Lean4

@[reassoc]
theorem lift_fst {W X Y : C} [HasBinaryProduct X Y] (f : W ⟶ X) (g : W ⟶ Y) : prod.lift f g ≫ prod.fst = f :=
  limit.lift_π _ _

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