theorem SweedlerH4.eq_sum_basis {k : Type u_1} [Field k] (a : SweedlerH4 k) : a = ∑ i : Fin 4, a.coeff i • e i

Every element of SweedlerH4 k is the sum of its coefficients times the standard basis vectors e i.

theorem SweedlerH4.linearMap_ext_basis {k : Type u_1} [Field k] {M : Type u_2} [AddCommMonoid M] [Module k M] {f g : SweedlerH4 k →ₗ[k] M} (h : ∀ (i : Fin 4), f (e i) = g (e i)) : f = g

Two k-linear maps out of SweedlerH4 k agree as soon as they agree on each of the four basis vectors e i.

noncomputable def SweedlerH4.lmOfBasis {k : Type u_1} [Field k] {M : Type u_2} [AddCommMonoid M] [Module k M] (v : Fin 4 → M) : SweedlerH4 k →ₗ[k] M

Build a k-linear map SweedlerH4 k →ₗ[k] M by prescribing its values on the four basis vectors e 0, e 1, e 2, e 3.

@[simp]

theorem SweedlerH4.lmOfBasis_e {k : Type u_1} [Field k] {M : Type u_2} [AddCommMonoid M] [Module k M] (v : Fin 4 → M) (i : Fin 4) : (lmOfBasis v) (e i) = v i

A linear map built via lmOfBasis evaluates to its prescribed value on each basis vector.

noncomputable def SweedlerH4.counitLM {k : Type u_1} [Field k] : SweedlerH4 k →ₗ[k] k

The counit of H₄ as a k-linear map: 1 ↦ 1, g ↦ 1, x ↦ 0, gx ↦ 0.

@[simp]

theorem SweedlerH4.counitLM_e {k : Type u_1} [Field k] (i : Fin 4) : counitLM (e i) = ![1, 1, 0, 0] i

The counit evaluates on basis vectors according to the tuple ![1, 1, 0, 0].

@[simp]

theorem SweedlerH4.counitLM_e0 {k : Type u_1} [Field k] : counitLM (e 0) = 1

Counit value on e 0: ε(1) = 1.

@[simp]

theorem SweedlerH4.counitLM_e1 {k : Type u_1} [Field k] : counitLM (e 1) = 1

Counit value on e 1 = g: ε(g) = 1.

@[simp]

theorem SweedlerH4.counitLM_e2 {k : Type u_1} [Field k] : counitLM (e 2) = 0

Counit value on e 2 = x: ε(x) = 0.

@[simp]

theorem SweedlerH4.counitLM_e3 {k : Type u_1} [Field k] : counitLM (e 3) = 0

Counit value on e 3 = gx: ε(gx) = 0.

@[simp]

theorem SweedlerH4.counitLM_one {k : Type u_1} [Field k] : counitLM 1 = 1

Counit preserves the unit: ε(1) = 1.

noncomputable def SweedlerH4.comulLM {k : Type u_1} [Field k] : SweedlerH4 k →ₗ[k] TensorProduct k (SweedlerH4 k) (SweedlerH4 k)

The comultiplication of H₄ as a k-linear map: 1 ↦ 1 ⊗ 1, g ↦ g ⊗ g, x ↦ x ⊗ g + 1 ⊗ x, gx ↦ gx ⊗ 1 + g ⊗ gx.

@[simp]

theorem SweedlerH4.comulLM_e0 {k : Type u_1} [Field k] : comulLM (e 0) = e 0 ⊗ₜ[k] e 0

Comultiplication value on e 0 = 1: Δ(1) = 1 ⊗ 1.

@[simp]

theorem SweedlerH4.comulLM_e1 {k : Type u_1} [Field k] : comulLM (e 1) = e 1 ⊗ₜ[k] e 1

Comultiplication value on e 1 = g: Δ(g) = g ⊗ g, exhibiting g as grouplike.

@[simp]

theorem SweedlerH4.comulLM_e2 {k : Type u_1} [Field k] : comulLM (e 2) = e 2 ⊗ₜ[k] e 1 + e 0 ⊗ₜ[k] e 2

Comultiplication value on e 2 = x: Δ(x) = x ⊗ g + 1 ⊗ x, exhibiting x as (g, 1)-skew-primitive.

@[simp]

theorem SweedlerH4.comulLM_e3 {k : Type u_1} [Field k] : comulLM (e 3) = e 3 ⊗ₜ[k] e 0 + e 1 ⊗ₜ[k] e 3

Comultiplication value on e 3 = gx: Δ(gx) = gx ⊗ 1 + g ⊗ gx.

@[simp]

theorem SweedlerH4.comulLM_one {k : Type u_1} [Field k] : comulLM 1 = e 0 ⊗ₜ[k] e 0

Comultiplication preserves the unit: Δ(1) = 1 ⊗ 1.

noncomputable def SweedlerH4.antipodeLM {k : Type u_1} [Field k] : SweedlerH4 k →ₗ[k] SweedlerH4 k

The antipode of H₄ as a k-linear map: 1 ↦ 1, g ↦ g, x ↦ gx, gx ↦ -x.

@[simp]

