English
If A is a coalgebra over R, then Aᵐᵒᵖ gains a Coalgebra structure via transporting comul and counit along the opposite linear equivalence; the comul and counit are defined by conjugation by the opposite equivalence.
Русский
Если A — коалгебра над R, то Aᵐᵒᵖ получает коалгебраическую структуру путём переноса comul и counit через противоположное линейное эквивалентство.
LaTeX
$$$\text{Coalgebra }(R,A^{op}) \text{ with } \mathrm{comul}_{A^{op}} = map( (opLinearEquiv_R).toLinearMap, (opLinearEquiv_R).toLinearMap) \circ\mathrm{comul} \circ (opLinearEquiv_R)^{-1}, \; \mathrm{counit}_{A^{op}} = counit \circ (opLinearEquiv_R)^{-1}.$$$
Lean4
noncomputable instance instCoalgebra : Coalgebra S (A ⊗[R] B)
where
coassoc := coassoc (R := R)
rTensor_counit_comp_comul := by
ext x y
convert
congr((TensorProduct.lid S _).symm
(TensorProduct.lid _ _ $(rTensor_counit_comul (R := S) x) ⊗ₜ[R]
TensorProduct.lid _ _ $(rTensor_counit_comul (R := R) y)))
· dsimp
hopf_tensor_induction comul (R := S) x with x₁ x₂
hopf_tensor_induction comul (R := R) y with y₁ y₂
apply (TensorProduct.lid S _).injective
dsimp
rw [tmul_smul, smul_assoc, one_smul, smul_tmul']
· dsimp
simp only [one_smul]
lTensor_counit_comp_comul := by
ext x y
convert
congr((TensorProduct.rid S _).symm
(TensorProduct.rid _ _ $(lTensor_counit_comul (R := S) x) ⊗ₜ[R]
TensorProduct.rid _ _ $(lTensor_counit_comul (R := R) y)))
· dsimp
hopf_tensor_induction comul (R := S) x with x₁ x₂
hopf_tensor_induction comul (R := R) y with y₁ y₂
apply (TensorProduct.rid S _).injective
dsimp
rw [tmul_smul, smul_assoc, one_smul, smul_tmul']
· dsimp
simp only [one_smul]
