Documentation Verification Report

Classifier

📁 Source: Mathlib/CategoryTheory/Topos/Classifier.lean

Statistics

Metric	Count
Definitions `Classifier`, `SubobjectRepresentableBy`, `classifier`, `isTerminalΩ₀`, `iso`, `isoΩ₀`, `Ω₀`, `π`, `χ`, `χ₀`, `instUniqueHomΩ₀`, `isTerminalΩ₀`, `mkOfTerminalΩ₀`, `representableBy`, `truth`, `truth_as_subobject`, `Ω`, `Ω₀`, `χ`, `χ₀`, `HasClassifier`, `truth`, `truthIsRegularMono`, `Ω`, `Ω₀`, `χ`	26
Theorems `hasTerminal`, `homEquiv_eq`, `isPullback`, `iso_inv_hom_left_comp`, `iso_inv_hom_left_comp_assoc`, `iso_inv_left_comp`, `iso_inv_left_π`, `iso_inv_left_π_assoc`, `pullback_homEquiv_symm_obj_Ω₀`, `uniq`, `isPullback`, `isTerminalFrom_eq_χ₀`, `mkOfTerminalΩ₀_truth`, `mkOfTerminalΩ₀_Ω`, `mkOfTerminalΩ₀_Ω₀`, `mkOfTerminalΩ₀_χ`, `mkOfTerminalΩ₀_χ₀`, `mono_truth`, `pullback_χ_obj_mk_truth`, `surjective_χ`, `uniq`, `χ_pullback_obj_mk_truth_arrow`, `comm`, `comm_assoc`, `exists_classifier`, `instIsRegularMonoTruth`, `isPullback_χ`, `isRegularMonoCategory`, `reflectsIsomorphisms`, `reflectsIsomorphismsOp`, `truthIsSplitMono`, `unique`, `isRepresentable_hasClassifier_iff`	33
Total	59

CategoryTheory

Definitions

Name	Category	Theorems
`Classifier` 📖	CompData	4 math math: `HasClassifier.exists_classifier`, `HasClassifier.comm`, `HasClassifier.isPullback_χ`, `HasClassifier.comm_assoc`
`HasClassifier` 📖	CompData	1 math math: `isRepresentable_hasClassifier_iff`

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`isRepresentable_hasClassifier_iff` 📖	mathematical	—	`HasClassifier` `Functor.IsRepresentable` `Subobject.presheaf`	—	`Functor.RepresentableBy.isRepresentable`

CategoryTheory.Classifier

Definitions

