English
If A and B are coalgebras over R, then the cartesian product A × B carries a natural coalgebra structure whose comultiplication and counit are defined from the coalgebra structures of A and B; in particular, Δ((a,b)) = ∑ (a1,b1) ⊗ (a2,b2) and ε(a,b) = ε_A(a) + ε_B(b).
Русский
Пусть A и B — коалгебры над R. Их произведение A × B естественным образом наделяется коалгеброй: копуляция и копунит задаются через копулоги соответствующих факторов, т. е. Δ((a,b)) = ∑ (a1,b1) ⊗ (a2,b2), ε(a,b) = ε_A(a) + ε_B(b).
LaTeX
$$$\text{Coalgebra on } A \times B: \\\Delta_{A\times B}(a,b) = \sum (a_{(1)}, b_{(1)}) \otimes (a_{(2)}, b_{(2)}), \quad \varepsilon_{A\times B}(a,b) = \varepsilon_A(a) + \varepsilon_B(b).$$$
Lean4
instance instCoalgebra : Coalgebra R (A × B)
where
rTensor_counit_comp_comul := by
ext : 1
·
rw [comp_assoc, comul_comp_inl, ← comp_assoc, rTensor_comp_map, counit_comp_inl, ← lTensor_comp_rTensor,
comp_assoc, rTensor_counit_comp_comul, lTensor_comp_mk]
·
rw [comp_assoc, comul_comp_inr, ← comp_assoc, rTensor_comp_map, counit_comp_inr, ← lTensor_comp_rTensor,
comp_assoc, rTensor_counit_comp_comul, lTensor_comp_mk]
lTensor_counit_comp_comul := by
ext : 1
·
rw [comp_assoc, comul_comp_inl, ← comp_assoc, lTensor_comp_map, counit_comp_inl, ← rTensor_comp_lTensor,
comp_assoc, lTensor_counit_comp_comul, rTensor_comp_flip_mk]
·
rw [comp_assoc, comul_comp_inr, ← comp_assoc, lTensor_comp_map, counit_comp_inr, ← rTensor_comp_lTensor,
comp_assoc, lTensor_counit_comp_comul, rTensor_comp_flip_mk]
coassoc := by
dsimp only [instCoalgebraStruct]
ext x : 2 <;> dsimp only [comp_apply, LinearEquiv.coe_coe, coe_inl, coe_inr, coprod_apply]
· simp only [map_zero, add_zero]
simp_rw [← comp_apply, ← comp_assoc, rTensor_comp_map, lTensor_comp_map, coprod_inl, ← map_comp_rTensor, ←
map_comp_lTensor, comp_assoc, ← coassoc, ← comp_assoc, TensorProduct.map_map_comp_assoc_eq, comp_apply,
LinearEquiv.coe_coe]
· simp only [map_zero, zero_add]
simp_rw [← comp_apply, ← comp_assoc, rTensor_comp_map, lTensor_comp_map, coprod_inr, ← map_comp_rTensor, ←
map_comp_lTensor, comp_assoc, ← coassoc, ← comp_assoc, TensorProduct.map_map_comp_assoc_eq, comp_apply,
LinearEquiv.coe_coe]
