Fundamental theorem of topos theory

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.

theorem declaration uses `sorry`fundamental_topos_theory {E : Type*} [Category E]
    (hE : LeanEval.ToposTheory.IsTopos E) (X : E) : LeanEval.ToposTheory.IsTopos (Over X) := byE:Type u_1inst✝:Category.{u_2, u_1} EhE:IsTopos EX:E⊢ IsTopos (Over X)
  sorryAll goals completed! 🐙

Solved by

Not yet solved.