Elements whose comultiplication is a single tensor

If the comultiplication of an element a of a coalgebra is the pure tensor a ⊗ c, then the counit law (ε ⊗ id) ∘ Δ = id collapses the coalgebra structure at a: applying it to Δ a = a ⊗ c gives a = ε(a) • c. In particular an element fixed by the regular coaction, Δ a = a ⊗ 1, is the scalar multiple ε(a) • 1 of the identity.

Main declarations

• TauCeti.Coalgebra.eq_counit_smul_of_comul_eq_tmul: Δ a = a ⊗ c implies a = ε(a) • c.

References

• M. E. Sweedler, Hopf Algebras, Chapter 1.

theorem TauCeti.Coalgebra.eq_counit_smul_of_comul_eq_tmul {R : Type u} {A : Type v} [CommSemiring R] [AddCommMonoid A] [Module R A] [Coalgebra R A] {a c : A} (h : CoalgebraStruct.comul a = a ⊗ₜ[R] c) : a = CoalgebraStruct.counit a • c

An element whose comultiplication is the pure tensor a ⊗ c is the scalar multiple of c by its counit.