Alphabeta Math
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.

6 results · all verified · 2 also independently AI-judged
Every result on this page is machine-checked by a proof checker and read in full and owner-audited; the judge is an additional, independent cross-model AI review of the proofs. The 4 not AI-judged were verified by owner audit (typically over a confirmed judge false positive), not failures.

Closed Monoidal Categories and the Internal Hom - Examples

1 · Prerequisites

2 · Summary

These examples compute the universal maps from the A page in concrete settings: function sets in Set, the Hom-tensor adjunction in Ab, exponential objects in Cat, dependent products in slices of Set, and a subobject classifier in a small presheaf category.

3 · Logical flowchart

4 · Definitions, theorems and proofs

None yet.

5 · Examples, counterexamples and false statements

ExampleConstruction: AI-generatedVerification: AI-generatedprecheck passjudge pass (gpt-5.6-terra)audited 2026-09-01 rests on unproved material (inherited)Open item page →
Rests on 3 statements not proved in this library, by way of the results it cites. This item cites no such statement directly; it depends on results that do. The unproved premises it inherits are Cohen's first model: an infinite Dedekind-finite set of reals, Sierpiński 1947: the generalised continuum hypothesis implies the Axiom of Choice and The continuum hypothesis and its generalisation are independent of ZFC. Each is recorded with a citation to the literature and is not established here, because the track that would prove it has not yet been developed in this library. Everything else in this proof is proved here.

A function set computed as an exponential object

Example

Take B={0,1} and C={x,y}. Then CB is the four-element set of functions BC:

xx,  xy,  yx,  yy,

where, for instance, xy means 0x and 1y.

Facts & Assumptions

Given: The sets B={0,1}, C={x,y}, and A={}.

[L1]

In Set, function sets are exponential objects (Set is cartesian closed).

Verification

technique · direct
1.1

The evaluation map is ev:CB×BC, (ϕ,b)ϕ(b). For example, ev(xy,0)=x and ev(xy,1)=y.

givenalgebra
2.1

Let A={}. A map A×BC is just a function BC, so it is exactly one of the four displayed elements of CB. Hence maps A×BC biject with maps ACB by sending the unique point of A to the corresponding function.

step 1.1givenalgebra
3.1

This is the exponential universal property in the concrete case, matching Set is cartesian closed.

step 2.1L1
ExampleConstruction: AI-generatedVerification: AI-generatedprecheck passaudited 2026-09-01Open item page →

Currying for sets of three variables

Example

Let A=B=C={0,1} and D={0,1,2,3}. Define

f:A×B×CD,f(a,b,c)=a+b+c,

where the sum is taken in the integers.

Facts & Assumptions

Given: The concrete map f(a,b,c)=a+b+c on {0,1}3.

[L1]

Currying and uncurrying are mutually inverse, and repeated currying is associative up to reassociation (Currying and uncurrying are mutually inverse).

Verification

technique · direct
1.1

Currying in the C-variable sends (a,b) to the function ca+b+c. Currying again in the B-variable sends a to the function b(ca+b+c).

givenalgebra
2.1

Uncurrying the result reverses those two assignments: from a recover the map b(ca+b+c), then evaluate at (b,c) to recover a+b+c=f(a,b,c).

step 1.1algebra
3.1

So the twice-curried and twice-uncurried maps return the original f, exactly as Currying and uncurrying are mutually inverse predicts.

step 2.1L1
ExampleConstruction: AI-generatedVerification: AI-generatedprecheck passjudge pass (gpt-5.6-terra)audited 2026-09-01Open item page →

The internal hom of abelian groups

Example

In Ab, viewed as Z-Mod, the internal hom from B to C is the abelian group HomZ(B,C).

Facts & Assumptions

Given: Abelian groups A,B,C.

[L1]

In a right-closed monoidal category, an internal hom is determined by its evaluation-transposition bijection (The internal hom and its evaluation morphism).

[L2]

The Hom-tensor adjunction holds for modules over a commutative ring, hence for abelian groups (Hom-tensor adjunction: HomR(MRN,P)HomR(M,HomR(N,P))).

Verification

technique · direct
1.1

The evaluation morphism is the group homomorphism ev:HomZ(B,C)ZBC, ϕbϕ(b). It is bilinear, so it is well defined.

givenalgebra
2.1

By Hom-tensor adjunction: HomR(MRN,P)HomR(M,HomR(N,P)), for every abelian group A there is a natural isomorphism Hom(AB,C)Hom(A,Hom(B,C)). This is exactly the transposition property from The internal hom and its evaluation morphism.

step 1.1L1L2
3.1

Therefore HomZ(B,C) is the internal hom in Ab.