theorem SweedlerH4.antipodeLM_e0 {k : Type u_1} [Field k] : antipodeLM (e 0) = e 0

Antipode value on e 0 = 1: S(1) = 1.

@[simp]

theorem SweedlerH4.antipodeLM_one {k : Type u_1} [Field k] : antipodeLM 1 = 1

Antipode preserves the unit: S(1) = 1.

@[simp]

theorem SweedlerH4.antipodeLM_e1 {k : Type u_1} [Field k] : antipodeLM (e 1) = e 1

Antipode value on e 1 = g: S(g) = g = g⁻¹.

@[simp]

theorem SweedlerH4.antipodeLM_e2 {k : Type u_1} [Field k] : antipodeLM (e 2) = e 3

Antipode value on e 2 = x: S(x) = gx.

@[simp]

theorem SweedlerH4.antipodeLM_e3 {k : Type u_1} [Field k] : antipodeLM (e 3) = -e 2

Antipode value on e 3 = gx: S(gx) = -x.

@[simp]

theorem SweedlerH4.e0_mul {k : Type u_1} [Field k] (a : SweedlerH4 k) : e 0 * a = a

Left multiplication by e 0 = 1 is the identity.

@[simp]

theorem SweedlerH4.mul_e0 {k : Type u_1} [Field k] (a : SweedlerH4 k) : a * e 0 = a

Right multiplication by e 0 = 1 is the identity.

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

Basis multiplication: g · g = 1.

theorem SweedlerH4.e1_mul_e2 {k : Type u_1} [Field k] : e 1 * e 2 = e 3

Basis multiplication: g · x = gx.

theorem SweedlerH4.e1_mul_e3 {k : Type u_1} [Field k] : e 1 * e 3 = e 2

Basis multiplication: g · gx = x (using g² = 1).

theorem SweedlerH4.e2_mul_e1 {k : Type u_1} [Field k] : e 2 * e 1 = -e 3

Basis multiplication: x · g = -gx, expressing the anti-commutation gx = -xg.

theorem SweedlerH4.e3_mul_e1 {k : Type u_1} [Field k] : e 3 * e 1 = -e 2

Basis multiplication: gx · g = -x.

theorem SweedlerH4.e2_mul_e2 {k : Type u_1} [Field k] : e 2 * e 2 = 0

Basis multiplication: x · x = 0 (nilpotency of x).

theorem SweedlerH4.e2_mul_e3 {k : Type u_1} [Field k] : e 2 * e 3 = 0

Basis multiplication: x · gx = 0.

theorem SweedlerH4.e3_mul_e2 {k : Type u_1} [Field k] : e 3 * e 2 = 0

Basis multiplication: gx · x = 0.

theorem SweedlerH4.e3_mul_e3 {k : Type u_1} [Field k] : e 3 * e 3 = 0

Basis multiplication: (gx)² = 0.

theorem SweedlerH4.counitLM_mul_basis {k : Type u_1} [Field k] (i j : Fin 4) : counitLM (e i * e j) = counitLM (e i) * counitLM (e j)

The counit is multiplicative on pairs of basis vectors, verified case-by-case.

theorem SweedlerH4.counitLM_mul {k : Type u_1} [Field k] (a b : SweedlerH4 k) : counitLM (a * b) = counitLM a * counitLM b

The counit is multiplicative on arbitrary elements, by bilinear extension of counitLM_mul_basis.

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

The unit in SweedlerH4 k ⊗[k] SweedlerH4 k is e 0 ⊗ e 0.

theorem SweedlerH4.comulLM_mul_e0j {k : Type u_1} [Field k] (j : Fin 4) : comulLM (e 0 * e j) = comulLM (e 0) * comulLM (e j)

Multiplicativity of Δ on the (e 0, e j) cases.

theorem SweedlerH4.comulLM_mul_ei0 {k : Type u_1} [Field k] (i : Fin 4) : comulLM (e i * e 0) = comulLM (e i) * comulLM (e 0)

Multiplicativity of Δ on the (e i, e 0) cases.

theorem SweedlerH4.comulLM_mul_e11 {k : Type u_1} [Field k] : comulLM (e 1 * e 1) = comulLM (e 1) * comulLM (e 1)

Multiplicativity of Δ on g · g.

theorem SweedlerH4.comulLM_mul_e12 {k : Type u_1} [Field k] : comulLM (e 1 * e 2) = comulLM (e 1) * comulLM (e 2)

Multiplicativity of Δ on g · x.

theorem SweedlerH4.comulLM_mul_e13 {k : Type u_1} [Field k] : comulLM (e 1 * e 3) = comulLM (e 1) * comulLM (e 3)

Multiplicativity of Δ on g · gx.

theorem SweedlerH4.comulLM_mul_e21 {k : Type u_1} [Field k] : comulLM (e 2 * e 1) = comulLM (e 2) * comulLM (e 1)

Multiplicativity of Δ on x · g.

theorem SweedlerH4.comulLM_mul_e22 {k : Type u_1} [Field k] : comulLM (e 2 * e 2) = comulLM (e 2) * comulLM (e 2)

Multiplicativity of Δ on x · x.

