English
Let R, S be commutative semirings and M a suitable module with an S-coalgebra structure, together with the necessary compatibility data. Then the canonical rid map on the coalgebra-tensor-product construction coincides with the rid map arising from the algebra-tensor-module viewpoint; in particular these two canonical linear equivalences are equal.
Русский
Пусть R и S — коммутативные полупрямые кольца, M — подходящая модульная структура с коалгебраной над S и необходимыми совместимостями. Тогда каноническое отображение rid для конструкций тензорного произведения с коалгеброй совпадает с rid, получаемым из подхода с алгебра-тензор-модулем; более точно, две канонические линейные эквивалентности совпадают.
LaTeX
$$$ (\text{Coalgebra.TensorProduct.rid} \, R \, S \, M) = (\text{AlgebraTensorModule.rid} \, R \, S \, M) $$$
Lean4
@[simp]
theorem rid_toLinearEquiv : (Coalgebra.TensorProduct.rid R S M) = AlgebraTensorModule.rid R S M :=
rfl