step 2.1L1
ExampleConstruction: AI-generatedVerification: AI-generatedprecheck passaudited 2026-09-01 rests on unproved material (inherited)Open item page →
Rests on 3 statements not proved in this library, by way of the results it cites. This item cites no such statement directly; it depends on results that do. The unproved premises it inherits are Cohen's first model: an infinite Dedekind-finite set of reals, Sierpiński 1947: the generalised continuum hypothesis implies the Axiom of Choice and The continuum hypothesis and its generalisation are independent of ZFC. Each is recorded with a citation to the literature and is not established here, because the track that would prove it has not yet been developed in this library. Everything else in this proof is proved here.

The exponential of two small categories computed on a walking-arrow source

Example

Let I be the walking-arrow category with objects 0,1 and one nonidentity arrow u:01. For any small category E, a functor IE is exactly an arrow of E.

Facts & Assumptions

Given: The walking-arrow category I and a small category E.

[L1]

In Cat, the exponential by I is the functor category [I,E] (The category of small categories is cartesian closed).

Verification

technique · direct
1.1

To give a functor F:IE is to choose the two objects F(0),F(1) and the image F(u):F(0)F(1). Thus the objects of the exponential EI are precisely the arrows of E.

givenalgebra
2.1

A morphism between two such functors is a natural transformation, so it is exactly a commutative square in E. Therefore EI is the arrow category of E.

step 1.1algebra
3.1

This is the concrete exponential object described by The category of small categories is cartesian closed: functors C×IE curry to functors CEI.

step 2.1L1
ExampleConstruction: AI-generatedVerification: AI-generatedprecheck passaudited 2026-09-01Open item page →

A slice of Set computed as a locally cartesian closed category

Example

Let f:XY be the function with X={a,b,c}, Y={0,1}, and

f(a)=0,f(b)=0,f(c)=1.

Let p:EX have fibers Ea={u,v}, Eb={w}, and Ec={z}.

Facts & Assumptions

Given: The displayed finite sets and maps over X and Y.

[L1]

Set is locally cartesian closed, so each pullback functor has a right adjoint Πf (Set is locally cartesian closed).

[L2]

Slice objects and pullback functors are defined as in Slice categories, composition, and pullback along a morphism.

Verification

technique · direct
1.1

The dependent product ΠfEY has fiber over 0 equal to Ea×Eb={(u,w),(v,w)} and fiber over 1 equal to Ec={z}. So ΠfE has three elements in total, two over 0 and one over 1.

givenalgebra
2.1

If q:BY is the singleton fiber over 1, then fqX is the singleton fiber over c, and a map fqp over X is exactly a choice of an element of Ec, namely z. This matches maps qΠfE over Y, which must choose the unique element over 1.

step 1.1algebra
3.1

This concrete fiber computation realizes the pullback/right-adjoint pattern guaranteed by Set is locally cartesian closed, using the slice formalism of Slice categories, composition, and pullback along a morphism.

step 2.1L1L2
ExampleConstruction: AI-generatedVerification: AI-generatedprecheck passaudited 2026-09-01Open item page →

The subobject classifier in a presheaf category on the walking arrow

Example

Let I be the walking-arrow category 0u1, and work in the presheaf category SetIop. The subobject classifier Ω sends an object to its set of sieves:

  • Ω(0)={,{10}},
  • Ω(1)={,{u},{u,11}}.

The truth morphism true:1Ω selects the maximal sieve at each object. For any presheaf P and subpresheaf SP, its characteristic morphism is χS,c(x)={f:dc:P(f)(x)S(d)}.

Facts & Assumptions

Given: The walking-arrow category I, the sieve presheaf Ω, and the subpresheaf Sy(1) defined below.

[L1]

A subobject classifier classifies subobjects by pullback of truth (Subobject classifier).

Verification

technique · direct
1.1

On the walking arrow, the arrows into 0 are only 10, so its sieves are and {10}. The arrows into 1 are u and 11, and downward closure forces any sieve containing 11 also to contain u, giving exactly the three displayed sieves on 1. Pullback of sieves makes Ω a presheaf, and the maximal sieves define the natural truth morphism above.

givenconstructalgebra
2.1

Consider the representable presheaf y(1) (The Yoneda assignment and the small-source Yoneda functor, traditionally called the Yoneda embedding) and the subpresheaf Sy(1) defined by S(1)= and S(0)={u}. Its characteristic map χ:y(1)Ω sends the unique element uy(1)(0) to the maximal sieve {10}, and sends 11y(1)(1) to the sieve {u}.

step 1.1givenconstruct
2.2

For a general subpresheaf TP, the displayed formula defines a sieve and is natural under restriction. Moreover χT,c(x) is maximal exactly when xT(c): the forward implication tests 1c, and the reverse follows from closure of the subpresheaf under restriction. Thus pulling back true along χT recovers T, and this condition uniquely determines χT. By [L1], Ω is a subobject classifier.

step 1.1L1constructalgebra
3.1

For the concrete Sy(1) of step 2.1, that pullback includes u at object 0 because χ0(u)={10} is maximal, and excludes 11 at object 1 because χ1(11)={u} is not maximal. Hence the general classifier calculation gives exactly the displayed example.

step 2.1step 2.2algebra

Sources