Defs

📁 Source: Mathlib/CategoryTheory/Subobject/Classifier/Defs.lean

Statistics

Metric	Count
Definitions Classifier, SubobjectRepresentableBy, hom, isTerminalΩ₀, mkOfTerminalΩ₀, ofEquivalence, ofIso, representableBy, truth_as_subobject, uniqueUpToIso, HasClassifier, truth, truthIsRegularMono, Ω, Ω₀, χ, HasSubobjectClassifier, truth, truthIsRegularMono, Ω, Ω₀, χ, Classifier, hom, instUniqueHomΩ₀, isTerminalΩ₀, mkOfTerminalΩ₀, ofEquivalence, ofIso, representableBy, truth, truth_as_subobject, uniqueUpToIso, Ω, Ω₀, χ, χ₀, SubobjectRepresentableBy, classifier, isTerminalΩ₀, iso, isoΩ₀, Ω₀, π, χ, χ₀	46
Theorems hom_comp_hom, hom_refl, isTerminalFrom_eq_χ₀, pullback_χ_obj_mk_truth, surjective_χ, truth_comp_hom, χ_comp_hom, χ_pullback_obj_mk_truth_arrow, comm, isPullback_χ, isRegularMonoCategory, reflectsIsomorphisms, reflectsIsomorphismsOp, truthIsSplitMono, unique, comm, comm_assoc, exists_classifier, instIsRegularMonoTruth, isPullback_χ, isRegularMonoCategory, reflectsIsomorphisms, reflectsIsomorphismsOp, truthIsSplitMono, unique, hom_comp_hom, hom_comp_hom_assoc, hom_refl, instIsIsoHom, isPullback, isTerminalFrom_eq_χ₀, mkOfTerminalΩ₀_truth, mkOfTerminalΩ₀_Ω, mkOfTerminalΩ₀_Ω₀, mkOfTerminalΩ₀_χ, mkOfTerminalΩ₀_χ₀, mono_truth, ofEquivalence_truth, ofEquivalence_Ω, ofEquivalence_Ω₀, ofEquivalence_χ, ofEquivalence_χ₀, ofIso_truth, ofIso_Ω, ofIso_Ω₀, ofIso_χ, ofIso_χ₀, pullback_χ_obj_mk_truth, surjective_χ, truth_comp_hom, truth_comp_hom_assoc, uniq, uniqueUpToIso_hom, uniqueUpToIso_inv, χ_comp_hom, χ_comp_hom_assoc, χ_pullback_obj_mk_truth_arrow, hasTerminal, homEquiv_eq, isPullback, iso_inv_hom_left_comp, iso_inv_hom_left_comp_assoc, iso_inv_left_π, iso_inv_left_π_assoc, pullback_homEquiv_symm_obj_Ω₀, uniq, hasSubobjectClassifier_iff_isRepresentable, isRepresentable_hasClassifier_iff	68
Total	114

CategoryTheory

Definitions

Name	Category	Theorems
Classifier 📖	CompOp	—
HasClassifier 📖	MathDef	—
HasSubobjectClassifier 📖	CompData	4 math math: Sheaf.instHasSubobjectClassifierTypeOfEssentiallySmall, instHasSubobjectClassifierFunctorOppositeTypeOfEssentiallySmall, isRepresentable_hasClassifier_iff, hasSubobjectClassifier_iff_isRepresentable
SubobjectRepresentableBy 📖	CompOp	—

Theorems

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

CategoryTheory.Classifier

Definitions