Name	Category	Theorems
`SubobjectRepresentableBy` 📖	CompOp	—
`instUniqueHomΩ₀` 📖	CompOp	—
`isTerminalΩ₀` 📖	CompOp	1 math math: `isTerminalFrom_eq_χ₀`
`mkOfTerminalΩ₀` 📖	CompOp	5 math math: `mkOfTerminalΩ₀_truth`, `mkOfTerminalΩ₀_χ`, `mkOfTerminalΩ₀_χ₀`, `mkOfTerminalΩ₀_Ω`, `mkOfTerminalΩ₀_Ω₀`
`representableBy` 📖	CompOp	—
`truth` 📖	CompOp	3 math math: `mkOfTerminalΩ₀_truth`, `isPullback`, `mono_truth`
`truth_as_subobject` 📖	CompOp	2 math math: `pullback_χ_obj_mk_truth`, `χ_pullback_obj_mk_truth_arrow`
`Ω` 📖	CompOp	5 math math: `pullback_χ_obj_mk_truth`, `χ_pullback_obj_mk_truth_arrow`, `mkOfTerminalΩ₀_Ω`, `isPullback`, `mono_truth`
`Ω₀` 📖	CompOp	7 math math: `isTerminalFrom_eq_χ₀`, `CategoryTheory.HasClassifier.comm`, `CategoryTheory.HasClassifier.isPullback_χ`, `mkOfTerminalΩ₀_Ω₀`, `CategoryTheory.HasClassifier.comm_assoc`, `isPullback`, `mono_truth`
`χ` 📖	CompOp	6 math math: `pullback_χ_obj_mk_truth`, `χ_pullback_obj_mk_truth_arrow`, `mkOfTerminalΩ₀_χ`, `surjective_χ`, `uniq`, `isPullback`
`χ₀` 📖	CompOp	6 math math: `mkOfTerminalΩ₀_χ₀`, `isTerminalFrom_eq_χ₀`, `CategoryTheory.HasClassifier.comm`, `CategoryTheory.HasClassifier.isPullback_χ`, `CategoryTheory.HasClassifier.comm_assoc`, `isPullback`

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`isPullback` 📖	mathematical	—	`CategoryTheory.IsPullback` `Ω₀` `Ω` `χ₀` `χ` `truth`	—	—
`isTerminalFrom_eq_χ₀` 📖	mathematical	—	`CategoryTheory.Limits.IsTerminal.from` `Ω₀` `isTerminalΩ₀` `χ₀`	—	—
`mkOfTerminalΩ₀_truth` 📖	mathematical	`CategoryTheory.IsPullback` `CategoryTheory.Limits.IsTerminal.from`	`truth` `mkOfTerminalΩ₀`	—	—
`mkOfTerminalΩ₀_Ω` 📖	mathematical	`CategoryTheory.IsPullback` `CategoryTheory.Limits.IsTerminal.from`	`Ω` `mkOfTerminalΩ₀`	—	—
`mkOfTerminalΩ₀_Ω₀` 📖	mathematical	`CategoryTheory.IsPullback` `CategoryTheory.Limits.IsTerminal.from`	`Ω₀` `mkOfTerminalΩ₀`	—	—
`mkOfTerminalΩ₀_χ` 📖	mathematical	`CategoryTheory.IsPullback` `CategoryTheory.Limits.IsTerminal.from`	`χ` `mkOfTerminalΩ₀`	—	—
`mkOfTerminalΩ₀_χ₀` 📖	mathematical	`CategoryTheory.IsPullback` `CategoryTheory.Limits.IsTerminal.from`	`χ₀` `mkOfTerminalΩ₀`	—	—
`mono_truth` 📖	mathematical	—	`CategoryTheory.Mono` `Ω₀` `Ω` `truth`	—	—
`pullback_χ_obj_mk_truth` 📖	mathematical	—	`CategoryTheory.Functor.obj` `CategoryTheory.Subobject` `Ω` `Preorder.smallCategory` `PartialOrder.toPreorder` `CategoryTheory.instPartialOrderSubobject` `CategoryTheory.Subobject.pullback` `χ` `truth_as_subobject`	—	`mono_truth` `CategoryTheory.IsPullback.flip` `isPullback`
`surjective_χ` 📖	mathematical	—	`χ`	—	`CategoryTheory.Limits.hasLimitOfHasLimitsOfShape` `CategoryTheory.Limits.pullback.fst_of_mono` `mono_truth` `uniq` `CategoryTheory.IsPullback.of_hasPullback`
`uniq` 📖	mathematical	`CategoryTheory.IsPullback` `Ω₀` `Ω` `truth`	`χ`	—	—
`χ_pullback_obj_mk_truth_arrow` 📖	mathematical	—	`χ` `CategoryTheory.Functor.obj` `CategoryTheory.Subobject` `Preorder.smallCategory` `PartialOrder.toPreorder` `CategoryTheory.instPartialOrderSubobject` `CategoryTheory.Subobject.underlying` `Ω` `CategoryTheory.Subobject.pullback` `truth_as_subobject` `CategoryTheory.Subobject.arrow` `CategoryTheory.Subobject.arrow_mono`	—	`CategoryTheory.Subobject.arrow_mono` `surjective_χ` `uniq` `CategoryTheory.IsPullback.of_iso` `CategoryTheory.Limits.hasLimitOfHasLimitsOfShape` `CategoryTheory.IsPullback.flip` `CategoryTheory.IsPullback.of_hasPullback` `mono_truth` `CategoryTheory.Iso.eq_inv_comp` `CategoryTheory.Category.comp_id` `CategoryTheory.Limits.IsTerminal.hom_ext` `CategoryTheory.Category.id_comp`

