Alphabeta Math
TheoremStatement: Literature-sourcedProof: AI-adaptedPipeline-generatedprecheck pass
How statement and proof provenance work

The first chip identifies the source of the statement or construction; the second identifies the source of its local proof or verification.

  • Literature-sourced: the exact statement appears in a cited source; only wording and notation differ.
  • AI-adapted: a semantically identical restatement of literature-sourced material, modulo indexing, notation, and boundary cases adopted by the library.
  • AI-generated: a genuinely novel statement formulated by AI, with no source for the claim itself.

These labels describe origin, not correctness: citations and verification chips remain separate evidence.

Modules over a quasi-bialgebra form a monoidal category

Statement

Let (H,Δ,ε,Φ) be a quasi-bialgebra over a field k in the convention of Quasi-bialgebras, quasi-antipodes, and quasi-Hopf algebras. The category H-Mod of unital left H-modules, with H-linear maps, is monoidal. Its tensor product has underlying vector space V⊗kW and action h⋅(v⊗w)=∑h(1)v⊗h(2)w. Its unit object is kε=k with h⋅c=ε(h)c. The associator from (U⊗V)⊗W to U⊗(V⊗W) is the canonical vector-space rebracketing followed by the action of Φ: aU,V,W((u⊗v)⊗w)=∑Φ1u⊗(Φ2v⊗Φ3w),Φ=∑Φ1⊗Φ2⊗Φ3. The left and right unit constraints are the canonical vector-space maps. No quasi-antipode is needed for this monoidal structure.

Pentagon diagram

The arrows are the indicated rebracketing maps, each acting by the corresponding component of Φ. The proof below verifies their equality by multiplying the induced operators in H⊗4.

diagram failed to render:
& (((U\otimes V)\otimes W)\otimes X)
  \arrow[rr,"a_{U\otimes V,W,X}"]
  \arrow[dl,"a_{U,V,W}\otimes 1_X"']
&& (U\otimes V)\otimes(W\otimes X)
  \arrow[dr,"a_{U,V,W\otimes X}"]
& \\
(U\otimes(V\otimes W))\otimes X
  \arrow[dr,"a_{U,V\otimes W,X}"']
&&&& U\otimes(V\otimes(W\otimes X)) \\
& U\otimes((V\otimes W)\otimes X)
  \arrow[ur,"1_U\otimes a_{V,W,X}"']
&&&

Facts & Assumptions

Given: A field k, a quasi-bialgebra (H,Δ,ε,Φ), and unital left H-modules U,V,W,X.

[F1]

Quasi-bialgebras, quasi-antipodes, and quasi-Hopf algebras: Δ and ε are unital algebra maps; (id⊗Δ)Δ(h)=Φ(Δ⊗id)Δ(h)Φ−1; Φ satisfies the pentagon identity and (id⊗ε⊗id)(Φ)=1⊗1.

[F2]

Unital left and right modules over a ring; unqualified module means left module: a left module action satisfies 1Hv=v and (ab)v=a(bv).

[F3]

Scalars, tensor powers, the empty tensor, opposite algebras and finite sums: tensor products are algebraic over k, and every tensor is a finite sum of elementary tensors.

[F4]

Universal property of the tensor product for balanced maps into abelian groups: a balanced bilinear pairing induces a unique map from the tensor product; elementary tensors span it.

[F5]

Symmetry and associativity isomorphisms for tensor products over a commutative ring: the canonical vector-space associator sends (u⊗v)⊗w to u⊗(v⊗w).

[F6]

Monoidal category: a monoidal category has a bifunctor, a unit, natural associator and unit isomorphisms satisfying the pentagon and triangle equations.

[F7]

Module homomorphism and isomorphism, kernel, image and cokernel: an H-linear map preserves addition and the left H-action.

[F8]

Associator naturality, pentagon, unit triangle and symmetry hexagons on elementary tensors: canonical vector-space rebracketings satisfy naturality, the pentagon and the unit triangle; the canonical unit isomorphisms are natural. We use these coherent identifications when suppressing tensor parentheses.

Proof

technique · direct
1.1F1F2F3F4F7construct

For left H-modules V,W, the formula in the Statement is a unital left action: its unit acts as Δ(1H)=1H⊗1H, and on every elementary tensor the two sides of the module associativity law are respectively Δ(h)Δ(g) and Δ(hg) acting on that tensor. They agree because Δ is an algebra map. The tensor maps induced by H-linear maps are H-linear by the same formula on elementary tensors, and preserve identities and compositions.

1.2F1F3F5F8algebra

Using the canonical vector-space identifications of [F5] and [F8], the map aU,V,W is invertible because Φ is invertible; its inverse is the reverse rebracketing followed by Φ−1. It is H-linear since, on the underlying triple tensor, Φ(Δ⊗id)Δ(h)=(id⊗Δ)Δ(h)Φ, which is the quasi-coassociativity identity in [F1] multiplied on the right by Φ.

1.3F1F2F3F4F7F8construct

The associator is natural: for module maps f,g,j, both composites send an elementary tensor to the same tensor with f,g,j applied to the three components, because these maps commute with each H-action. The unit object kε is a left module since ε is a unital algebra map. The canonical left and right unit maps are natural vector-space isomorphisms by [F8], with inverses v↦1⊗v and v↦v⊗1. They are H-linear by the two counit equations: their values on c⊗v and v⊗c reduce respectively to ∑ε(h(1))c h(2)v=c hv and ∑h(1)v ε(h(2))c=c hv. Their inverses are therefore H-linear as well.

2.1F1F3F8step 1.1step 1.2algebra

Both pentagon paths go from ((U⊗V)⊗W)⊗X to U⊗(V⊗(W⊗X)). Under the coherent vector-space identifications of [F8], the short composite acts by (id⊗id⊗Δ)(Φ)(Δ⊗id⊗id)(Φ). The long composite acts by (1⊗Φ)(id⊗Δ⊗id)(Φ)(Φ⊗1). Each coproduct appears where a component of Φ acts on a two-factor module, by step 1.1; later operators multiply on the left. The products are equal by [F1], and the underlying rebracketing paths agree by [F8], so the pentagon commutes as an equality of H-linear maps.

2.2F1F3F8step 1.3

In the triangle equation, aU,kε,V acts, after rebracketing, by (id⊗ε⊗id)(Φ)=1⊗1. Both composites from (U⊗k)⊗V to U⊗V therefore send (u⊗c)⊗v to cu⊗v=u⊗cv, by the vector-space unit triangle in [F8]. Elementary tensors span, so the triangle commutes.

3.1F6step 1.1step 1.2step 1.3step 2.1step 2.2∎

Steps 1.1–2.2 provide the bifunctor, unit, natural isomorphisms, pentagon, and triangle required by [F6]; hence H-Mod is monoidal with the stated convention.

Depends on

Used by

Dependency tree · two levels

30 results within two dependency steps of this one, each drawn at its shortest distance from it. An arrow runs from a result to what uses it, so the chart reads left to right and ends at this result, which carries a heavier outline. Every node is a link to that result. Click elsewhere on the chart to enlarge it.

Sources