def Definition_1_22_2_antipode (k : Type u_1) [CommSemiring k] (H : Type u_2) [Semiring H] [HopfAlgebra k H] : H →ₗ[k] H

Definition 1.22.2: the antipode of a Hopf algebra, as the k-linear map S : H → H satisfying the equalities of Proposition 1.22.1.

theorem Proposition_1_22_1 {R : Type u} {A : Type v} [CommSemiring R] [Semiring A] [HopfAlgebra R A] : LinearMap.mul' R A ∘ₗ LinearMap.lTensor A (HopfAlgebraStruct.antipode R) ∘ₗ CoalgebraStruct.comul = Algebra.linearMap R A ∘ₗ CoalgebraStruct.counit ∧ LinearMap.mul' R A ∘ₗ LinearMap.rTensor A (HopfAlgebraStruct.antipode R) ∘ₗ CoalgebraStruct.comul = Algebra.linearMap R A ∘ₗ CoalgebraStruct.counit

Proposition 1.22.1: the defining identities of an antipode S on a bialgebra, namely that μ ∘ (S ⊗ id) ∘ Δ and μ ∘ (id ⊗ S) ∘ Δ both equal η ∘ ε.

theorem HopfAlgebra.antipode_conv_id {R : Type u} {A : Type v} [CommSemiring R] [Semiring A] [HopfAlgebra R A] : WithConv.toConv (antipode R) * WithConv.toConv LinearMap.id = 1

The antipode acts as a right inverse to the identity in the convolution algebra: S * id = 1 in WithConv (A →ₗ[R] A).

theorem HopfAlgebra.id_conv_antipode {R : Type u} {A : Type v} [CommSemiring R] [Semiring A] [HopfAlgebra R A] : WithConv.toConv LinearMap.id * WithConv.toConv (antipode R) = 1

The antipode acts as a left inverse to the identity in the convolution algebra: id * S = 1 in WithConv (A →ₗ[R] A).

theorem HopfAlgebra.antipode_unique {R : Type u} {A : Type v} [CommSemiring R] [Semiring A] [Bialgebra R A] (S₁ S₂ : A →ₗ[R] A) (hS₁_left : LinearMap.mul' R A ∘ₗ LinearMap.rTensor A S₁ ∘ₗ CoalgebraStruct.comul = Algebra.linearMap R A ∘ₗ CoalgebraStruct.counit) (hS₂_right : LinearMap.mul' R A ∘ₗ LinearMap.lTensor A S₂ ∘ₗ CoalgebraStruct.comul = Algebra.linearMap R A ∘ₗ CoalgebraStruct.counit) : S₁ = S₂

Uniqueness of the antipode: any two linear maps satisfying the antipode axioms on a bialgebra must coincide.

theorem Proposition_1_22_4 {R : Type u} {A : Type v} [CommSemiring R] [Semiring A] [Bialgebra R A] (S₁ S₂ : A →ₗ[R] A) (hS₁_left : LinearMap.mul' R A ∘ₗ LinearMap.rTensor A S₁ ∘ₗ CoalgebraStruct.comul = Algebra.linearMap R A ∘ₗ CoalgebraStruct.counit) (hS₂_right : LinearMap.mul' R A ∘ₗ LinearMap.lTensor A S₂ ∘ₗ CoalgebraStruct.comul = Algebra.linearMap R A ∘ₗ CoalgebraStruct.counit) : S₁ = S₂

Proposition 1.22.4: an antipode on a bialgebra H is unique if it exists.

def HopfAlgebra.antimulComm {R : Type u} {A : Type v} [CommSemiring R] [CommSemiring A] [HopfAlgebra R A] : TensorProduct R A A →ₗ[R] A

The candidate "antimultiplication" map A ⊗ A → A in the commutative case, defined as μ ∘ (S ⊗ S). Used to show S is an algebra antihomomorphism.

@[simp]

