fundamental_topos_theory.toml

id = "fundamental_topos_theory"
title = "Fundamental theorem of topos theory"
test = false
module = "LeanEval.CategoryTheory.FundamentalTopos"
holes = ["fundamental_topos_theory"]
submitter = "Kim Morrison"
notes = "The slice category E/X of an elementary topos E is again an elementary topos. The trusted helper IsTopos (non-hole) bundles finite limits + cartesian-closed (CartesianMonoidalCategory + MonoidalClosed) + a subobject classifier. Mathlib has finite limits and cartesian-monoidal structure on Over X and a HasSubobjectClassifier class, but neither MonoidalClosed (Over X) (the locally-cartesian-closed upgrade) nor HasSubobjectClassifier (Over X). Candidate from §54 of the Knill survey."
source = "F. W. Lawvere & M. Tierney (elementary topos, 1970); see S. Mac Lane & I. Moerdijk, *Sheaves in Geometry and Logic*, IV.7. Knill, *Some fundamental theorems in mathematics*, §54."
informal_solution = "Reconstruct the three topos structures on E/X from those on E. Finite limits in the slice come from the comma-category construction (already in Mathlib). Cartesian closedness is the locally-cartesian-closed upgrade: the pullback functor f* : E/Y → E/X has a right adjoint Π_f (dependent product), built from exponentials in E; this gives internal homs in E/X. The subobject classifier of E/X is (Ω × X → X): a subobject of (A → X) is classified by composing A's characteristic map with the projection. Verifying the pullback/universal properties (Mac Lane–Moerdijk IV.7) is the substantive work."