fac — Mathlib

English

In the product category, any morphism f factors as f = (id × f2) ∘ (f1 × id).

Русский

В произведении категорий любой морфизм разбивается на f = (id × f_2) ∘ (f_1 × id).

LaTeX

$$$f = (\mathrm{id}_{X_1} \times f_2) \circ (f_1 \times \mathrm{id}_{Y_2})$ for $f = ((f_1,f_2))$$$

Lean4

/-- Any morphism in a product factors as a morphsim whose left component is an identity
followed by a morphism whose right component is an identity. -/
@[reassoc]
theorem fac {x y : C × D} (f : x ⟶ y) : f = (𝟙 x.1 ×ₘ f.2) ≫ (f.1 ×ₘ (𝟙 y.2)) := by simp

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