class EnvelopingHopfAlgebra (k : Type u) [CommRing k] (L : Type v) [LieRing L] [LieAlgebra k L] (H : Type w) [Ring H] [HopfAlgebra k H] : Type (max v w)

A Hopf algebra H is the universal enveloping algebra of a Lie algebra L if it admits a Lie homomorphism ι : L → H whose image consists of primitive elements.

• ι : L →ₗ⁅k⁆ H
• comul_ι (x : L) : CoalgebraStruct.comul (ι x) = ι x ⊗ₜ[k] 1 + 1 ⊗ₜ[k] ι x

class SweedlerHopfAlgebra (k : Type u) [Field k] (A : Type v) [Ring A] [HopfAlgebra k A] : Type v

The Sweedler Hopf algebra: a four-dimensional pointed non-commutative non-cocommutative Hopf algebra over a field of characteristic ≠ 2, generated by a grouplike g and a (g, 1) skew-primitive x.

• g : A
• x : A
• g_sq : g k * g k = 1
• x_sq : x k * x k = 0
• gx_comm : g k * x k = -(x k * g k)
• char_ne_two : 2 ≠ 0
• comul_g : CoalgebraStruct.comul (g k) = g k ⊗ₜ[k] g k
• comul_x : CoalgebraStruct.comul (x k) = x k ⊗ₜ[k] g k + 1 ⊗ₜ[k] x k
• counit_g : CoalgebraStruct.counit (g k) = 1
• counit_x : CoalgebraStruct.counit (x k) = 0
• antipode_g : (HopfAlgebraStruct.antipode k) (g k) = g k
• antipode_x : (HopfAlgebraStruct.antipode k) (x k) = -(x k * g k)
• finrank_eq : Module.finrank k A = 4

def SweedlerHopfAlgebra.isPointed_statement {k : Type u} [Field k] {A : Type v} [Ring A] [HopfAlgebra k A] : Prop

The proposition that the Sweedler Hopf algebra is pointed as a coalgebra.

class TaftAlgebra (k : Type u) [Field k] (A : Type v) [Ring A] [HopfAlgebra k A] : Type (max u v)

The Taft algebra T_n(q): an n^2-dimensional pointed Hopf algebra generated by a grouplike g of order n and a (g, 1) skew-primitive x with x^n = 0, where q is a primitive nth root of unity. Specializes to the Sweedler algebra at n = 2.

• n : ℕ
• hn : n k A ≥ 2
• q : k
• hq : IsPrimitiveRoot (q A) (n k A)
• g : A
• x : A
• g_pow_n : g k ^ n k A = 1
• x_pow_n : x k ^ n k A = 0
• gx_comm : g k * x k = (algebraMap k A) (q A) * (x k * g k)
• comul_g : CoalgebraStruct.comul (g k) = g k ⊗ₜ[k] g k
• comul_x : CoalgebraStruct.comul (x k) = x k ⊗ₜ[k] g k + 1 ⊗ₜ[k] x k
• counit_g : CoalgebraStruct.counit (g k) = 1
• counit_x : CoalgebraStruct.counit (x k) = 0
• antipode_g : (HopfAlgebraStruct.antipode k) (g k) = g k ^ (n k A - 1)
• antipode_x : (HopfAlgebraStruct.antipode k) (x k) = -(g k ^ (n k A - 1) * x k)
• finrank_eq : Module.finrank k A = n k A ^ 2

def TaftAlgebra.isPointed_statement {k : Type u} [Field k] {A : Type v} [Ring A] [HopfAlgebra k A] : Prop

The proposition that the Taft algebra is pointed as a coalgebra.

theorem andruskiewitschSchneider_conjecture (k : Type u) [Field k] [CharZero k] (H : Type v) [Ring H] [HopfAlgebra k H] [FiniteDimensional k H] (hPointed : IsPointedCoalgebra) : Algebra.adjoin k ↑(coradicalFiltration 1) = ⊤

Conjecture 1.32.1 (Andruskiewitsch-Schneider): any finite-dimensional pointed Hopf algebra over a field of characteristic zero is generated by grouplike and skew-primitive elements, equivalently by the first level of the coradical filtration.