noncomputable def QuasiBialgebra.idTensorComul (R : Type u) [CommSemiring R] (H : Type v) [Semiring H] [Algebra R H] (Δ : H →ₐ[R] TensorProduct R H H) : H →ₐ[R] TensorProduct R H (TensorProduct R H H)

The algebra map (Id ⊗ Δ) ∘ Δ : H → H ⊗ (H ⊗ H) used in the quasi-coassociativity axiom.

noncomputable def QuasiBialgebra.comulTensorId (R : Type u) [CommSemiring R] (H : Type v) [Semiring H] [Algebra R H] (Δ : H →ₐ[R] TensorProduct R H H) : H →ₐ[R] TensorProduct R H (TensorProduct R H H)

The algebra map ((Δ ⊗ Id) ∘ Δ) reassociated to H ⊗ (H ⊗ H), used in the quasi-coassociativity axiom.

noncomputable def QuasiBialgebra.idCounitId (R : Type u) [CommSemiring R] (H : Type v) [Semiring H] [Algebra R H] (ε : H →ₐ[R] R) : TensorProduct R H (TensorProduct R H H) →ₐ[R] TensorProduct R H H

The contraction (Id ⊗ ε ⊗ Id) : H ⊗ (H ⊗ H) → H ⊗ H used in stating (Id ⊗ ε ⊗ Id)(Φ) = 1 ⊗ 1.

noncomputable def QuasiBialgebra.idIdComul (R : Type u) [CommSemiring R] (H : Type v) [Semiring H] [Algebra R H] (Δ : H →ₐ[R] TensorProduct R H H) : TensorProduct R H (TensorProduct R H H) →ₐ[R] TensorProduct R H (TensorProduct R H (TensorProduct R H H))

(Id ⊗ Id ⊗ Δ), the map embedding into H ⊗ (H ⊗ (H ⊗ H)), used in the pentagon axiom.

noncomputable def QuasiBialgebra.comulIdId (R : Type u) [CommSemiring R] (H : Type v) [Semiring H] [Algebra R H] (Δ : H →ₐ[R] TensorProduct R H H) : TensorProduct R H (TensorProduct R H H) →ₐ[R] TensorProduct R H (TensorProduct R H (TensorProduct R H H))

(Δ ⊗ Id ⊗ Id), reassociated into H ⊗ (H ⊗ (H ⊗ H)), used in the pentagon axiom.

noncomputable def QuasiBialgebra.idComulId (R : Type u) [CommSemiring R] (H : Type v) [Semiring H] [Algebra R H] (Δ : H →ₐ[R] TensorProduct R H H) : TensorProduct R H (TensorProduct R H H) →ₐ[R] TensorProduct R H (TensorProduct R H (TensorProduct R H H))

(Id ⊗ Δ ⊗ Id), the middle inflation used in the pentagon axiom.

noncomputable def QuasiBialgebra.embedPhiRight (R : Type u) [CommSemiring R] (H : Type v) [Semiring H] [Algebra R H] : TensorProduct R H (TensorProduct R H H) →ₐ[R] TensorProduct R H (TensorProduct R H (TensorProduct R H H))

The right-tensoring embedding H ⊗ (H ⊗ H) → H ⊗ (H ⊗ (H ⊗ H)) realizing Φ ⊗ 1 in the pentagon axiom.

def QuasiBialgebra.rmulMap (R : Type u) [CommSemiring R] (H : Type v) [Semiring H] [Algebra R H] (c : H) : H →ₗ[R] H

Right multiplication by c, as an R-linear map.

noncomputable def QuasiBialgebra.sAlphaMap (R : Type u) [CommSemiring R] (H : Type v) [Semiring H] [Algebra R H] (S : H →ₗ[R] H) (α_elem : H) : TensorProduct R H H →ₗ[R] H

The linear map x ⊗ y ↦ S(x) · α · y, used to express the left antipode axiom.

noncomputable def QuasiBialgebra.betaSMap (R : Type u) [CommSemiring R] (H : Type v) [Semiring H] [Algebra R H] (S : H →ₗ[R] H) (β_elem : H) : TensorProduct R H H →ₗ[R] H

The linear map x ⊗ y ↦ x · β · S(y), used to express the right antipode axiom.

