Cocommutative coalgebras #
Cocommutativity descends along surjective coalgebra homomorphisms. In particular, it transfers across coalgebra equivalences without requiring compatible algebra structures.
Main declarations #
CoalgHom.isCocomm_of_surjective: a surjective image of a cocommutative coalgebra is cocommutative.
theorem
CoalgHom.isCocomm_of_surjective
{R : Type u_1}
{A : Type u_2}
{B : Type u_3}
[CommSemiring R]
[AddCommMonoid A]
[AddCommMonoid B]
[Module R A]
[Module R B]
[Coalgebra R A]
[Coalgebra R B]
(f : A →ₗc[R] B)
(hf : Function.Surjective ⇑f)
[hA : Coalgebra.IsCocomm R A]
:
A surjective image of a cocommutative coalgebra is cocommutative.