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 second projection snd in the sense that comul followed by snd equals the map that applies snd to both tensor factors after comul.
Русский
Пусть R — коммутативное полукольцо, A и B — коалгебры над R. Для произведения коалгебр A × B комул совместим с проекцией на вторую компоненту: после применения snd к комулю следует применить тот же snd к обоим тензорным компонентам.
LaTeX
$$$ \\mathrm{comul} \\circ \\mathrm{snd}_{R,A,B} = \\big( \\mathrm{TensorProduct.map} (\\mathrm{snd}_{R,A,B}) (\\mathrm{snd}_{R,A,B}) \\big) \\circ \\mathrm{comul} $$$
Lean4
theorem comul_comp_snd : comul ∘ₗ .snd R A B = TensorProduct.map (.snd R A B) (.snd R A B) ∘ₗ comul :=
by
ext : 1
·
rw [comp_assoc, snd_comp_inl, comp_zero, comp_assoc, comul_comp_inl, ← comp_assoc, ← TensorProduct.map_comp,
snd_comp_inl, TensorProduct.map_zero_left, zero_comp]
·
rw [comp_assoc, snd_comp_inr, comp_id, comp_assoc, comul_comp_inr, ← comp_assoc, ← TensorProduct.map_comp,
snd_comp_inr, TensorProduct.map_id, id_comp]