noncomputable def QuasiBialgebra.phiBetaSAlphaMap (R : Type u) [CommSemiring R] (H : Type v) [Semiring H] [Algebra R H] (S : H →ₗ[R] H) (α_elem β_elem : H) : TensorProduct R H (TensorProduct R H H) →ₗ[R] H

The map x ⊗ y ⊗ z ↦ x · β · S(y) · α · z evaluating the antipode identity ∑ Φ¹ β S(Φ²) α Φ³ = 1 from Proposition 1.35.1.

noncomputable def QuasiBialgebra.phiInvSAlphaBetaSMap (R : Type u) [CommSemiring R] (H : Type v) [Semiring H] [Algebra R H] (S : H →ₗ[R] H) (α_elem β_elem : H) : TensorProduct R H (TensorProduct R H H) →ₗ[R] H

The map x ⊗ y ⊗ z ↦ S(x) · α · y · β · S(z) evaluating the dual antipode identity ∑ S(Φ̄¹) α Φ̄² β S(Φ̄³) = 1 from Proposition 1.35.1.

class QuasiBialgebra (R : Type u) (H : Type v) [CommSemiring R] [Semiring H] [Algebra R H] : Type (max u v)

Definition 1.34.5 (Etingof–Gelaki–Nikshych–Ostrik): A quasi-bialgebra over R consists of an associative unital R-algebra H together with a coproduct comul : H → H ⊗ H, a counit counit : H → R (both unital algebra homomorphisms), and an invertible associator Φ ∈ H^{⊗3} satisfying the quasi-coassociativity, counit and pentagon axioms.

• comul : H →ₐ[R] TensorProduct R H H
• counit : H →ₐ[R] R
• Φ : (TensorProduct R H (TensorProduct R H H))ˣ
• quasi_coassoc (a : H) : (idTensorComul R H comul) a * ↑Φ = ↑Φ * (comulTensorId R H comul) a
• left_counit : (↑(Algebra.TensorProduct.lid R H)).comp ((Algebra.TensorProduct.map counit (AlgHom.id R H)).comp comul) = AlgHom.id R H
• right_counit : (↑(Algebra.TensorProduct.rid R R H)).comp ((Algebra.TensorProduct.map (AlgHom.id R H) counit).comp comul) = AlgHom.id R H
• Φ_counit : (idCounitId R H counit) ↑Φ = 1
• pentagon : 1 ⊗ₜ[R] ↑Φ * (idComulId R H comul) ↑Φ * (embedPhiRight R H) ↑Φ = (idIdComul R H comul) ↑Φ * (comulIdId R H comul) ↑Φ

noncomputable def QuasiBialgebra.associator {R : Type u} {H : Type v} [CommSemiring R] [Semiring H] [Algebra R H] [qb : QuasiBialgebra R H] : (TensorProduct R H (TensorProduct R H H))ˣ

Accessor: the associator element Φ of a quasi-bialgebra.

structure QuasiBialgebraAntipode (R : Type u) (H : Type v) [CommSemiring R] [Semiring H] [Algebra R H] [qb : QuasiBialgebra R H] : Type v

Definition 1.35.2 (Etingof–Gelaki–Nikshych–Ostrik): An antipode on a quasi-bialgebra is a triple (S, α, β) with S : H → H a unital algebra antihomomorphism and α, β ∈ H satisfying the antipode identities (1.35.1) and (1.35.2).

• S : H →ₗ[R] H
• α_elem : H
• β_elem : H
• S_anti_mul (a b : H) : self.S (a * b) = self.S b * self.S a
• S_one : self.S 1 = 1
• left_antipode (b : H) : (QuasiBialgebra.sAlphaMap R H self.S self.α_elem) (QuasiBialgebra.comul b) = QuasiBialgebra.counit b • self.α_elem
• right_antipode (b : H) : (QuasiBialgebra.betaSMap R H self.S self.β_elem) (QuasiBialgebra.comul b) = QuasiBialgebra.counit b • self.β_elem
• phi_beta_S_alpha : (QuasiBialgebra.phiBetaSAlphaMap R H self.S self.α_elem self.β_elem) ↑QuasiBialgebra.Φ = 1
• phiInv_S_alpha_beta_S : (QuasiBialgebra.phiInvSAlphaBetaSMap R H self.S self.α_elem self.β_elem) ↑QuasiBialgebra.Φ⁻¹ = 1