Name	Category	Theorems
SubobjectRepresentableBy 📖	CompOp	—
hom 📖	CompOp	—
isTerminalΩ₀ 📖	CompOp	—
mkOfTerminalΩ₀ 📖	CompOp	—
ofEquivalence 📖	CompOp	—
ofIso 📖	CompOp	—
representableBy 📖	CompOp	—
truth_as_subobject 📖	CompOp	—
uniqueUpToIso 📖	CompOp	—

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
hom_comp_hom 📖	mathematical	—	CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct CategoryTheory.Subobject.Classifier.Ω CategoryTheory.Subobject.Classifier.hom	—	CategoryTheory.Subobject.Classifier.hom_comp_hom
hom_refl 📖	mathematical	—	CategoryTheory.Subobject.Classifier.hom CategoryTheory.CategoryStruct.id CategoryTheory.Category.toCategoryStruct CategoryTheory.Subobject.Classifier.Ω	—	CategoryTheory.Subobject.Classifier.hom_refl
isTerminalFrom_eq_χ₀ 📖	mathematical	—	CategoryTheory.Limits.IsTerminal.from CategoryTheory.Subobject.Classifier.Ω₀ CategoryTheory.Subobject.Classifier.isTerminalΩ₀ CategoryTheory.Subobject.Classifier.χ₀	—	CategoryTheory.Subobject.Classifier.isTerminalFrom_eq_χ₀
pullback_χ_obj_mk_truth 📖	mathematical	—	CategoryTheory.Functor.obj CategoryTheory.Subobject CategoryTheory.Subobject.Classifier.Ω Preorder.smallCategory PartialOrder.toPreorder CategoryTheory.instPartialOrderSubobject CategoryTheory.Subobject.pullback CategoryTheory.Subobject.Classifier.χ CategoryTheory.Subobject.Classifier.truth_as_subobject	—	CategoryTheory.Subobject.Classifier.pullback_χ_obj_mk_truth
surjective_χ 📖	mathematical	—	Quiver.Hom CategoryTheory.CategoryStruct.toQuiver CategoryTheory.Category.toCategoryStruct CategoryTheory.Mono CategoryTheory.Subobject.Classifier.χ	—	CategoryTheory.Subobject.Classifier.surjective_χ
truth_comp_hom 📖	mathematical	—	CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct CategoryTheory.Subobject.Classifier.Ω₀ CategoryTheory.Subobject.Classifier.Ω CategoryTheory.Subobject.Classifier.truth CategoryTheory.Subobject.Classifier.hom CategoryTheory.Subobject.Classifier.χ₀	—	CategoryTheory.Subobject.Classifier.truth_comp_hom
χ_comp_hom 📖	mathematical	—	CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct CategoryTheory.Subobject.Classifier.Ω CategoryTheory.Subobject.Classifier.χ CategoryTheory.Subobject.Classifier.hom	—	CategoryTheory.Subobject.Classifier.χ_comp_hom
χ_pullback_obj_mk_truth_arrow 📖	mathematical	—	CategoryTheory.Subobject.Classifier.χ CategoryTheory.Functor.obj CategoryTheory.Subobject Preorder.smallCategory PartialOrder.toPreorder CategoryTheory.instPartialOrderSubobject CategoryTheory.Subobject.underlying CategoryTheory.Subobject.Classifier.Ω CategoryTheory.Subobject.pullback CategoryTheory.Subobject.Classifier.truth_as_subobject CategoryTheory.Subobject.arrow CategoryTheory.Subobject.arrow_mono	—	CategoryTheory.Subobject.Classifier.χ_pullback_obj_mk_truth_arrow

CategoryTheory.HasClassifier

Definitions

Name	Category	Theorems
truth 📖	CompOp	—
truthIsRegularMono 📖	CompOp	—
Ω 📖	CompOp	—
Ω₀ 📖	CompOp	—
χ 📖	CompOp	—

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
comm 📖	mathematical	—	CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct CategoryTheory.HasSubobjectClassifier.Ω CategoryTheory.HasSubobjectClassifier.χ CategoryTheory.Subobject.Classifier.Ω₀ Nonempty.some CategoryTheory.Subobject.Classifier CategoryTheory.HasSubobjectClassifier.exists_classifier CategoryTheory.Subobject.Classifier.χ₀ CategoryTheory.HasSubobjectClassifier.truth	—	CategoryTheory.HasSubobjectClassifier.comm
isPullback_χ 📖	mathematical	—	CategoryTheory.IsPullback CategoryTheory.Subobject.Classifier.Ω₀ Nonempty.some CategoryTheory.Subobject.Classifier CategoryTheory.HasSubobjectClassifier.exists_classifier CategoryTheory.HasSubobjectClassifier.Ω CategoryTheory.Subobject.Classifier.χ₀ CategoryTheory.HasSubobjectClassifier.χ CategoryTheory.HasSubobjectClassifier.truth	—	CategoryTheory.HasSubobjectClassifier.isPullback_χ
isRegularMonoCategory 📖	mathematical	—	CategoryTheory.IsRegularMonoCategory	—	CategoryTheory.HasSubobjectClassifier.isRegularMonoCategory
reflectsIsomorphisms 📖	mathematical	—	CategoryTheory.Functor.ReflectsIsomorphisms	—	CategoryTheory.HasSubobjectClassifier.reflectsIsomorphisms
reflectsIsomorphismsOp 📖	mathematical	—	CategoryTheory.Functor.ReflectsIsomorphisms Opposite CategoryTheory.Category.opposite	—	CategoryTheory.HasSubobjectClassifier.reflectsIsomorphismsOp
truthIsSplitMono 📖	mathematical	—	CategoryTheory.IsSplitMono CategoryTheory.HasSubobjectClassifier.Ω₀ CategoryTheory.HasSubobjectClassifier.Ω CategoryTheory.HasSubobjectClassifier.truth	—	CategoryTheory.HasSubobjectClassifier.truthIsSplitMono
unique 📖	mathematical	CategoryTheory.IsPullback CategoryTheory.Subobject.Classifier.Ω₀ Nonempty.some CategoryTheory.Subobject.Classifier CategoryTheory.HasSubobjectClassifier.exists_classifier CategoryTheory.HasSubobjectClassifier.Ω CategoryTheory.Subobject.Classifier.χ₀ CategoryTheory.HasSubobjectClassifier.truth	CategoryTheory.HasSubobjectClassifier.χ	—	CategoryTheory.HasSubobjectClassifier.unique