theorem SweedlerH4.comulLM_mul_e23 {k : Type u_1} [Field k] : comulLM (e 2 * e 3) = comulLM (e 2) * comulLM (e 3)

Multiplicativity of Δ on x · gx.

theorem SweedlerH4.comulLM_mul_e31 {k : Type u_1} [Field k] : comulLM (e 3 * e 1) = comulLM (e 3) * comulLM (e 1)

Multiplicativity of Δ on gx · g.

theorem SweedlerH4.comulLM_mul_e32 {k : Type u_1} [Field k] : comulLM (e 3 * e 2) = comulLM (e 3) * comulLM (e 2)

Multiplicativity of Δ on gx · x.

theorem SweedlerH4.comulLM_mul_e33 {k : Type u_1} [Field k] : comulLM (e 3 * e 3) = comulLM (e 3) * comulLM (e 3)

Multiplicativity of Δ on gx · gx.

theorem SweedlerH4.comulLM_mul_basis {k : Type u_1} [Field k] (i j : Fin 4) : comulLM (e i * e j) = comulLM (e i) * comulLM (e j)

The comultiplication is multiplicative on pairs of basis vectors, verified case-by-case.

theorem SweedlerH4.comulLM_mul {k : Type u_1} [Field k] (a b : SweedlerH4 k) : comulLM (a * b) = comulLM a * comulLM b

The comultiplication is multiplicative on arbitrary elements, by bilinear extension of comulLM_mul_basis.

@[implicit_reducible]

noncomputable instance SweedlerH4.instCoalgebraStruct {k : Type u_1} [Field k] : CoalgebraStruct k (SweedlerH4 k)

The k-coalgebra structure on SweedlerH4 k, packaged from comulLM and counitLM.

@[simp]

theorem SweedlerH4.comul_is {k : Type u_1} [Field k] : CoalgebraStruct.comul = comulLM

The coalgebra-structure comultiplication unfolds to comulLM.

@[simp]

theorem SweedlerH4.counit_is {k : Type u_1} [Field k] : CoalgebraStruct.counit = counitLM

The coalgebra-structure counit unfolds to counitLM.

@[implicit_reducible]

noncomputable instance SweedlerH4.instCoalgebra {k : Type u_1} [Field k] : Coalgebra k (SweedlerH4 k)

The full k-coalgebra structure on SweedlerH4 k, verifying coassociativity and the counit axioms on the basis.

@[implicit_reducible]

noncomputable instance SweedlerH4.instBialgebra {k : Type u_1} [Field k] : Bialgebra k (SweedlerH4 k)

SweedlerH4 k is a k-bialgebra: counit and comultiplication are both algebra homomorphisms.

@[implicit_reducible]

noncomputable instance SweedlerH4.instHopfAlgebraStruct {k : Type u_1} [Field k] : HopfAlgebraStruct k (SweedlerH4 k)

The Hopf-algebra-structure layer on SweedlerH4 k, with antipode given by antipodeLM.

@[simp]

theorem SweedlerH4.antipode_is {k : Type u_1} [Field k] : HopfAlgebraStruct.antipode k = antipodeLM

The Hopf-structure antipode unfolds to antipodeLM.

@[implicit_reducible]

noncomputable instance SweedlerH4.instHopfAlgebra {k : Type u_1} [Field k] : HopfAlgebra k (SweedlerH4 k)

The full k-Hopf algebra structure on SweedlerH4 k, verifying both antipode axioms on the basis.

theorem SweedlerH4.comul_gen_g {k : Type u_1} [Field k] : CoalgebraStruct.comul gen_g = gen_g ⊗ₜ[k] gen_g

The generator g is grouplike: Δ(g) = g ⊗ g.

theorem SweedlerH4.comul_gen_x {k : Type u_1} [Field k] : CoalgebraStruct.comul gen_x = gen_x ⊗ₜ[k] gen_g + 1 ⊗ₜ[k] gen_x

The generator x is (g, 1)-skew-primitive: Δ(x) = x ⊗ g + 1 ⊗ x.

theorem SweedlerH4.counit_gen_g {k : Type u_1} [Field k] : CoalgebraStruct.counit gen_g = 1

Counit value ε(g) = 1.

theorem SweedlerH4.counit_gen_x {k : Type u_1} [Field k] : CoalgebraStruct.counit gen_x = 0

Counit value ε(x) = 0.

theorem SweedlerH4.antipode_gen_g {k : Type u_1} [Field k] : (HopfAlgebraStruct.antipode k) gen_g = gen_g

Antipode value S(g) = g.

theorem SweedlerH4.antipode_gen_x {k : Type u_1} [Field k] : (HopfAlgebraStruct.antipode k) gen_x = gen_g * gen_x

Antipode value S(x) = g · x = gx.

@[implicit_reducible]

noncomputable instance SweedlerH4.sweedlerHopfAlgebra {k : Type u_1} [Field k] [CharZero k] : SweedlerHopfAlgebra k (SweedlerH4 k)

SweedlerH4 k is an instance of the abstract SweedlerHopfAlgebra axiomatisation, witnessing that the concrete model satisfies the textbook Sweedler defining relations.