Commit 2025-02-24 22:30 ab84c0ea

feat(CategoryTheory): Define subobject classifier (#21281) This creates the folder CategoryTheory/Topos and the file CategoryTheory/Topos/Classifier.lean. The proposed code includes the definition of what it means to be a subobject classifier in a category C with a terminal object, and relevant basic results about such a category. This is done in the "internal" sense, for the purpose of eventually defining what it means for a category to be a topos utilizing this definition; see also [#21269](https://github.com/leanprover-community/mathlib4/pull/21269).