Alphabeta Math
TheoremStatement: Literature-sourcedProof: AI-adaptedprecheck passjudge pass (gpt-5.6-terra)audited 2026-09-01
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.

Local cartesian closure is equivalent to every pullback functor having a right adjoint

Statement

Let C be a category with chosen pullback functors. Then the following are equivalent.

  1. C is locally cartesian closed.
  2. For every morphism f:XY, the pullback functor f:C/YC/X has a right adjoint.

Facts & Assumptions

Given: A category C with chosen pullback functors.

[L1]

Local cartesian closedness means that every slice category is cartesian closed (Locally cartesian closed category).

[L2]

For each f:XY, the functors Σf and f between slice categories are the postcomposition and pullback functors (Slice categories, composition, and pullback along a morphism).

[L3]

Every slice of a locally cartesian closed category is locally cartesian closed, and every locally cartesian closed category has pullbacks (Slices of a locally cartesian closed category are locally cartesian closed, A locally cartesian closed category has pullbacks, and with a terminal object it has all finite limits).

Proof

technique · iff
1.1

Assume condition (1), fix f:XY, and put K=C/Y. For an object a:AX of C/X, regard a as a morphism Σfaf in K. By [L1] and [L3], the category K is cartesian closed and has pullbacks. Form in K the pullback Πf(a):=(Σfa)f×ff1, where (Σfa)fff is induced by a and 1ff is the transpose of 1f:ff. For BY, currying identifies a map B(Σfa)f with a map h:B×YXA over Y; the pullback equation defining Πf(a) says exactly that ah is the projection B×YXX. Hence (C/Y)(B,Πf(a))(C/X)(fB,a) naturally in B and a. Thus f has right adjoint Πf.

assume-hypL1L2L3constructalgebra
1.2

Assume condition (2), and fix an object X. Chosen pullbacks give binary products in C/X, and 1X:XX is terminal there. For a:AX, the pullback universal property gives Σaa, while condition (2) gives aΠa. The product functor with a on C/X is the composite ×Xa=Σaa. Consequently it has right adjoint Πaa. Since this holds for every a, the slice C/X is cartesian closed.

assume-hypL1L2constructalgebra
2.1

Step 1.1 proves that condition (1) implies condition (2). Step 1.2 proves that each slice C/X is cartesian closed, so condition (2) implies condition (1). Therefore the two conditions are equivalent.

step 1.1step 1.2L1

Depends on

Used by

Dependency tree · two levels

9 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