structure SweedlerH4 (k : Type u_1) [Field k] : Type u_1

Concrete model of Sweedler's 4-dimensional Hopf algebra H₄ over a field k: an element is recorded as a tuple of 4 coefficients in the basis (1, g, x, gx).

• coeff : Fin 4 → k

theorem SweedlerH4.ext {k : Type u_1} {inst✝ : Field k} {x y : SweedlerH4 k} (coeff : x.coeff = y.coeff) : x = y

theorem SweedlerH4.ext_iff {k : Type u_1} {inst✝ : Field k} {x y : SweedlerH4 k} : x = y ↔ x.coeff = y.coeff

@[implicit_reducible]

noncomputable instance SweedlerH4.instZero {k : Type u_1} [Field k] : Zero (SweedlerH4 k)

Zero element of SweedlerH4 k, with all coefficients zero.

@[implicit_reducible]

noncomputable instance SweedlerH4.instAdd {k : Type u_1} [Field k] : Add (SweedlerH4 k)

Addition on SweedlerH4 k, componentwise on coefficients.

@[implicit_reducible]

noncomputable instance SweedlerH4.instNeg {k : Type u_1} [Field k] : Neg (SweedlerH4 k)

Negation on SweedlerH4 k, componentwise on coefficients.

@[implicit_reducible]

noncomputable instance SweedlerH4.instSub {k : Type u_1} [Field k] : Sub (SweedlerH4 k)

Subtraction on SweedlerH4 k, componentwise on coefficients.

@[implicit_reducible]

noncomputable instance SweedlerH4.instSMul {k : Type u_1} [Field k] : SMul k (SweedlerH4 k)

Scalar multiplication by k on SweedlerH4 k, scaling each coefficient.

@[simp]

theorem SweedlerH4.coeff_zero' {k : Type u_1} [Field k] (i : Fin 4) : coeff 0 i = 0

All coefficients of 0 : SweedlerH4 k are zero.

@[simp]

theorem SweedlerH4.coeff_add {k : Type u_1} [Field k] (a b : SweedlerH4 k) (i : Fin 4) : (a + b).coeff i = a.coeff i + b.coeff i

Componentwise formula for addition coefficients in SweedlerH4 k.

@[simp]

theorem SweedlerH4.coeff_neg {k : Type u_1} [Field k] (a : SweedlerH4 k) (i : Fin 4) : (-a).coeff i = -a.coeff i

Componentwise formula for negation coefficients in SweedlerH4 k.

@[simp]

theorem SweedlerH4.coeff_sub {k : Type u_1} [Field k] (a b : SweedlerH4 k) (i : Fin 4) : (a - b).coeff i = a.coeff i - b.coeff i

Componentwise formula for subtraction coefficients in SweedlerH4 k.

@[simp]

theorem SweedlerH4.coeff_smul {k : Type u_1} [Field k] (r : k) (a : SweedlerH4 k) (i : Fin 4) : (r • a).coeff i = r * a.coeff i

Componentwise formula for scalar multiplication coefficients in SweedlerH4 k.

noncomputable def SweedlerH4.basisMul {k : Type u_1} [Field k] (i j : Fin 4) : Fin 4 → k

Structure constants of SweedlerH4 k in the basis e₀ = 1, e₁ = g, e₂ = x, e₃ = gx: for each pair (i, j), gives the coefficient of e_m in e_i · e_j.

@[implicit_reducible]

noncomputable instance SweedlerH4.instMul {k : Type u_1} [Field k] : Mul (SweedlerH4 k)

Multiplication on SweedlerH4 k, given by bilinearly extending the basis structure constants basisMul.

@[implicit_reducible]

noncomputable instance SweedlerH4.instOne {k : Type u_1} [Field k] : One (SweedlerH4 k)

The unit element of SweedlerH4 k, the basis vector e₀.

@[implicit_reducible]

noncomputable instance SweedlerH4.instNatCast {k : Type u_1} [Field k] : NatCast (SweedlerH4 k)

The natural-number cast into SweedlerH4 k, sending n to n · e₀.

@[implicit_reducible]

noncomputable instance SweedlerH4.instIntCast {k : Type u_1} [Field k] : IntCast (SweedlerH4 k)

The integer cast into SweedlerH4 k, sending n to n · e₀.

@[simp]

theorem SweedlerH4.coeff_mul {k : Type u_1} [Field k] (a b : SweedlerH4 k) (m : Fin 4) : (a * b).coeff m = ∑ i : Fin 4, ∑ j : Fin 4, a.coeff i * b.coeff j * basisMul i j m

Componentwise formula for multiplication coefficients in SweedlerH4 k, in terms of the basis structure constants.