theorem HopfAlgebra.antimulComm_tmul {R : Type u} {A : Type v} [CommSemiring R] [CommSemiring A] [HopfAlgebra R A] (a b : A) : antimulComm (a ⊗ₜ[R] b) = (antipode R) a * (antipode R) b

Evaluation of antimulComm on a pure tensor: (a ⊗ b) ↦ S(a) * S(b).

theorem lmul'_comp_map_id {R : Type u} {A : Type v} [CommSemiring R] [CommSemiring A] [HopfAlgebra R A] : (Algebra.TensorProduct.lmul' R).toLinearMap ∘ₗ TensorProduct.map LinearMap.id LinearMap.id = LinearMap.mul' R A

Composing lmul' with id ⊗ id recovers the ordinary multiplication map μ.

theorem lmul'_comp_unit_tensor_unit {R : Type u} {A : Type v} [CommSemiring R] [CommSemiring A] [HopfAlgebra R A] : (Algebra.TensorProduct.lmul' R).toLinearMap ∘ₗ TensorProduct.map (Algebra.linearMap R A ∘ₗ CoalgebraStruct.counit) (Algebra.linearMap R A ∘ₗ CoalgebraStruct.counit) = Algebra.linearMap R A ∘ₗ CoalgebraStruct.counit

Composing lmul' with (η ∘ ε) ⊗ (η ∘ ε) recovers the unit-times-counit map on A ⊗ A, i.e. η ∘ (ε ⊗ ε).