CategoryTheory.HasSubobjectClassifier

Definitions

Name	Category	Theorems
truth 📖	CompOp	8 math math: truthIsSplitMono, CategoryTheory.HasClassifier.comm, comm_assoc, comm, CategoryTheory.HasClassifier.truthIsSplitMono, instIsRegularMonoTruth, CategoryTheory.HasClassifier.isPullback_χ, isPullback_χ
truthIsRegularMono 📖	CompOp	—
Ω 📖	CompOp	8 math math: truthIsSplitMono, CategoryTheory.HasClassifier.comm, comm_assoc, comm, CategoryTheory.HasClassifier.truthIsSplitMono, instIsRegularMonoTruth, CategoryTheory.HasClassifier.isPullback_χ, isPullback_χ
Ω₀ 📖	CompOp	3 math math: truthIsSplitMono, CategoryTheory.HasClassifier.truthIsSplitMono, instIsRegularMonoTruth
χ 📖	CompOp	7 math math: CategoryTheory.HasClassifier.comm, comm_assoc, comm, unique, CategoryTheory.HasClassifier.isPullback_χ, CategoryTheory.HasClassifier.unique, isPullback_χ

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
comm 📖	mathematical	—	CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct Ω χ CategoryTheory.Subobject.Classifier.Ω₀ Nonempty.some CategoryTheory.Subobject.Classifier exists_classifier CategoryTheory.Subobject.Classifier.χ₀ truth	—	CategoryTheory.CommSq.w exists_classifier CategoryTheory.IsPullback.toCommSq isPullback_χ
comm_assoc 📖	mathematical	—	CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct Ω χ CategoryTheory.Subobject.Classifier.Ω₀ Nonempty.some CategoryTheory.Subobject.Classifier exists_classifier CategoryTheory.Subobject.Classifier.χ₀ truth	—	exists_classifier CategoryTheory.Category.assoc Mathlib.Tactic.Reassoc.eq_whisker' comm
exists_classifier 📖	mathematical	—	CategoryTheory.Subobject.Classifier	—	—
instIsRegularMonoTruth 📖	mathematical	—	CategoryTheory.IsRegularMono Ω₀ Ω truth	—	—
isPullback_χ 📖	mathematical	—	CategoryTheory.IsPullback CategoryTheory.Subobject.Classifier.Ω₀ Nonempty.some CategoryTheory.Subobject.Classifier exists_classifier Ω CategoryTheory.Subobject.Classifier.χ₀ χ truth	—	CategoryTheory.Subobject.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.Subobject.Classifier.Ω₀ Nonempty.some CategoryTheory.Subobject.Classifier exists_classifier Ω CategoryTheory.Subobject.Classifier.χ₀ truth	χ	—	exists_classifier CategoryTheory.Subobject.Classifier.uniq

CategoryTheory.Subobject

Definitions