CategoryTheory.Classifier.SubobjectRepresentableBy

Definitions

Name	Category	Theorems
`classifier` 📖	CompOp	—
`isTerminalΩ₀` 📖	CompOp	—
`iso` 📖	CompOp	5 math math: `iso_inv_hom_left_comp`, `iso_inv_left_π_assoc`, `iso_inv_hom_left_comp_assoc`, `iso_inv_left_comp`, `iso_inv_left_π`
`isoΩ₀` 📖	CompOp	—
`Ω₀` 📖	CompOp	8 math math: `pullback_homEquiv_symm_obj_Ω₀`, `iso_inv_hom_left_comp`, `homEquiv_eq`, `isPullback`, `iso_inv_left_π_assoc`, `iso_inv_hom_left_comp_assoc`, `iso_inv_left_comp`, `iso_inv_left_π`
`π` 📖	CompOp	3 math math: `isPullback`, `iso_inv_left_π_assoc`, `iso_inv_left_π`
`χ` 📖	CompOp	7 math math: `iso_inv_hom_left_comp`, `uniq`, `isPullback`, `iso_inv_left_π_assoc`, `iso_inv_hom_left_comp_assoc`, `iso_inv_left_comp`, `iso_inv_left_π`
`χ₀` 📖	CompOp	—

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`hasTerminal` 📖	mathematical	—	`CategoryTheory.Limits.HasTerminal`	—	`CategoryTheory.Limits.IsTerminal.hasTerminal`
`homEquiv_eq` 📖	mathematical	—	`DFunLike.coe` `Equiv` `Quiver.Hom` `CategoryTheory.CategoryStruct.toQuiver` `CategoryTheory.Category.toCategoryStruct` `CategoryTheory.Functor.obj` `Opposite` `CategoryTheory.Category.opposite` `CategoryTheory.types` `Subobject.presheaf` `Opposite.op` `EquivLike.toFunLike` `Equiv.instEquivLike` `CategoryTheory.Functor.RepresentableBy.homEquiv` `CategoryTheory.Subobject` `Preorder.smallCategory` `PartialOrder.toPreorder` `CategoryTheory.instPartialOrderSubobject` `CategoryTheory.Subobject.pullback` `Ω₀`	—	`CategoryTheory.Category.comp_id` `CategoryTheory.Functor.RepresentableBy.homEquiv_comp`
`isPullback` 📖	mathematical	—	`CategoryTheory.IsPullback` `CategoryTheory.Functor.obj` `CategoryTheory.Subobject` `Preorder.smallCategory` `PartialOrder.toPreorder` `CategoryTheory.instPartialOrderSubobject` `CategoryTheory.Subobject.underlying` `Ω₀` `π` `χ` `CategoryTheory.Subobject.arrow`	—	`CategoryTheory.IsPullback.of_iso` `CategoryTheory.IsPullback.flip` `CategoryTheory.Subobject.isPullback` `CategoryTheory.Category.comp_id` `iso_inv_hom_left_comp` `iso_inv_left_π` `CategoryTheory.Category.id_comp`
`iso_inv_hom_left_comp` 📖	mathematical	—	`CategoryTheory.CategoryStruct.comp` `CategoryTheory.Category.toCategoryStruct` `CategoryTheory.Comma.left` `CategoryTheory.Discrete` `CategoryTheory.discreteCategory` `CategoryTheory.Functor.id` `CategoryTheory.Functor.fromPUnit` `CategoryTheory.ObjectProperty.FullSubcategory.obj` `CategoryTheory.Over` `CategoryTheory.instCategoryOver` `CategoryTheory.Over.isMono` `CategoryTheory.Functor.obj` `CategoryTheory.Subobject` `Preorder.smallCategory` `PartialOrder.toPreorder` `CategoryTheory.instPartialOrderSubobject` `CategoryTheory.MonoOver` `CategoryTheory.ObjectProperty.FullSubcategory.category` `CategoryTheory.Subobject.representative` `CategoryTheory.Subobject.pullback` `χ` `Ω₀` `CategoryTheory.CommaMorphism.left` `CategoryTheory.InducedCategory.Hom.hom` `CategoryTheory.ObjectProperty.FullSubcategory` `CategoryTheory.Iso.inv` `iso` `CategoryTheory.Subobject.arrow`	—	`CategoryTheory.MonoOver.w`
`iso_inv_hom_left_comp_assoc` 📖	mathematical	—	`CategoryTheory.CategoryStruct.comp` `CategoryTheory.Category.toCategoryStruct` `CategoryTheory.Comma.left` `CategoryTheory.Discrete` `CategoryTheory.discreteCategory` `CategoryTheory.Functor.id` `CategoryTheory.Functor.fromPUnit` `CategoryTheory.ObjectProperty.FullSubcategory.obj` `CategoryTheory.Over` `CategoryTheory.instCategoryOver` `CategoryTheory.Over.isMono` `CategoryTheory.Functor.obj` `CategoryTheory.Subobject` `Preorder.smallCategory` `PartialOrder.toPreorder` `CategoryTheory.instPartialOrderSubobject` `CategoryTheory.MonoOver` `CategoryTheory.ObjectProperty.FullSubcategory.category` `CategoryTheory.Subobject.representative` `CategoryTheory.Subobject.pullback` `χ` `Ω₀` `CategoryTheory.CommaMorphism.left` `CategoryTheory.InducedCategory.Hom.hom` `CategoryTheory.ObjectProperty.FullSubcategory` `CategoryTheory.Iso.inv` `iso` `CategoryTheory.Subobject.arrow`	—	`CategoryTheory.Category.assoc` `Mathlib.Tactic.Reassoc.eq_whisker'` `iso_inv_hom_left_comp`
`iso_inv_left_comp` 📖	mathematical	—	`CategoryTheory.CategoryStruct.comp` `CategoryTheory.Category.toCategoryStruct` `CategoryTheory.Comma.left` `CategoryTheory.Discrete` `CategoryTheory.discreteCategory` `CategoryTheory.Functor.id` `CategoryTheory.Functor.fromPUnit` `CategoryTheory.ObjectProperty.FullSubcategory.obj` `CategoryTheory.Over` `CategoryTheory.instCategoryOver` `CategoryTheory.Over.isMono` `CategoryTheory.Functor.obj` `CategoryTheory.Subobject` `Preorder.smallCategory` `PartialOrder.toPreorder` `CategoryTheory.instPartialOrderSubobject` `CategoryTheory.MonoOver` `CategoryTheory.ObjectProperty.FullSubcategory.category` `CategoryTheory.Subobject.representative` `CategoryTheory.Subobject.pullback` `χ` `Ω₀` `CategoryTheory.CommaMorphism.left` `CategoryTheory.InducedCategory.Hom.hom` `CategoryTheory.ObjectProperty.FullSubcategory` `CategoryTheory.Iso.inv` `iso` `CategoryTheory.Subobject.arrow`	—	`iso_inv_hom_left_comp`
`iso_inv_left_π` 📖	mathematical	—	`CategoryTheory.CategoryStruct.comp` `CategoryTheory.Category.toCategoryStruct` `CategoryTheory.Comma.left` `CategoryTheory.Discrete` `CategoryTheory.discreteCategory` `CategoryTheory.Functor.id` `CategoryTheory.Functor.fromPUnit` `CategoryTheory.ObjectProperty.FullSubcategory.obj` `CategoryTheory.Over` `CategoryTheory.instCategoryOver` `CategoryTheory.Over.isMono` `CategoryTheory.Functor.obj` `CategoryTheory.Subobject` `Preorder.smallCategory` `PartialOrder.toPreorder` `CategoryTheory.instPartialOrderSubobject` `CategoryTheory.MonoOver` `CategoryTheory.ObjectProperty.FullSubcategory.category` `CategoryTheory.Subobject.representative` `CategoryTheory.Subobject.pullback` `χ` `Ω₀` `CategoryTheory.Subobject.underlying` `CategoryTheory.CommaMorphism.left` `CategoryTheory.InducedCategory.Hom.hom` `CategoryTheory.ObjectProperty.FullSubcategory` `CategoryTheory.Iso.inv` `iso` `π` `CategoryTheory.Subobject.pullbackπ`	—	`CategoryTheory.Over.comp_left_assoc` `CategoryTheory.Functor.congr_map` `CategoryTheory.Iso.inv_hom_id` `CategoryTheory.Category.id_comp`
`iso_inv_left_π_assoc` 📖	mathematical	—	`CategoryTheory.CategoryStruct.comp` `CategoryTheory.Category.toCategoryStruct` `CategoryTheory.Comma.left` `CategoryTheory.Discrete` `CategoryTheory.discreteCategory` `CategoryTheory.Functor.id` `CategoryTheory.Functor.fromPUnit` `CategoryTheory.ObjectProperty.FullSubcategory.obj` `CategoryTheory.Over` `CategoryTheory.instCategoryOver` `CategoryTheory.Over.isMono` `CategoryTheory.Functor.obj` `CategoryTheory.Subobject` `Preorder.smallCategory` `PartialOrder.toPreorder` `CategoryTheory.instPartialOrderSubobject` `CategoryTheory.MonoOver` `CategoryTheory.ObjectProperty.FullSubcategory.category` `CategoryTheory.Subobject.representative` `CategoryTheory.Subobject.pullback` `χ` `Ω₀` `CategoryTheory.CommaMorphism.left` `CategoryTheory.InducedCategory.Hom.hom` `CategoryTheory.ObjectProperty.FullSubcategory` `CategoryTheory.Iso.inv` `iso` `CategoryTheory.Subobject.underlying` `π` `CategoryTheory.Subobject.pullbackπ`	—	`CategoryTheory.Category.assoc` `Mathlib.Tactic.Reassoc.eq_whisker'` `iso_inv_left_π`
`pullback_homEquiv_symm_obj_Ω₀` 📖	mathematical	—	`CategoryTheory.Functor.obj` `CategoryTheory.Subobject` `Preorder.smallCategory` `PartialOrder.toPreorder` `CategoryTheory.instPartialOrderSubobject` `CategoryTheory.Subobject.pullback` `DFunLike.coe` `Equiv` `Opposite` `CategoryTheory.Category.opposite` `CategoryTheory.types` `Subobject.presheaf` `Opposite.op` `Quiver.Hom` `CategoryTheory.CategoryStruct.toQuiver` `CategoryTheory.Category.toCategoryStruct` `EquivLike.toFunLike` `Equiv.instEquivLike` `Equiv.symm` `CategoryTheory.Functor.RepresentableBy.homEquiv` `Ω₀`	—	`homEquiv_eq` `Equiv.apply_symm_apply`
`uniq` 📖	mathematical	`CategoryTheory.IsPullback` `CategoryTheory.Functor.obj` `CategoryTheory.Subobject` `Preorder.smallCategory` `PartialOrder.toPreorder` `CategoryTheory.instPartialOrderSubobject` `CategoryTheory.Subobject.underlying` `Ω₀` `CategoryTheory.Subobject.arrow`	`χ`	—	`Equiv.injective` `homEquiv_eq` `Equiv.apply_symm_apply` `CategoryTheory.Subobject.arrow_mono` `CategoryTheory.Subobject.mk_arrow` `CategoryTheory.IsPullback.flip`

