Commit 2025-07-15 08:52 40b305cc

feat(CategoryTheory/Topos): subobject classifier without limits (#26556) Adds an alternative API for constructing a subobject classifier without reference to limits. This PR modifies two files:

• Mathlib/CategoryTheory/Limits/Shapes/Pullback/CommSq.lean: Adds strengthened versions of two existing theorems:
  • of_horiz_isIso_mono (alongside the existing of_horiz_isIso)
  • of_vert_isIso_mono (alongside the existing of_vert_isIso)
• Mathlib/CategoryTheory/Topos/Classifier.lean: Addresses the TODO (removed from the file):

  Make API for constructing a subobject classifier without reference to limits (replacing ⊤_ C with an arbitrary Ω₀ : C and including the assumption mono truth) This implementation accepts a monomorphism truth : Ω₀ ⟶ Ω such that for every monomorphism m : U ⟶ X there exists a pair χ₀ : U ⟶ Ω₀ and χ : X ⟶ Ω which creates a pullback square and χ must be unique in that it admits such a pair. Given these assumptions, we construct an instance of the existing Classifier structure, alongside with a proof that Ω₀ is terminal. Klaus Gy klausgy@gmail.com