theorem HopfAlgebra.antimulComm_conv_mul {R : Type u} {A : Type v} [CommSemiring R] [CommSemiring A] [HopfAlgebra R A] : WithConv.toConv antimulComm * WithConv.toConv (LinearMap.mul' R A) = 1

In the commutative case, antimulComm is a right convolution inverse of μ as maps A ⊗ A → A.

theorem HopfAlgebra.mul_conv_antimulComm {R : Type u} {A : Type v} [CommSemiring R] [CommSemiring A] [HopfAlgebra R A] : WithConv.toConv (LinearMap.mul' R A) * WithConv.toConv antimulComm = 1

In the commutative case, antimulComm is a left convolution inverse of μ as maps A ⊗ A → A.

theorem HopfAlgebra.Smul_conv_mul {R : Type u} {A : Type v} [CommSemiring R] [CommSemiring A] [HopfAlgebra R A] : WithConv.toConv (antipode R ∘ₗ LinearMap.mul' R A) * WithConv.toConv (LinearMap.mul' R A) = 1

The composite S ∘ μ is a right convolution inverse of μ in the commutative case.

theorem HopfAlgebra.antipode_mul_comm {R : Type u} {A : Type v} [CommSemiring R] [CommSemiring A] [HopfAlgebra R A] (a b : A) : (antipode R) (a * b) = (antipode R) a * (antipode R) b

Multiplicativity of the antipode in the commutative case: S(ab) = S(a) S(b). (In the commutative setting this matches the antihomomorphism law since S(a) S(b) = S(b) S(a).)

def HopfAlgebra.antipodeAlgHom {R : Type u} {A : Type v} [CommSemiring R] [CommSemiring A] [HopfAlgebra R A] : A →ₐ[R] A

On a commutative Hopf algebra, the antipode promoted to an algebra homomorphism A →ₐ[R] A.

theorem HopfAlgebra.antipode_sq_eq_id_comm {R : Type u} {A : Type v} [CommSemiring R] [CommSemiring A] [HopfAlgebra R A] (a : A) : (antipode R) ((antipode R) a) = a

The antipode of a commutative Hopf algebra is an involution: S² = id.

def Coalgebra.Repr.mulRepr {R : Type u} {A : Type v} [CommSemiring R] [Semiring A] [HopfAlgebra R A] {a b : A} (ra : Repr R a) (rb : Repr R b) : Repr R (a * b)

Sigma-notation representative of Δ(a * b) obtained by multiplying termwise the representatives of Δ(a) and Δ(b).

theorem HopfAlgebra.sum_antimul_mul_eq {R : Type u} {A : Type v} [CommSemiring R] [Semiring A] [HopfAlgebra R A] {a b : A} (ra : Coalgebra.Repr R a) (rb : Coalgebra.Repr R b) : ∑ i ∈ ra.index, ∑ j ∈ rb.index, (antipode R) (rb.left j) * (antipode R) (ra.left i) * (ra.right i * rb.right j) = (algebraMap R A) (CoalgebraStruct.counit a * CoalgebraStruct.counit b)

"Antimultiplication-then-multiplication" sum identity: pairing antipoded left factors (in reversed order) with right factors collapses to η(ε(a) · ε(b)).

theorem HopfAlgebra.sum_mul_antimul_eq {R : Type u} {A : Type v} [CommSemiring R] [Semiring A] [HopfAlgebra R A] {a b : A} (ra : Coalgebra.Repr R a) (rb : Coalgebra.Repr R b) : ∑ i ∈ ra.index, ∑ j ∈ rb.index, ra.left i * rb.left j * ((antipode R) (rb.right j) * (antipode R) (ra.right i)) = (algebraMap R A) (CoalgebraStruct.counit a * CoalgebraStruct.counit b)

"Multiplication-then-antimultiplication" sum identity: pairing left factors with antipoded right factors (in reversed order) collapses to η(ε(a) · ε(b)).

theorem HopfAlgebra.Smul_conv_mul_general {R : Type u} {A : Type v} [CommSemiring R] [Semiring A] [HopfAlgebra R A] : WithConv.toConv (antipode R ∘ₗ LinearMap.mul' R A) * WithConv.toConv (LinearMap.mul' R A) = 1

The composite S ∘ μ is a right convolution inverse of μ for a general (not necessarily commutative) Hopf algebra.

def HopfAlgebra.antimul {R : Type u} {A : Type v} [CommSemiring R] [Semiring A] [HopfAlgebra R A] : TensorProduct R A A →ₗ[R] A

The "antimultiplication" map A ⊗ A → A in the general (possibly noncommutative) case, defined as μ ∘ τ ∘ (S ⊗ S) where τ is the tensor swap. Sends a ⊗ b to S(b) S(a).

@[simp]

theorem HopfAlgebra.antimul_tmul {R : Type u} {A : Type v} [CommSemiring R] [Semiring A] [HopfAlgebra R A] (a b : A) : antimul (a ⊗ₜ[R] b) = (antipode R) b * (antipode R) a

Evaluation of antimul on a pure tensor: (a ⊗ b) ↦ S(b) * S(a).

theorem HopfAlgebra.mul_conv_antimul {R : Type u} {A : Type v} [CommSemiring R] [Semiring A] [HopfAlgebra R A] : WithConv.toConv (LinearMap.mul' R A) * WithConv.toConv antimul = 1

The general antimultiplication map antimul is a left convolution inverse of μ.

theorem HopfAlgebra.antipode_mul_anti {R : Type u} {A : Type v} [CommSemiring R] [Semiring A] [HopfAlgebra R A] (a b : A) : (antipode R) (a * b) = (antipode R) b * (antipode R) a

The antipode of a Hopf algebra is an algebra antihomomorphism: S(a b) = S(b) S(a). This is part of Proposition 1.22.5.

theorem HopfAlgebra.comul_antipode_eq (R : Type u) [CommSemiring R] (A : Type v) [Semiring A] [HopfAlgebra R A] : CoalgebraStruct.comul ∘ₗ antipode R = ↑(TensorProduct.comm R A A) ∘ₗ TensorProduct.map (antipode R) (antipode R) ∘ₗ CoalgebraStruct.comul

The antipode of a Hopf algebra is a coalgebra antihomomorphism: Δ ∘ S = τ ∘ (S ⊗ S) ∘ Δ. This is part of Proposition 1.22.5.

theorem Proposition_1_22_5 (R : Type u) [CommSemiring R] (A : Type v) [Semiring A] [HopfAlgebra R A] : (∀ (a b : A), (HopfAlgebraStruct.antipode R) (a * b) = (HopfAlgebraStruct.antipode R) b * (HopfAlgebraStruct.antipode R) a) ∧ (HopfAlgebraStruct.antipode R) 1 = 1 ∧ CoalgebraStruct.comul ∘ₗ HopfAlgebraStruct.antipode R = ↑(TensorProduct.comm R A A) ∘ₗ TensorProduct.map (HopfAlgebraStruct.antipode R) (HopfAlgebraStruct.antipode R) ∘ₗ CoalgebraStruct.comul ∧ CoalgebraStruct.counit ∘ₗ HopfAlgebraStruct.antipode R = CoalgebraStruct.counit

Proposition 1.22.5: the antipode S on a bialgebra H is an antihomomorphism of algebras with unit and of coalgebras with counit. Packaged as a fourfold conjunction covering antimultiplicativity, unit preservation, anti-comultiplicativity, and counit preservation.

noncomputable def HopfAlgebra.rightDualSMulMap {k : Type u} [CommSemiring k] {H : Type v} [Semiring H] {V : Type v} [AddCommGroup V] [Module k V] [Module H V] [SMulCommClass k H V] (h : H) : V →ₗ[k] V

The k-linear map on V given by scalar multiplication by an element h : H (used to build the right-dual H-action on V^*).

noncomputable def HopfAlgebra.rightDualAction {k : Type u} [CommSemiring k] {H : Type v} [Semiring H] [HopfAlgebra k H] {V : Type v} [AddCommGroup V] [Module k V] [Module H V] [SMulCommClass k H V] (a : H) (f : Module.Dual k V) : Module.Dual k V

The right-dual H-action on the linear dual V^* coming from a Hopf algebra H: (a · f)(v) = f(S(a) · v).

class HopfAlgebraEGNO (R : Type u) (A : Type v) [CommSemiring R] [Semiring A] extends HopfAlgebra R A : Type (max u v)

Definition 1.22.9 (EGNO): a Hopf algebra in the sense of EGNO is a bialgebra equipped with an invertible (bijective) antipode S.

• smul : R → A → A
• algebraMap : R →+* A
• commutes' (r : R) (x : A) : Algebra.algebraMap r * x = x * Algebra.algebraMap r
• smul_def' (r : R) (x : A) : r • x = Algebra.algebraMap r * x
• comul : A →ₗ[R] TensorProduct R A A
• counit : A →ₗ[R] R
• coassoc : ↑(_root_.TensorProduct.assoc R A A A) ∘ₗ LinearMap.rTensor A comul ∘ₗ comul = LinearMap.lTensor A comul ∘ₗ comul
• rTensor_counit_comp_comul : LinearMap.rTensor A counit ∘ₗ comul = (TensorProduct.mk R R A) 1
• lTensor_counit_comp_comul : LinearMap.lTensor A counit ∘ₗ comul = (TensorProduct.mk R A R).flip 1
• counit_one : CoalgebraStruct.counit 1 = 1
• mul_compr₂_counit : (LinearMap.mul R A).compr₂ CoalgebraStruct.counit = (LinearMap.mul R R).compl₁₂ CoalgebraStruct.counit CoalgebraStruct.counit
• comul_one : CoalgebraStruct.comul 1 = 1
• mul_compr₂_comul : (LinearMap.mul R A).compr₂ CoalgebraStruct.comul = (LinearMap.mul R (TensorProduct R A A)).compl₁₂ CoalgebraStruct.comul CoalgebraStruct.comul
• antipode : A →ₗ[R] A
• mul_antipode_rTensor_comul : LinearMap.mul' R A ∘ₗ LinearMap.rTensor A (antipode R) ∘ₗ CoalgebraStruct.comul = Algebra.linearMap R A ∘ₗ CoalgebraStruct.counit
• mul_antipode_lTensor_comul : LinearMap.mul' R A ∘ₗ LinearMap.lTensor A (antipode R) ∘ₗ CoalgebraStruct.comul = Algebra.linearMap R A ∘ₗ CoalgebraStruct.counit
• antipode_bijective : Function.Bijective ⇑(HopfAlgebraStruct.antipode R)

@[reducible]

noncomputable def HopfAlgebraEGNO.ofCommutative (R : Type u) (A : Type v) [CommSemiring R] [CommSemiring A] [HopfAlgebra R A] : HopfAlgebraEGNO R A

Any commutative Hopf algebra is automatically an EGNO Hopf algebra, because its antipode is an involution and hence bijective.

@[reducible, inline]

abbrev Definition_1_22_9 (k : Type u_1) [CommRing k] (H : Type u_2) [Ring H] [Algebra k H] : Type (max u_1 u_2)

Definition 1.22.9 (alias): a Hopf algebra is a bialgebra with an invertible antipode.

theorem Proposition_1_22_15_algebra_anti (R : Type u) [CommSemiring R] (A : Type v) [Semiring A] [HopfAlgebra R A] (a b : A) : (HopfAlgebraStruct.antipode R) (a * b) = (HopfAlgebraStruct.antipode R) b * (HopfAlgebraStruct.antipode R) a

Algebra-antihomomorphism part of Proposition 1.22.15 / 1.22.5: S(ab) = S(b) S(a).

theorem Proposition_1_22_15_coalgebra_anti (R : Type u) [CommSemiring R] (A : Type v) [Semiring A] [HopfAlgebra R A] : CoalgebraStruct.comul ∘ₗ HopfAlgebraStruct.antipode R = ↑(TensorProduct.comm R A A) ∘ₗ TensorProduct.map (HopfAlgebraStruct.antipode R) (HopfAlgebraStruct.antipode R) ∘ₗ CoalgebraStruct.comul

Coalgebra-antihomomorphism part of Proposition 1.22.15 / 1.22.5: Δ ∘ S = τ ∘ (S ⊗ S) ∘ Δ.

theorem HopfAlgebra.antipode_range_descent (k : Type u) [Field k] (A : Type v) [Ring A] [HopfAlgebra k A] [FiniteDimensional k A] (m : ℕ) (hm_pos : 0 < m) (hstab : (antipode k).iterateRange m = (antipode k).iterateRange (m + 1)) : (antipode k).iterateRange (m - 1) = (antipode k).iterateRange m

Descent step: if the iterated ranges of S stabilize at index m, then they already agreed at index m - 1. Used to prove S is surjective on a finite-dimensional Hopf algebra.

theorem HopfAlgebra.antipode_bijective (k : Type u) [Field k] (A : Type v) [Ring A] [HopfAlgebra k A] [FiniteDimensional k A] : Function.Bijective ⇑(antipode k)

On a finite-dimensional Hopf algebra over a field, the antipode is bijective.

noncomputable def HopfAlgebra.antipodeEquiv (k : Type u) [Field k] (A : Type v) [Ring A] [HopfAlgebra k A] [FiniteDimensional k A] : A ≃ₗ[k] A

The antipode of a finite-dimensional Hopf algebra packaged as a k-linear equivalence.

theorem Proposition_1_22_15 (k : Type u) [Field k] (H : Type v) [Ring H] [HopfAlgebra k H] [FiniteDimensional k H] : Function.Bijective ⇑(HopfAlgebraStruct.antipode k)

Proposition 1.22.15: if H is a finite-dimensional bialgebra with an antipode S, then S is invertible, so H is a Hopf algebra.