Commit 2025-05-20 10:01 a228b7f6

feat(CategoryTheory/Topos): add representability results for subobject classifier (#22881) We add a section Representability at the end of Mathlib.CategoryTheory.Topos.Classifier where we formalize the necessary lemmas and definitions that lead to the proof of CategoryTheory.isRepresentable_hasClassifier_iff, which states that a category C has a subobject classifier if and only if the subobjects presheaf CategoryTheory.Subobject.presheaf C is representable (Proposition 1 in Section I.3 of Sheaves in Geometry and Logic [MM92]). The toughest part is found in definition CategoryTheory.Classifier.fromRepresentation, which formalizes as closely as possible the argument given in [MM92, pp. 33-34].