fac' — Mathlib

English

A dual decomposition states f = (f1 × id) ∘ (id × f2).

Русский

Двойная факторизация: f = (f_1 × id) ∘ (id × f_2).

LaTeX

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

Lean4

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

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