Theorem CategoryTheory.Classifier.SubobjectRepresentableBy.iso_inv_left_comp

Modification history

2025-12-18 13:14

Mathlib/CategoryTheory/Topos/Classifier.lean

refactor(CategoryTheory): make morphisms in full subcategories a 1-field structure (#26446) …

Deleted CategoryTheory.Classifier.SubobjectRepresentableBy.iso_inv_left_comp View on Github →

2025-05-20 10:01

Mathlib/CategoryTheory/Topos/Classifier.lean

feat(CategoryTheory/Topos): add representability results for subobject classifier (#22881) …

Added CategoryTheory.Classifier.SubobjectRepresentableBy.iso_inv_left_comp View on Github →