Alphabeta Math
DefinitionDefinition: Literature-sourcedProof: Not applicablejudge pass (gpt-5.6-terra)audited 2026-08-31
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.

Lax, strong, and strict monoidal functors

Definition

Let (C,⊗,1,α,λ,ρ) and (D,⊠,1′,α′,λ′,ρ′) be monoidal categories (Monoidal category).

A lax monoidal functor is a functor F:C→D (Covariant functor, identity functor, composite functor, and contravariant functor) together with natural transformations (Natural transformation and its components)

F2;X,Y:F(X)⊠F(Y)⟶F(X⊗Y),

and

the morphism

F0:1′⟶F(1),

such that, for all X,Y,Z,

F(αX,Y,Z)∘F2;X⊗Y,Z∘(F2;X,Y⊠1F(Z))=F2;X,Y⊗Z∘(1F(X)⊠F2;Y,Z)∘αF(X),F(Y),F(Z)′,

F(λX)∘F2;1,X∘(F0⊠1F(X))=λF(X)′,

F(ρX)∘F2;X,1∘(1F(X)⊠F0)=ρF(X)′.

A lax monoidal functor is strong monoidal when the natural transformation F2 is a natural isomorphism (Natural isomorphism)—equivalently, every component F2;X,Y is an isomorphism—and F0 is an isomorphism.

A strong monoidal functor is strict monoidal when the functor preserves the unit and tensor on the nose and every structure map above is an identity.

Depends on

Dependency tree · 2 levels

Sources