class QuasiHopfAlgebra (R : Type u) (H : Type v) [CommSemiring R] [Semiring H] [Algebra R H] extends QuasiBialgebra R H : Type (max u v)

Definition 1.35.2 (Etingof–Gelaki–Nikshych–Ostrik): A quasi-Hopf algebra is a quasi-bialgebra (H, Δ, ε, Φ) equipped with an antipode (S, α, β) where S is bijective.

• comul : H →ₐ[R] TensorProduct R H H
• counit : H →ₐ[R] R
• Φ : (TensorProduct R H (TensorProduct R H H))ˣ
• quasi_coassoc (a : H) : (idTensorComul R H comul) a * ↑Φ = ↑Φ * (comulTensorId R H comul) a
• left_counit : (↑(Algebra.TensorProduct.lid R H)).comp ((Algebra.TensorProduct.map counit (AlgHom.id R H)).comp comul) = AlgHom.id R H
• right_counit : (↑(Algebra.TensorProduct.rid R R H)).comp ((Algebra.TensorProduct.map (AlgHom.id R H) counit).comp comul) = AlgHom.id R H
• Φ_counit : (idCounitId R H counit) ↑Φ = 1
• pentagon : 1 ⊗ₜ[R] ↑Φ * (idComulId R H comul) ↑Φ * (embedPhiRight R H) ↑Φ = (idIdComul R H comul) ↑Φ * (comulIdId R H comul) ↑Φ
• S : H ≃ₗ[R] H
• α_elem : H
• β_elem : H
• S_anti_mul (a b : H) : S (a * b) = S b * S a
• S_one : S 1 = 1
• left_antipode (b : H) : (QuasiBialgebra.sAlphaMap R H (↑S) (α_elem R)) (QuasiBialgebra.comul b) = QuasiBialgebra.counit b • α_elem R
• right_antipode (b : H) : (QuasiBialgebra.betaSMap R H (↑S) (β_elem R)) (QuasiBialgebra.comul b) = QuasiBialgebra.counit b • β_elem R
• phi_beta_S_alpha : (QuasiBialgebra.phiBetaSAlphaMap R H (↑S) (α_elem R) (β_elem R)) ↑QuasiBialgebra.Φ = 1
• phiInv_S_alpha_beta_S : (QuasiBialgebra.phiInvSAlphaBetaSMap R H (↑S) (α_elem R) (β_elem R)) ↑QuasiBialgebra.Φ⁻¹ = 1

noncomputable def QuasiBialgebraTwist.counitTensorId (R : Type u) [CommSemiring R] (H : Type v) [Semiring H] [Algebra R H] (ε : H →ₐ[R] R) : TensorProduct R H H →ₐ[R] H

(ε ⊗ Id) : H ⊗ H → H, used in the twist counit normalization.

noncomputable def QuasiBialgebraTwist.idTensorCounit (R : Type u) [CommSemiring R] (H : Type v) [Semiring H] [Algebra R H] (ε : H →ₐ[R] R) : TensorProduct R H H →ₐ[R] H

(Id ⊗ ε) : H ⊗ H → H, used in the twist counit normalization.

noncomputable def QuasiBialgebraTwist.idTensorComul (R : Type u) [CommSemiring R] (H : Type v) [Semiring H] [Algebra R H] (Δ : H →ₐ[R] TensorProduct R H H) : TensorProduct R H H →ₐ[R] TensorProduct R H (TensorProduct R H H)

(Id ⊗ Δ) : H ⊗ H → H ⊗ (H ⊗ H), used in the formula for the twisted associator.

noncomputable def QuasiBialgebraTwist.comulTensorId (R : Type u) [CommSemiring R] (H : Type v) [Semiring H] [Algebra R H] (Δ : H →ₐ[R] TensorProduct R H H) : TensorProduct R H H →ₐ[R] TensorProduct R H (TensorProduct R H H)

(Δ ⊗ Id) : H ⊗ H → H ⊗ (H ⊗ H), reassociated, used in the formula for the twisted associator.

noncomputable def QuasiBialgebraTwist.embedRight (R : Type u) [CommSemiring R] (H : Type v) [Semiring H] [Algebra R H] : TensorProduct R H H →ₐ[R] TensorProduct R H (TensorProduct R H H)

The embedding x ↦ 1 ⊗ x : H ⊗ H → H ⊗ (H ⊗ H), realizing 1 ⊗ J in the twisted associator formula.