@[simp]

theorem SweedlerH4.coeff_one {k : Type u_1} [Field k] (m : Fin 4) : coeff 1 m = if m = 0 then 1 else 0

Componentwise formula for the unit coefficients in SweedlerH4 k.

@[simp]

theorem SweedlerH4.coeff_natCast {k : Type u_1} [Field k] (n : ℕ) (m : Fin 4) : (↑n).coeff m = if m = 0 then ↑n else 0

Componentwise formula for natural-cast coefficients in SweedlerH4 k.

@[simp]

theorem SweedlerH4.coeff_intCast {k : Type u_1} [Field k] (n : ℤ) (m : Fin 4) : (↑n).coeff m = if m = 0 then ↑n else 0

Componentwise formula for integer-cast coefficients in SweedlerH4 k.

@[simp]

theorem SweedlerH4.Fin4_sum {k : Type u_1} [Field k] (f : Fin 4 → k) : ∑ i : Fin 4, f i = f 0 + f 1 + f 2 + f 3

A finite sum over Fin 4 expands as the sum of the four values at 0, 1, 2, 3.

@[implicit_reducible]

noncomputable instance SweedlerH4.instAddCommGroup {k : Type u_1} [Field k] : AddCommGroup (SweedlerH4 k)

SweedlerH4 k is an additive abelian group under componentwise operations.

@[implicit_reducible]

noncomputable instance SweedlerH4.instRing {k : Type u_1} [Field k] : Ring (SweedlerH4 k)

SweedlerH4 k is a (noncommutative) ring with multiplication given by the basis structure constants basisMul.

@[implicit_reducible]

noncomputable instance SweedlerH4.instModule {k : Type u_1} [Field k] : Module k (SweedlerH4 k)

SweedlerH4 k is a k-module under componentwise scaling.

@[implicit_reducible]

noncomputable instance SweedlerH4.instAlgebra {k : Type u_1} [Field k] : Algebra k (SweedlerH4 k)

SweedlerH4 k is a k-algebra with scalar action factoring through multiplication by e₀.

noncomputable def SweedlerH4.toFunEquiv {k : Type u_1} [Field k] : SweedlerH4 k ≃ₗ[k] Fin 4 → k

The canonical k-linear equivalence between SweedlerH4 k and Fin 4 → k extracting the coefficient tuple.

theorem SweedlerH4.finrank_eq {k : Type u_1} [Field k] : Module.finrank k (SweedlerH4 k) = 4

SweedlerH4 k has k-dimension exactly 4, matching its basis (1, g, x, gx).

def SweedlerH4.e {k : Type u_1} [Field k] (i : Fin 4) : SweedlerH4 k

The standard basis vector e i of SweedlerH4 k, with coefficient 1 at i and 0 elsewhere.

def SweedlerH4.gen_g {k : Type u_1} [Field k] : SweedlerH4 k

The Sweedler generator g, identified with the basis vector e 1.

def SweedlerH4.gen_x {k : Type u_1} [Field k] : SweedlerH4 k

The Sweedler generator x, identified with the basis vector e 2.

@[simp]

theorem SweedlerH4.coeff_e {k : Type u_1} [Field k] (i j : Fin 4) : (e i).coeff j = if i = j then 1 else 0

Coefficient formula for the basis vector e i.

@[simp]

theorem SweedlerH4.coeff_gen_g {k : Type u_1} [Field k] (j : Fin 4) : gen_g.coeff j = if 1 = j then 1 else 0

Coefficient formula for the generator g = e 1.

@[simp]

theorem SweedlerH4.coeff_gen_x {k : Type u_1} [Field k] (j : Fin 4) : gen_x.coeff j = if 2 = j then 1 else 0

Coefficient formula for the generator x = e 2.

theorem SweedlerH4.gen_g_sq {k : Type u_1} [Field k] : gen_g * gen_g = 1

Defining relation of H₄: g² = 1.

theorem SweedlerH4.gen_x_sq {k : Type u_1} [Field k] : gen_x * gen_x = 0

Defining relation of H₄: x² = 0.

theorem SweedlerH4.gen_gx_comm {k : Type u_1} [Field k] : gen_g * gen_x = -(gen_x * gen_g)

Defining anti-commutation relation of H₄: gx = -xg.

theorem SweedlerH4.gen_g_mul_x {k : Type u_1} [Field k] : gen_g * gen_x = e 3

The product g · x is the fourth basis vector e 3, i.e. the basis element usually denoted gx.

theorem SweedlerH4.e_zero_eq_one {k : Type u_1} [Field k] : e 0 = 1

The first basis vector e 0 is the multiplicative unit 1 of SweedlerH4 k.