Descent of group-like elements

Being group-like can be checked after faithfully flat extension of scalars. This allows a character whose coefficients lie in a smaller field to be regarded as a character over that field.

@[simp]

theorem TauCeti.isGroupLikeElem_one_tmul_iff {R : Type u_1} {K : Type u_2} {C : Type u_3} [CommRing R] [CommRing K] [Algebra R K] [Module.FaithfullyFlat R K] [AddCommGroup C] [Module R C] [Coalgebra R C] (x : C) : IsGroupLikeElem K (1 ⊗ₜ[R] x) ↔ IsGroupLikeElem R x

An element of a coalgebra is group-like if and only if it is group-like after faithfully flat extension of scalars.