English
Coalgebra equivalences are symmetric: given e: A ≃ₗc[R] B, there exists e.symm: B ≃ₗc[R] A, which is a coalgebra equivalence.
Русский
Коалгебраические эквивалентности симметричны: для e: A ≃ₗc[R] B существует e.symm: B ≃ₗc[R] A, которое является коалгебраической эквивалентностью.
LaTeX
$$$e : A \\simeq_{\\ell_c[R]} B \\Rightarrow e^{\\mathrm{symm}} : B \\simeq_{\\ell_c[R]} A$$$
Lean4
/-- Coalgebra equivalences are symmetric. -/
@[symm]
def symm (e : A ≃ₗc[R] B) : B ≃ₗc[R] A :=
{
(e : A ≃ₗ[R]
B).symm with
counit_comp := (LinearEquiv.comp_toLinearMap_symm_eq _ _).2 e.counit_comp.symm
map_comp_comul :=
by
change
(TensorProduct.congr (e : A ≃ₗ[R] B) (e : A ≃ₗ[R] B)).symm.toLinearMap ∘ₗ comul = comul ∘ₗ (e : A ≃ₗ[R] B).symm
rw [LinearEquiv.toLinearMap_symm_comp_eq]
simp only [TensorProduct.congr, toLinearEquiv_toLinearMap, LinearEquiv.ofLinear_toLinearMap,
← LinearMap.comp_assoc, CoalgHomClass.map_comp_comul, LinearEquiv.eq_comp_toLinearMap_symm] }
