English
Let R be a commutative semiring and A, B be coalgebras over R. For the product coalgebra A × B, the comultiplication is compatible with the first projection fst in the sense that comul followed by fst equals the map that applies fst to both tensor factors after comul.
Русский
Пусть R — коммутативное полукольцо, A и B — коалгебры над R. Для произведения коалгебр A × B комул совместим с проекцией на первую компоненту: после применения fst к комулю следует применить тот же fst к обоим тensor-коэффициентам.
LaTeX
$$$ \\mathrm{comul} \\circ \\mathrm{fst}_{R,A,B} = \\big( \\mathrm{TensorProduct.map} (\\mathrm{fst}_{R,A,B}) (\\mathrm{fst}_{R,A,B}) \\big) \\circ \\mathrm{comul} $$$
Lean4
theorem comul_comp_fst : comul ∘ₗ .fst R A B = TensorProduct.map (.fst R A B) (.fst R A B) ∘ₗ comul :=
by
ext : 1
·
rw [comp_assoc, fst_comp_inl, comp_id, comp_assoc, comul_comp_inl, ← comp_assoc, ← TensorProduct.map_comp,
fst_comp_inl, TensorProduct.map_id, id_comp]
·
rw [comp_assoc, fst_comp_inr, comp_zero, comp_assoc, comul_comp_inr, ← comp_assoc, ← TensorProduct.map_comp,
fst_comp_inr, TensorProduct.map_zero_left, zero_comp]
