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.

The category of right-module endofunctors

Definition

Let (C,⊗,1,α,λ,ρ) be a monoidal category (Monoidal category).

The category of right-module endofunctors C′ has:

  • objects given by pairs (F,c) where F:C→C is a functor (Covariant functor, identity functor, composite functor, and contravariant functor) and cX,Y:F(X)⊗Y⟶F(X⊗Y) is a natural isomorphism (Natural isomorphism) in X and Y such that F(αX,Y,Z)∘cX⊗Y,Z∘(cX,Y⊗1Z)=cX,Y⊗Z∘αF(X),Y,Z and F(ρX)∘cX,1=ρF(X);
  • morphisms (F,c)→(G,d) given by natural transformations θ:F⇒G (Natural transformation and its components) satisfying θX⊗Y∘cX,Y=dX,Y∘(θX⊗1Y) for all objects X,Y.

Identities and composition are inherited from natural transformations: the identity transformation satisfies the compatibility equation immediately, and if θ:(F,c)⇒(G,d) and η:(G,d)⇒(H,e) are compatible, then substituting their two equations shows that η∘θ is compatible as well. Associativity and the identity laws are therefore inherited from vertical composition of natural transformations.

Thus an object of C′ is an endofunctor equipped with a coherent way to slide a tensor factor on the right through the functor.

Depends on

Used by

Dependency tree · two levels

10 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