Commit 2026-03-06 00:15 89c5d63b

View on Github →

feat(CategoryTheory/Topos/Classifier): subobject classifiers, isos and equivalences (#35895) this PR adds Classifier.ofEquivalence, Classifier.ofIso and Classifier.uniqueUpToIso, as well as accompanying lemmas

Estimated changes

Modified Mathlib/CategoryTheory/Topos/Classifier.lean

added def CategoryTheory.Classifier.hom

added theorem CategoryTheory.Classifier.hom_comp_hom

added theorem CategoryTheory.Classifier.hom_refl

added def CategoryTheory.Classifier.ofEquivalence

added def CategoryTheory.Classifier.ofIso

added theorem CategoryTheory.Classifier.truth_comp_hom

added def CategoryTheory.Classifier.uniqueUpToIso

added theorem CategoryTheory.Classifier.χ_comp_hom