English
A coalgebra equivalence between A and B induces a coalgebra structure on B compatible with the equivalence, making the equivalence a coalgebra isomorphism.
Русский
Коалгебраическое эквивалентное отображение между A и B порождает коалгебраическую структуру на B, совместимую с эквивалентностью, делая её коалгебраическим изоморфизмом.
LaTeX
$$$\\text{toCoalgebra}(f) : \\text{Coalgebra } R B$$$
Lean4
/-- Let `A` be an `R`-coalgebra and let `B` be an `R`-module with a `CoalgebraStruct`.
A linear equivalence `A ≃ₗ[R] B` that respects the `CoalgebraStruct`s defines an `R`-coalgebra
structure on `B`. -/
@[reducible]
def toCoalgebra (f : A ≃ₗc[R] B) : Coalgebra R B
where
coassoc :=
by
simp only [← ((f : A ≃ₗ[R] B).comp_toLinearMap_symm_eq _ _).2 f.map_comp_comul, ← LinearMap.comp_assoc]
congr 1
ext x
simpa only [toCoalgHom_eq_coe, CoalgHom.toLinearMap_eq_coe, LinearMap.coe_comp, LinearEquiv.coe_coe,
Function.comp_apply, ← (ℛ R _).eq, map_sum, TensorProduct.map_tmul, LinearMap.coe_coe, CoalgHom.coe_coe,
LinearMap.rTensor_tmul, coe_symm_toLinearEquiv, symm_apply_apply, LinearMap.lTensor_comp_map,
TensorProduct.sum_tmul, TensorProduct.assoc_tmul, TensorProduct.tmul_sum] using
(sum_map_tmul_tmul_eq f f f x).symm
rTensor_counit_comp_comul :=
by
simp_rw [(f.toLinearEquiv.eq_comp_toLinearMap_symm _ _).2 f.counit_comp, ←
(f.toLinearEquiv.comp_toLinearMap_symm_eq _ _).2 f.map_comp_comul, ← LinearMap.comp_assoc,
f.toLinearEquiv.comp_toLinearMap_symm_eq]
ext x
simp [← (ℛ R _).eq, coe_symm_toLinearEquiv]
lTensor_counit_comp_comul :=
by
simp_rw [(f.toLinearEquiv.eq_comp_toLinearMap_symm _ _).2 f.counit_comp, ←
(f.toLinearEquiv.comp_toLinearMap_symm_eq _ _).2 f.map_comp_comul, ← LinearMap.comp_assoc,
f.toLinearEquiv.comp_toLinearMap_symm_eq]
ext x
simp [← (ℛ R _).eq, coe_symm_toLinearEquiv]
