LemmaStatement: Literature-sourcedProof: AI-adaptedPipeline-generated

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.

The braided tensor product of separable algebras is separable

Statement

Let $C$ be a braided fusion category and let $A, B$ be separable algebra objects, with bimodule sections $σ_{A}, σ_{B}$ . Give $A \otimes B$ the braided tensor-product algebra structure from A braiding gives the tensor product algebra structure. A separability section is $σ_{A \otimes B} = (1_{A} \otimes c_{B, A}^{- 1} \otimes 1_{B}) \circ (σ_{A} \otimes σ_{B}) : A \otimes B ⟶ (A \otimes B) \otimes (A \otimes B) .$ This is an $A \otimes B$ -bimodule map and its composite with multiplication is the identity.

Facts & Assumptions

Given: A braided fusion category and separable algebras $A, B$ with the chosen bimodule sections.

[F1]

Separable algebra objects and bimodules in a fusion category gives the two bimodule-section equations and the section identity.

[F2]

A braiding gives the tensor product algebra structure gives the positive braided tensor-product multiplication; naturality and both braiding hexagons hold.

Proof

1.1F1F2givenalgebra

Let D=C⊠C, whose objects needed here are pairs, with componentwise tensor. Define T(U,V)=U⊗V and strong tensorator t_{(U,V),(U',V')}=1_U⊗c_{V,U'}⊗1_{V'} : UVU'V'→UU'VV'.

1.2F1F2givenalgebra

The tensorator pentagon compares three such pairs. Expanding crossings past products by the two hexagons leaves crossings V1 past U2,U3 and V2 past U3; the two crossings on disjoint slots commute. Thus the two composites coincide. Unit coherence follows from the braiding unit equation. This proves T strong monoidal without a strictification theorem: insert the given associations and its pentagon throughout.

1.3F1F2givenalgebra

For R=(A,B), put mu=(m_A,m_B), s=(sigma_A,sigma_B). In D, mu s=id and s mu=(mu⊗id)(id⊗s)=(id⊗mu)(s⊗id), componentwise. Put K=T(R), m=T(mu)t, sigma=t^{-1}T(s). Naturality of t and its just-proved coherence transport the THREE equations to m sigma=id_K, sigma m=(m⊗id_K)(id_K⊗sigma), sigma m=(id_K⊗m)(sigma⊗id_K).

2.1F1F2givenalgebra∎

For clarity the first left-linearity transport starts with t^{-1} T(s mu)t; replace s mu by (mu⊗id)(id⊗s), use naturality to move T(s) to the last two inputs, and use the tensorator pentagon to replace the two intervening tensorators by (t⊗id)(id⊗t^{-1}). This is exactly (T(mu)t⊗id)(id⊗t^{-1}T(s)). The right-linearity calculation replaces s mu by (id⊗mu)(s⊗id) and gives (id⊗T(mu)t)(t^{-1}T(s)⊗id) in the same way. These are both linearity composites, not merely a multiplication/section cancellation. Expanding t gives exactly the candidate sigma=(1_A⊗c_{B,A}^{-1}⊗1_B)(sigma_A⊗sigma_B).

Depends on

Used by

Dependency tree · two levels

5 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

Douglas and Reutter, Fusion 2-Categories and a State-Sum Invariant for 4-Manifolds, Construction 2.1.19 (standard reference, not scraped)
Décoppet, The Relative Deligne Tensor Product over Pointed Braided Fusion Categories, §1 (standard reference, not scraped)