noncomputable def QuasiBialgebraTwist.embedLeft (R : Type u) [CommSemiring R] (H : Type v) [Semiring H] [Algebra R H] : TensorProduct R H H →ₐ[R] TensorProduct R H (TensorProduct R H H)

The embedding x ↦ x ⊗ 1 : H ⊗ H → H ⊗ (H ⊗ H), realizing J ⊗ 1 in the twisted associator formula.

structure QuasiBialgebraTwist (R : Type u) (H : Type v) [CommSemiring R] [Semiring H] [Algebra R H] [QuasiBialgebra R H] : Type v

A twist for a quasi-bialgebra H: an invertible element J ∈ H ⊗ H with (ε ⊗ Id)(J) = (Id ⊗ ε)(J) = 1 (Definition 1.34.6).

• J : (TensorProduct R H H)ˣ
• counit_left : (counitTensorId R H QuasiBialgebra.counit) ↑self.J = 1
• counit_right : (idTensorCounit R H QuasiBialgebra.counit) ↑self.J = 1

noncomputable def QuasiBialgebraTwist.twistedComul {R : Type u} {H : Type v} [CommSemiring R] [Semiring H] [Algebra R H] [QuasiBialgebra R H] (tw : QuasiBialgebraTwist R H) (x : H) : TensorProduct R H H

The twisted coproduct Δ^J(x) = J^{-1} Δ(x) J (Definition 1.34.6).

noncomputable def QuasiBialgebraTwist.twistedAssociator {R : Type u} {H : Type v} [CommSemiring R] [Semiring H] [Algebra R H] [qb : QuasiBialgebra R H] (tw : QuasiBialgebraTwist R H) : TensorProduct R H (TensorProduct R H H)

The twisted associator Φ^J = (1 ⊗ J)^{-1} (Id ⊗ Δ)(J)^{-1} Φ (Δ ⊗ Id)(J) (J ⊗ 1) (Definition 1.34.6).

def QuasiBialgebraTwistEquiv {R : Type u} {H : Type v} [CommSemiring R] [Semiring H] [Algebra R H] (qb₁ qb₂ : QuasiBialgebra R H) : Prop

Twist equivalence of quasi-bialgebras: two quasi-bialgebra structures on the same underlying algebra H are twist equivalent if one is obtained from the other by conjugation by a normalized invertible twist J (Definition 1.34.6).

@[reducible, inline]

abbrev Definition_1_34_5_QuasiBialgebra (R : Type u_1) (H : Type u_2) [CommSemiring R] [Semiring H] [Algebra R H] : Type (max u_1 u_2)

Reference abbreviation for Definition 1.34.5: a quasi-bialgebra.

@[reducible, inline]

abbrev Definition_1_34_6 (R : Type u_1) (H : Type u_2) [CommSemiring R] [Semiring H] [Algebra R H] [QuasiBialgebra R H] : Type u_2

Reference abbreviation for Definition 1.34.6: a twist for a quasi-bialgebra.

@[reducible, inline]

abbrev Definition_1_34_6_Twist (R : Type u_1) (H : Type u_2) [CommSemiring R] [Semiring H] [Algebra R H] [QuasiBialgebra R H] : Type u_2

Reference abbreviation for Definition 1.34.6: the twist data.

@[reducible, inline]

abbrev Definition_1_34_6_TwistEquiv {R : Type u_1} {H : Type u_2} [CommSemiring R] [Semiring H] [Algebra R H] (qb₁ qb₂ : QuasiBialgebra R H) : Prop

Reference abbreviation for Definition 1.34.6: twist equivalence of quasi-bialgebras.

@[reducible, inline]

abbrev Definition_1_35_2_Antipode (R : Type u_1) (H : Type u_2) [CommSemiring R] [Semiring H] [Algebra R H] [qb : QuasiBialgebra R H] : Type u_2

Reference abbreviation for Definition 1.35.2: an antipode on a quasi-bialgebra.

@[reducible, inline]

abbrev Definition_1_35_2_QuasiHopfAlgebra (R : Type u_1) (H : Type u_2) [CommSemiring R] [Semiring H] [Algebra R H] : Type (max u_1 u_2)

Reference abbreviation for Definition 1.35.2: a quasi-Hopf algebra.