Alphabeta Math
DefinitionDefinition: Literature-sourcedProof: Not applicableaudited 2026-09-05
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.

Enriched category over a monoidal base

Definition

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

A V-enriched category, or V-category, consists of

  • a set Ob⁡(A) of objects;
  • for every ordered pair A,B∈Ob⁡(A), an object A(A,B) of V;
  • for every triple A,B,C, a composition morphism MA,B,C:A(B,C)⊗A(A,B)⟶A(A,C);
  • for every object A, an identity morphism jA:1⟶A(A,A);

such that the following diagrams commute.

For every A,B,C,D, the two composites

((A(C,D)⊗A(B,C))⊗A(A,B))⇉A(A,D)

agree, namely

MA,B,D∘(MB,C,D⊗1)=MA,C,D∘(1⊗MA,B,C)∘αA(C,D),A(B,C),A(A,B).

For every A,B, the left and right unit laws hold:

MA,B,B∘(jB⊗1)∘λA(A,B)−1=1A(A,B),

MA,A,B∘(1⊗jA)∘ρA(A,B)−1=1A(A,B).

The order of the two hom-objects in the tensor product is part of the definition: the factor A(B,C) stands on the left and A(A,B) on the right because composition is "first A→B, then B→C".

Remarks

The object collection is required here to be a set. This is the standing size convention for the present page, and it is what makes later statements about V-Cat honest inside the library's current foundations.

Depends on

Used by

Dependency tree · two levels

4 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