Skew-primitive elements in a coalgebra

This file defines (g, h)-skew-primitive elements in a coalgebra, i.e. elements a such that ε a = 0 and Δ a = g ⊗ₜ a + a ⊗ₜ h, for group-like elements g and h.

Main declarations

• Coalgebra.IsSkewPrimitiveElem R g h a: a is (g, h)-skew-primitive.
• Coalgebra.skewPrimitive R g h: the (g, h)-skew-primitive elements as a submodule.

TODO

• g - h is (g, h)-skew-primitive, and the quotient of skewPrimitive R g h by R ∙ (g - h) is Ext¹(h, g), where g and h are regarded as one-dimensional right comodules.

References

• P. Etingof, S. Gelaki, D. Nikshych, V. Ostrik, Tensor categories

structure Coalgebra.IsSkewPrimitiveElem (R : Type u_2) {A : Type u_3} [CommSemiring R] [AddCommMonoid A] [Module R A] [Coalgebra R A] (g h a : A) : Prop

An element a of a coalgebra is (g, h)-skew-primitive if ε a = 0 and Δ a = g ⊗ₜ a + a ⊗ₜ h, where ε and Δ are the counit and comultiplication respectively.

• counit_eq_zero : counit a = 0

  A skew-primitive element a satisfies ε(a) = 0.

• comul_eq_tmul_add_tmul : comul a = g ⊗ₜ[R] a + a ⊗ₜ[R] h

  A (g, h)-skew-primitive element a satisfies Δ(a) = g ⊗ₜ a + a ⊗ₜ h.

theorem Coalgebra.isSkewPrimitiveElem_iff (R : Type u_2) {A : Type u_3} [CommSemiring R] [AddCommMonoid A] [Module R A] [Coalgebra R A] (g h a : A) : IsSkewPrimitiveElem R g h a ↔ counit a = 0 ∧ comul a = g ⊗ₜ[R] a + a ⊗ₜ[R] h

@[simp]

theorem Coalgebra.IsSkewPrimitiveElem.zero {R : Type u_2} {A : Type u_3} [CommSemiring R] [AddCommMonoid A] [Module R A] [Coalgebra R A] {g h : A} : IsSkewPrimitiveElem R g h 0

theorem Coalgebra.IsSkewPrimitiveElem.add {R : Type u_2} {A : Type u_3} [CommSemiring R] [AddCommMonoid A] [Module R A] [Coalgebra R A] {g h a b : A} (ha : IsSkewPrimitiveElem R g h a) (hb : IsSkewPrimitiveElem R g h b) : IsSkewPrimitiveElem R g h (a + b)

theorem Coalgebra.IsSkewPrimitiveElem.smul {R : Type u_2} {A : Type u_3} [CommSemiring R] [AddCommMonoid A] [Module R A] [Coalgebra R A] {g h a : A} (ha : IsSkewPrimitiveElem R g h a) (r : R) : IsSkewPrimitiveElem R g h (r • a)

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

A coalgebra homomorphism sends (g, h)-skew-primitive elements to (f g, f h)-skew-primitive elements.

@[simp]

theorem Coalgebra.isSkewPrimitiveElem_map_equiv {F : Type u_1} {R : Type u_2} {A : Type u_3} {B : Type u_4} [CommSemiring R] [AddCommMonoid A] [Module R A] [Coalgebra R A] [AddCommMonoid B] [Module R B] [Coalgebra R B] {g h a : A} [EquivLike F A B] [CoalgEquivClass F R A B] (f : F) : IsSkewPrimitiveElem R (f g) (f h) (f a) ↔ IsSkewPrimitiveElem R g h a

A coalgebra isomorphism preserves skew-primitivity.

def Coalgebra.skewPrimitive (R : Type u_2) {A : Type u_3} [CommSemiring R] [AddCommMonoid A] [Module R A] [Coalgebra R A] (g h : A) : Submodule R A

The (g, h)-skew-primitive elements form a submodule.

Equations

• Coalgebra.skewPrimitive R g h = { carrier := {a : A | Coalgebra.IsSkewPrimitiveElem R g h a}, add_mem' := ⋯, zero_mem' := ⋯, smul_mem' := ⋯ }

@[simp]

theorem Coalgebra.mem_skewPrimitive {R : Type u_2} {A : Type u_3} [CommSemiring R] [AddCommMonoid A] [Module R A] [Coalgebra R A] {g h a : A} : a ∈ skewPrimitive R g h ↔ IsSkewPrimitiveElem R g h a

theorem Coalgebra.counit_eq_zero_of_comul_eq_tmul_add_tmul {R : Type u_2} {A : Type u_3} [CommSemiring R] [AddCommMonoid A] [Module R A] [Coalgebra R A] {g h a : A} [IsCancelAdd A] (hg : counit g = 1) (hh : counit h = 1) (ha : comul a = g ⊗ₜ[R] a + a ⊗ₜ[R] h) : counit a = 0

When g and h have counit 1 (e.g. when they are group-like), the counit condition follows from the comultiplication condition.

theorem Coalgebra.IsSkewPrimitiveElem.of_comul_eq_tmul_add_tmul {R : Type u_2} {A : Type u_3} [CommSemiring R] [AddCommMonoid A] [Module R A] [Coalgebra R A] {g h a : A} [IsCancelAdd A] (hg : counit g = 1) (hh : counit h = 1) (ha : comul a = g ⊗ₜ[R] a + a ⊗ₜ[R] h) : IsSkewPrimitiveElem R g h a

theorem Coalgebra.isSkewPrimitiveElem_iff_comul_eq_tmul_add_tmul {R : Type u_2} {A : Type u_3} [CommSemiring R] [AddCommMonoid A] [Module R A] [Coalgebra R A] {g h a : A} [IsCancelAdd A] (hg : counit g = 1) (hh : counit h = 1) : IsSkewPrimitiveElem R g h a ↔ comul a = g ⊗ₜ[R] a + a ⊗ₜ[R] h

theorem Coalgebra.IsSkewPrimitiveElem.neg {R : Type u_2} {A : Type u_3} [CommSemiring R] [AddCommGroup A] [Module R A] [Coalgebra R A] {g h a : A} (ha : IsSkewPrimitiveElem R g h a) : IsSkewPrimitiveElem R g h (-a)

theorem Coalgebra.IsSkewPrimitiveElem.sub {R : Type u_2} {A : Type u_3} [CommSemiring R] [AddCommGroup A] [Module R A] [Coalgebra R A] {g h a b : A} (ha : IsSkewPrimitiveElem R g h a) (hb : IsSkewPrimitiveElem R g h b) : IsSkewPrimitiveElem R g h (a - b)

@[simp]

theorem Coalgebra.isSkewPrimitiveElem_neg {R : Type u_2} {A : Type u_3} [CommSemiring R] [AddCommGroup A] [Module R A] [Coalgebra R A] {g h a : A} : IsSkewPrimitiveElem R g h (-a) ↔ IsSkewPrimitiveElem R g h a