Name	Category	Theorems
Classifier 📖	CompData	6 math math: CategoryTheory.HasClassifier.comm, CategoryTheory.HasSubobjectClassifier.comm_assoc, CategoryTheory.HasSubobjectClassifier.comm, CategoryTheory.HasSubobjectClassifier.exists_classifier, CategoryTheory.HasClassifier.isPullback_χ, CategoryTheory.HasSubobjectClassifier.isPullback_χ

CategoryTheory.Subobject.Classifier

Definitions

Name	Category	Theorems
hom 📖	CompOp	14 math math: χ_comp_hom, CategoryTheory.Classifier.hom_comp_hom, CategoryTheory.Classifier.truth_comp_hom, instIsIsoHom, CategoryTheory.Classifier.hom_refl, truth_comp_hom_assoc, χ_comp_hom_assoc, CategoryTheory.Classifier.χ_comp_hom, uniqueUpToIso_hom, uniqueUpToIso_inv, truth_comp_hom, hom_comp_hom_assoc, hom_comp_hom, hom_refl
instUniqueHomΩ₀ 📖	CompOp	—
isTerminalΩ₀ 📖	CompOp	2 math math: CategoryTheory.Classifier.isTerminalFrom_eq_χ₀, isTerminalFrom_eq_χ₀
mkOfTerminalΩ₀ 📖	CompOp	5 math math: mkOfTerminalΩ₀_χ₀, mkOfTerminalΩ₀_Ω, mkOfTerminalΩ₀_Ω₀, mkOfTerminalΩ₀_truth, mkOfTerminalΩ₀_χ
ofEquivalence 📖	CompOp	5 math math: ofEquivalence_truth, ofEquivalence_Ω, ofEquivalence_Ω₀, ofEquivalence_χ, ofEquivalence_χ₀
ofIso 📖	CompOp	5 math math: ofIso_Ω₀, ofIso_χ₀, ofIso_Ω, ofIso_χ, ofIso_truth
representableBy 📖	CompOp	—
truth 📖	CompOp	10 math math: mono_truth, ofEquivalence_truth, CategoryTheory.Classifier.truth_comp_hom, CategoryTheory.Sheaf.classifier_truth, truth_comp_hom_assoc, mkOfTerminalΩ₀_truth, CategoryTheory.Presheaf.classifier_truth, ofIso_truth, truth_comp_hom, isPullback
truth_as_subobject 📖	CompOp	4 math math: CategoryTheory.Classifier.pullback_χ_obj_mk_truth, pullback_χ_obj_mk_truth, CategoryTheory.Classifier.χ_pullback_obj_mk_truth_arrow, χ_pullback_obj_mk_truth_arrow
uniqueUpToIso 📖	CompOp	2 math math: uniqueUpToIso_hom, uniqueUpToIso_inv
Ω 📖	CompOp	28 math math: CategoryTheory.Classifier.pullback_χ_obj_mk_truth, mono_truth, ofEquivalence_truth, χ_comp_hom, CategoryTheory.Classifier.hom_comp_hom, ofEquivalence_Ω, mkOfTerminalΩ₀_Ω, pullback_χ_obj_mk_truth, CategoryTheory.Presheaf.classifier_Ω, CategoryTheory.Classifier.truth_comp_hom, CategoryTheory.Sheaf.classifier_Ω, instIsIsoHom, CategoryTheory.Classifier.χ_pullback_obj_mk_truth_arrow, CategoryTheory.Classifier.hom_refl, truth_comp_hom_assoc, χ_comp_hom_assoc, ofIso_Ω, CategoryTheory.Classifier.χ_comp_hom, uniqueUpToIso_hom, ofEquivalence_χ, ofIso_χ, χ_pullback_obj_mk_truth_arrow, uniqueUpToIso_inv, truth_comp_hom, hom_comp_hom_assoc, hom_comp_hom, isPullback, hom_refl
Ω₀ 📖	CompOp	19 math math: mono_truth, ofEquivalence_truth, ofIso_Ω₀, CategoryTheory.Classifier.truth_comp_hom, CategoryTheory.Sheaf.classifier_Ω₀, CategoryTheory.Classifier.isTerminalFrom_eq_χ₀, mkOfTerminalΩ₀_Ω₀, truth_comp_hom_assoc, CategoryTheory.HasClassifier.comm, CategoryTheory.HasSubobjectClassifier.comm_assoc, ofEquivalence_Ω₀, CategoryTheory.HasSubobjectClassifier.comm, ofEquivalence_χ₀, isTerminalFrom_eq_χ₀, truth_comp_hom, CategoryTheory.HasClassifier.isPullback_χ, CategoryTheory.Presheaf.classifier_Ω₀, isPullback, CategoryTheory.HasSubobjectClassifier.isPullback_χ
χ 📖	CompOp	16 math math: CategoryTheory.Classifier.pullback_χ_obj_mk_truth, χ_comp_hom, CategoryTheory.Sheaf.classifier_χ, pullback_χ_obj_mk_truth, CategoryTheory.Presheaf.classifier_χ, uniq, CategoryTheory.Classifier.χ_pullback_obj_mk_truth_arrow, χ_comp_hom_assoc, CategoryTheory.Classifier.χ_comp_hom, ofEquivalence_χ, CategoryTheory.Classifier.surjective_χ, ofIso_χ, χ_pullback_obj_mk_truth_arrow, surjective_χ, mkOfTerminalΩ₀_χ, isPullback
χ₀ 📖	CompOp	16 math math: mkOfTerminalΩ₀_χ₀, CategoryTheory.Classifier.truth_comp_hom, ofIso_χ₀, CategoryTheory.Classifier.isTerminalFrom_eq_χ₀, truth_comp_hom_assoc, CategoryTheory.HasClassifier.comm, CategoryTheory.Sheaf.classifier_χ₀, CategoryTheory.HasSubobjectClassifier.comm_assoc, CategoryTheory.HasSubobjectClassifier.comm, ofEquivalence_χ₀, isTerminalFrom_eq_χ₀, truth_comp_hom, CategoryTheory.HasClassifier.isPullback_χ, CategoryTheory.Presheaf.classifier_χ₀, isPullback, CategoryTheory.HasSubobjectClassifier.isPullback_χ

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
hom_comp_hom 📖	mathematical	—	CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct Ω hom	—	uniq mono_truth CategoryTheory.IsPullback.paste_vert isPullback
hom_comp_hom_assoc 📖	mathematical	—	CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct Ω hom	—	CategoryTheory.Category.assoc Mathlib.Tactic.Reassoc.eq_whisker' hom_comp_hom
hom_refl 📖	mathematical	—	hom CategoryTheory.CategoryStruct.id CategoryTheory.Category.toCategoryStruct Ω	—	mono_truth uniq CategoryTheory.IsPullback.of_id_snd
instIsIsoHom 📖	mathematical	—	CategoryTheory.IsIso Ω hom	—	CategoryTheory.Iso.isIso_hom
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Ω₀ CategoryTheory.Limits.IsTerminal.from	—	—
mono_truth 📖	mathematical	—	CategoryTheory.Mono Ω₀ Ω truth	—	—
ofEquivalence_truth 📖	mathematical	—	truth ofEquivalence CategoryTheory.Functor.map CategoryTheory.Equivalence.functor Ω₀ Ω	—	—
ofEquivalence_Ω 📖	mathematical	—	Ω ofEquivalence CategoryTheory.Functor.obj CategoryTheory.Equivalence.functor	—	—
ofEquivalence_Ω₀ 📖	mathematical	—	Ω₀ ofEquivalence CategoryTheory.Functor.obj CategoryTheory.Equivalence.functor	—	—
ofEquivalence_χ 📖	mathematical	—	χ ofEquivalence CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct CategoryTheory.Functor.obj CategoryTheory.Functor.comp CategoryTheory.Equivalence.inverse CategoryTheory.Equivalence.functor Ω CategoryTheory.NatTrans.app CategoryTheory.Functor.id CategoryTheory.Equivalence.counitInv CategoryTheory.Functor.map	—	—
ofEquivalence_χ₀ 📖	mathematical	—	χ₀ ofEquivalence CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct CategoryTheory.Functor.obj CategoryTheory.Functor.comp CategoryTheory.Equivalence.inverse CategoryTheory.Equivalence.functor Ω₀ CategoryTheory.NatTrans.app CategoryTheory.Functor.id CategoryTheory.Equivalence.counitInv CategoryTheory.Functor.map	—	—
ofIso_truth 📖	mathematical	Quiver.Hom CategoryTheory.CategoryStruct.toQuiver CategoryTheory.Category.toCategoryStruct CategoryTheory.CategoryStruct.comp Ω₀ CategoryTheory.Iso.inv Ω truth CategoryTheory.Iso.hom	truth ofIso	—	—
ofIso_Ω 📖	mathematical	Quiver.Hom CategoryTheory.CategoryStruct.toQuiver CategoryTheory.Category.toCategoryStruct CategoryTheory.CategoryStruct.comp Ω₀ CategoryTheory.Iso.inv Ω truth CategoryTheory.Iso.hom	Ω ofIso	—	—
ofIso_Ω₀ 📖	mathematical	Quiver.Hom CategoryTheory.CategoryStruct.toQuiver CategoryTheory.Category.toCategoryStruct CategoryTheory.CategoryStruct.comp Ω₀ CategoryTheory.Iso.inv Ω truth CategoryTheory.Iso.hom	Ω₀ ofIso	—	—
ofIso_χ 📖	mathematical	Quiver.Hom CategoryTheory.CategoryStruct.toQuiver CategoryTheory.Category.toCategoryStruct CategoryTheory.CategoryStruct.comp Ω₀ CategoryTheory.Iso.inv Ω truth CategoryTheory.Iso.hom	χ ofIso CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct Ω CategoryTheory.Iso.hom	—	—
ofIso_χ₀ 📖	mathematical	Quiver.Hom CategoryTheory.CategoryStruct.toQuiver CategoryTheory.Category.toCategoryStruct CategoryTheory.CategoryStruct.comp Ω₀ CategoryTheory.Iso.inv Ω truth CategoryTheory.Iso.hom	χ₀ ofIso	—	—
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	—	Quiver.Hom CategoryTheory.CategoryStruct.toQuiver CategoryTheory.Category.toCategoryStruct CategoryTheory.Mono χ	—	CategoryTheory.Limits.hasLimitOfHasLimitsOfShape CategoryTheory.Limits.pullback.fst_of_mono mono_truth uniq CategoryTheory.IsPullback.of_hasPullback
truth_comp_hom 📖	mathematical	—	CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct Ω₀ Ω truth hom χ₀	—	CategoryTheory.CommSq.w mono_truth CategoryTheory.IsPullback.toCommSq isPullback
truth_comp_hom_assoc 📖	mathematical	—	CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct Ω₀ Ω truth hom χ₀	—	CategoryTheory.Category.assoc Mathlib.Tactic.Reassoc.eq_whisker' truth_comp_hom
uniq 📖	mathematical	CategoryTheory.IsPullback Ω₀ Ω truth	χ	—	—
uniqueUpToIso_hom 📖	mathematical	—	CategoryTheory.Iso.hom Ω uniqueUpToIso hom	—	—
uniqueUpToIso_inv 📖	mathematical	—	CategoryTheory.Iso.inv Ω uniqueUpToIso hom	—	—
χ_comp_hom 📖	mathematical	—	CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct Ω χ hom	—	uniq CategoryTheory.IsPullback.paste_vert isPullback mono_truth
χ_comp_hom_assoc 📖	mathematical	—	CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct Ω χ hom	—	CategoryTheory.Category.assoc Mathlib.Tactic.Reassoc.eq_whisker' χ_comp_hom
χ_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.SubobjectRepresentableBy

Definitions

Name	Category	Theorems
classifier 📖	CompOp	—
isTerminalΩ₀ 📖	CompOp	—
iso 📖	CompOp	4 math math: iso_inv_left_π_assoc, iso_inv_hom_left_comp, iso_inv_left_π, iso_inv_hom_left_comp_assoc
isoΩ₀ 📖	CompOp	—
Ω₀ 📖	CompOp	7 math math: homEquiv_eq, pullback_homEquiv_symm_obj_Ω₀, iso_inv_left_π_assoc, isPullback, iso_inv_hom_left_comp, iso_inv_left_π, iso_inv_hom_left_comp_assoc
π 📖	CompOp	3 math math: iso_inv_left_π_assoc, isPullback, iso_inv_left_π
χ 📖	CompOp	6 math math: iso_inv_left_π_assoc, uniq, isPullback, iso_inv_hom_left_comp, iso_inv_left_π, iso_inv_hom_left_comp_assoc
χ₀ 📖	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_π 📖	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

---

← Back to Index