Group-like elements in a coalgebra

This file defines group-like elements in a coalgebra, i.e. elements a such that ε a = 1 and Δ a = a ⊗ₜ a.

Main declarations

• IsGroupLikeElem: Predicate for an element in a coalgebra to be group-like.
• linearIndepOn_isGroupLikeElem: Group-like elements over a domain are linearly independent.

structure IsGroupLikeElem (R : Type u_2) {A : Type u_3} [CommSemiring R] [AddCommMonoid A] [Module R A] [Coalgebra R A] (a : A) : Prop

A group-like element in a coalgebra is an element a such that ε(a) = 1 and Δ(a) = a ⊗ₜ a, where ε and Δ are the counit and comultiplication respectively.

• counit_eq_one : CoalgebraStruct.counit a = 1

  A group-like element a satisfies ε(a) = 1.

• comul_eq_tmul_self : CoalgebraStruct.comul a = a ⊗ₜ[R] a

  A group-like element a satisfies Δ(a) = a ⊗ₜ a.

theorem isGroupLikeElem_iff (R : Type u_2) {A : Type u_3} [CommSemiring R] [AddCommMonoid A] [Module R A] [Coalgebra R A] (a : A) : IsGroupLikeElem R a ↔ CoalgebraStruct.counit a = 1 ∧ CoalgebraStruct.comul a = a ⊗ₜ[R] a

@[simp]

theorem isGroupLikeElem_self {R : Type u_2} [CommSemiring R] {r : R} : IsGroupLikeElem R r ↔ r = 1

theorem IsGroupLikeElem.ne_zero {R : Type u_2} {A : Type u_3} [CommSemiring R] [AddCommMonoid A] [Module R A] [Coalgebra R A] {a : A} [Nontrivial R] (ha : IsGroupLikeElem R a) : a ≠ 0

theorem IsGroupLikeElem.map {F : Type u_1} {R : Type u_2} {A : Type u_3} {B : Type u_4} [CommSemiring R] [AddCommMonoid A] [AddCommMonoid B] [Module R A] [Coalgebra R A] [Module R B] [Coalgebra R B] {a : A} [FunLike F A B] [CoalgHomClass F R A B] (f : F) (ha : IsGroupLikeElem R a) : IsGroupLikeElem R (f a)

A coalgebra homomorphism sends group-like elements to group-like elements.

@[simp]

theorem isGroupLikeElem_map_equiv {F : Type u_1} {R : Type u_2} {A : Type u_3} {B : Type u_4} [CommSemiring R] [AddCommMonoid A] [AddCommMonoid B] [Module R A] [Coalgebra R A] [Module R B] [Coalgebra R B] {a : A} [EquivLike F A B] [CoalgEquivClass F R A B] (f : F) : IsGroupLikeElem R (f a) ↔ IsGroupLikeElem R a

A coalgebra isomorphism preserves group-like elements.

structure GroupLike (R : Type u_2) (A : Type u_3) [CommSemiring R] [AddCommMonoid A] [Module R A] [Coalgebra R A] : Type u_3

The type of group-like elements in a coalgebra.

• val : A

  The underlying element of a group-like element.

• isGroupLikeElem_val : IsGroupLikeElem R ↑self

theorem GroupLike.ext_iff {R : Type u_2} {A : Type u_3} {inst✝ : CommSemiring R} {inst✝¹ : AddCommMonoid A} {inst✝² : Module R A} {inst✝³ : Coalgebra R A} {x y : GroupLike R A} : x = y ↔ ↑x = ↑y

theorem GroupLike.ext {R : Type u_2} {A : Type u_3} {inst✝ : CommSemiring R} {inst✝¹ : AddCommMonoid A} {inst✝² : Module R A} {inst✝³ : Coalgebra R A} {x y : GroupLike R A} (val : ↑x = ↑y) : x = y

instance GroupLike.instCoeOut {R : Type u_2} {A : Type u_3} [CommSemiring R] [AddCommMonoid A] [Module R A] [Coalgebra R A] : CoeOut (GroupLike R A) A

theorem GroupLike.val_injective {R : Type u_2} {A : Type u_3} [CommSemiring R] [AddCommMonoid A] [Module R A] [Coalgebra R A] : Function.Injective val

@[simp]

theorem GroupLike.val_inj {R : Type u_2} {A : Type u_3} [CommSemiring R] [AddCommMonoid A] [Module R A] [Coalgebra R A] {a b : GroupLike R A} : ↑a = ↑b ↔ a = b

def GroupLike.valEquiv {R : Type u_2} {A : Type u_3} [CommSemiring R] [AddCommMonoid A] [Module R A] [Coalgebra R A] : GroupLike R A ≃ Subtype (IsGroupLikeElem R)

Identity equivalence between GroupLike R A and {a : A // IsGroupLikeElem R a}.

theorem linearIndepOn_isGroupLikeElem {R : Type u_2} {A : Type u_3} [CommRing R] [IsDomain R] [AddCommGroup A] [Module R A] [Coalgebra R A] [Module.IsTorsionFree R A] : LinearIndepOn R id {a : A | IsGroupLikeElem R a}

Group-like elements over a domain are linearly independent.

theorem linearIndep_groupLikeVal {R : Type u_2} {A : Type u_3} [CommRing R] [IsDomain R] [AddCommGroup A] [Module R A] [Coalgebra R A] [Module.IsTorsionFree R A] : LinearIndependent R GroupLike.val

Group-like elements over a domain are linearly independent.