English
Given a coalgebra A over R, the opposite A^op carries a natural coalgebra structure induced by transporting comul and counit along the linear equivalence with A; i.e., A^op is a coalgebra over R.
Русский
Пусть A — коалгебра над R. Противоположная A^op обладает естественной коалгебраической структурой, полученной переносом comul и counit по линейному эквиваленту между A и A^op; то есть A^op — коалгебра над R.
LaTeX
$$$A^{op}$ is a coalgebra over R with comul_{A^{op}} = map((opLinearEquiv_R).toLinearMap, (opLinearEquiv_R).toLinearMap) \circ comul \circ (opLinearEquiv_R)^{-1},\; counit_{A^{op}} = counit \circ (opLinearEquiv_R)^{-1}. $$$
Lean4
noncomputable instance [Coalgebra R A] : Coalgebra R Aᵐᵒᵖ
where
coassoc :=
ext fun _ => by
rw [comul_def, rTensor_comp, rTensor_comp]
simp only [coe_comp, LinearEquiv.coe_coe, Function.comp_apply, lTensor_map, rTensor_def]
simp_rw [← map_map_assoc, map_map, comp_assoc, ← lTensor_comp_rTensor]
simp [lTensor_tensor, comp_assoc]
rTensor_counit_comp_comul :=
ext fun _ => by
simp only [counit_def, comul_def, coe_comp, Function.comp_apply, rTensor_map, comp_assoc]
simp [← lTensor_comp_rTensor]
lTensor_counit_comp_comul :=
ext fun _ => by
simp only [counit_def, comul_def, coe_comp, Function.comp_apply, lTensor_map, comp_assoc]
simp [← rTensor_comp_lTensor]