CategoryTheory.HasClassifier

Definitions

Name	Category	Theorems
`truth` 📖	CompOp	5 math math: `instIsRegularMonoTruth`, `comm`, `truthIsSplitMono`, `isPullback_χ`, `comm_assoc`
`truthIsRegularMono` 📖	CompOp	—
`Ω` 📖	CompOp	5 math math: `instIsRegularMonoTruth`, `comm`, `truthIsSplitMono`, `isPullback_χ`, `comm_assoc`
`Ω₀` 📖	CompOp	2 math math: `instIsRegularMonoTruth`, `truthIsSplitMono`
`χ` 📖	CompOp	4 math math: `comm`, `isPullback_χ`, `comm_assoc`, `unique`

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`comm` 📖	mathematical	—	`CategoryTheory.CategoryStruct.comp` `CategoryTheory.Category.toCategoryStruct` `Ω` `χ` `CategoryTheory.Classifier.Ω₀` `Nonempty.some` `CategoryTheory.Classifier` `exists_classifier` `CategoryTheory.Classifier.χ₀` `truth`	—	`CategoryTheory.CommSq.w` `exists_classifier` `CategoryTheory.IsPullback.toCommSq` `isPullback_χ`
`comm_assoc` 📖	mathematical	—	`CategoryTheory.CategoryStruct.comp` `CategoryTheory.Category.toCategoryStruct` `Ω` `χ` `CategoryTheory.Classifier.Ω₀` `Nonempty.some` `CategoryTheory.Classifier` `exists_classifier` `CategoryTheory.Classifier.χ₀` `truth`	—	`exists_classifier` `CategoryTheory.Category.assoc` `Mathlib.Tactic.Reassoc.eq_whisker'` `comm`
`exists_classifier` 📖	mathematical	—	`CategoryTheory.Classifier`	—	—
`instIsRegularMonoTruth` 📖	mathematical	—	`CategoryTheory.IsRegularMono` `Ω₀` `Ω` `truth`	—	—
`isPullback_χ` 📖	mathematical	—	`CategoryTheory.IsPullback` `CategoryTheory.Classifier.Ω₀` `Nonempty.some` `CategoryTheory.Classifier` `exists_classifier` `Ω` `CategoryTheory.Classifier.χ₀` `χ` `truth`	—	`CategoryTheory.Classifier.isPullback` `exists_classifier`
`isRegularMonoCategory` 📖	mathematical	—	`CategoryTheory.IsRegularMonoCategory`	—	`exists_classifier` `CategoryTheory.CommSq.w` `CategoryTheory.IsPullback.toCommSq` `isPullback_χ`
`reflectsIsomorphisms` 📖	mathematical	—	`CategoryTheory.Functor.ReflectsIsomorphisms`	—	`CategoryTheory.reflectsIsomorphisms_of_reflectsMonomorphisms_of_reflectsEpimorphisms` `CategoryTheory.balanced_of_strongMonoCategory` `CategoryTheory.strongMonoCategory_of_regularMonoCategory` `isRegularMonoCategory` `CategoryTheory.Functor.reflectsMonomorphisms_of_faithful` `CategoryTheory.Functor.reflectsEpimorphisms_of_faithful`
`reflectsIsomorphismsOp` 📖	mathematical	—	`CategoryTheory.Functor.ReflectsIsomorphisms` `Opposite` `CategoryTheory.Category.opposite`	—	`CategoryTheory.reflectsIsomorphisms_of_reflectsMonomorphisms_of_reflectsEpimorphisms` `CategoryTheory.balanced_opposite` `CategoryTheory.balanced_of_strongMonoCategory` `CategoryTheory.strongMonoCategory_of_regularMonoCategory` `isRegularMonoCategory` `CategoryTheory.Functor.reflectsMonomorphisms_of_faithful` `CategoryTheory.Functor.reflectsEpimorphisms_of_faithful`
`truthIsSplitMono` 📖	mathematical	—	`CategoryTheory.IsSplitMono` `Ω₀` `Ω` `truth`	—	`CategoryTheory.Limits.IsTerminal.isSplitMono_from` `exists_classifier`
`unique` 📖	mathematical	`CategoryTheory.IsPullback` `CategoryTheory.Classifier.Ω₀` `Nonempty.some` `CategoryTheory.Classifier` `exists_classifier` `Ω` `CategoryTheory.Classifier.χ₀` `truth`	`χ`	—	`exists_classifier` `CategoryTheory.Classifier.uniq`

---

← Back to Index