Documentation Verification Report

Subobject

📁 Source: Mathlib/CategoryTheory/Abelian/GrothendieckCategory/Subobject.lean

Statistics

Metric	Count
Definitions `isColimitMapCoconeOfSubobjectMkEqISup`	1
Theorems `exists_isIso_of_functor_from_monoOver`, `mono_of_isColimit_monoOver`, `subobjectMk_of_isColimit_eq_iSup`	3
Total	4

CategoryTheory.IsGrothendieckAbelian

Definitions

Name	Category	Theorems
`isColimitMapCoconeOfSubobjectMkEqISup` 📖	CompOp	—

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`exists_isIso_of_functor_from_monoOver` 📖	mathematical	`HasCardinalLT` `CategoryTheory.Subobject` `CategoryTheory.CategoryStruct.comp` `CategoryTheory.Category.toCategoryStruct` `CategoryTheory.Functor.obj` `CategoryTheory.Functor.comp` `CategoryTheory.MonoOver` `CategoryTheory.ObjectProperty.FullSubcategory.category` `CategoryTheory.Over` `CategoryTheory.instCategoryOver` `CategoryTheory.Over.isMono` `CategoryTheory.MonoOver.forget` `CategoryTheory.Over.forget` `CategoryTheory.Functor` `CategoryTheory.Functor.category` `CategoryTheory.Functor.const` `CategoryTheory.Limits.Cocone.pt` `CategoryTheory.NatTrans.app` `CategoryTheory.Limits.Cocone.ι` `CategoryTheory.Comma.hom` `CategoryTheory.Discrete` `CategoryTheory.discreteCategory` `CategoryTheory.Functor.id` `CategoryTheory.Functor.fromPUnit` `CategoryTheory.ObjectProperty.FullSubcategory.obj`	`CategoryTheory.IsIso` `CategoryTheory.Functor.obj` `CategoryTheory.Functor.id` `CategoryTheory.Comma.left` `CategoryTheory.Discrete` `CategoryTheory.discreteCategory` `CategoryTheory.Functor.fromPUnit` `CategoryTheory.ObjectProperty.FullSubcategory.obj` `CategoryTheory.Over` `CategoryTheory.instCategoryOver` `CategoryTheory.Over.isMono` `CategoryTheory.MonoOver` `CategoryTheory.ObjectProperty.FullSubcategory.category` `CategoryTheory.Comma.right` `CategoryTheory.Comma.hom`	—	`CategoryTheory.isFiltered_of_isCardinalFiltered` `mono_of_isColimit_monoOver` `CategoryTheory.MonoOver.mono` `Function.Surjective.hasRightInverse` `HasCardinalLT.of_injective` `Subtype.val_injective` `CategoryTheory.Subobject.isIso_iff_mk_eq_top` `top_le_iff` `locallySmall` `wellPowered` `CategoryTheory.Limits.hasLimitsOfShapeOfHasLimits` `hasLimits` `CategoryTheory.Limits.hasImages_of_hasStrongEpiMonoFactorisations` `CategoryTheory.Abelian.instHasStrongEpiMonoFactorisations` `CategoryTheory.Limits.hasColimitsOfShapeOfHasColimitsOfSize` `hasColimits` `CategoryTheory.Limits.HasZeroObject.initialMonoClass` `CategoryTheory.Abelian.hasZeroObject` `subobjectMk_of_isColimit_eq_iSup` `CategoryTheory.Subobject.epi_iff_mk_eq_top` `CategoryTheory.balanced_of_strongMonoCategory` `CategoryTheory.strongMonoCategory_of_regularMonoCategory` `CategoryTheory.regularMonoCategoryOfNormalMonoCategory` `CategoryTheory.Abelian.toIsNormalMonoCategory` `iSup_le_iff` `Eq.le` `CategoryTheory.MonoOver.subobjectMk_le_mk_of_hom`
`mono_of_isColimit_monoOver` 📖	mathematical	`CategoryTheory.CategoryStruct.comp` `CategoryTheory.Category.toCategoryStruct` `CategoryTheory.Functor.obj` `CategoryTheory.Functor.comp` `CategoryTheory.MonoOver` `CategoryTheory.ObjectProperty.FullSubcategory.category` `CategoryTheory.Over` `CategoryTheory.instCategoryOver` `CategoryTheory.Over.isMono` `CategoryTheory.MonoOver.forget` `CategoryTheory.Over.forget` `CategoryTheory.Functor` `CategoryTheory.Functor.category` `CategoryTheory.Functor.const` `CategoryTheory.Limits.Cocone.pt` `CategoryTheory.NatTrans.app` `CategoryTheory.Limits.Cocone.ι` `CategoryTheory.Comma.hom` `CategoryTheory.Discrete` `CategoryTheory.discreteCategory` `CategoryTheory.Functor.id` `CategoryTheory.Functor.fromPUnit` `CategoryTheory.ObjectProperty.FullSubcategory.obj`	`CategoryTheory.Mono` `CategoryTheory.Limits.Cocone.pt` `CategoryTheory.Functor.comp` `CategoryTheory.MonoOver` `CategoryTheory.ObjectProperty.FullSubcategory.category` `CategoryTheory.Over` `CategoryTheory.instCategoryOver` `CategoryTheory.Over.isMono` `CategoryTheory.MonoOver.forget` `CategoryTheory.Over.forget`	—	`CategoryTheory.Over.w` `CategoryTheory.Category.comp_id` `CategoryTheory.NatTrans.mono_of_mono_app` `CategoryTheory.MonoOver.mono` `CategoryTheory.Limits.colim.map_mono'` `CategoryTheory.Limits.hasColimitsOfShape_of_has_filtered_colimits` `hasFilteredColimitsOfSize` `CategoryTheory.Functor.instPreservesMonomorphisms` `CategoryTheory.Limits.HasZeroObject.instFunctor` `CategoryTheory.Abelian.hasZeroObject` `CategoryTheory.Functor.preservesZeroMorphisms_of_preserves_terminal_object` `CategoryTheory.Limits.PreservesLimitsOfShape.preservesLimit` `CategoryTheory.Limits.PreservesFiniteLimits.preservesFiniteLimits` `CategoryTheory.HasExactColimitsOfShape.preservesFiniteLimits` `CategoryTheory.AB5OfSize.ofShape` `ab5OfSize` `CategoryTheory.Functor.preservesHomologyOfExact` `CategoryTheory.Limits.PreservesColimits.preservesFiniteColimits` `CategoryTheory.Adjunction.colim_preservesColimits` `CategoryTheory.IsFiltered.isConnected`
`subobjectMk_of_isColimit_eq_iSup` 📖	mathematical	`CategoryTheory.CategoryStruct.comp` `CategoryTheory.Category.toCategoryStruct` `CategoryTheory.Functor.obj` `CategoryTheory.Functor.comp` `CategoryTheory.MonoOver` `CategoryTheory.ObjectProperty.FullSubcategory.category` `CategoryTheory.Over` `CategoryTheory.instCategoryOver` `CategoryTheory.Over.isMono` `CategoryTheory.MonoOver.forget` `CategoryTheory.Over.forget` `CategoryTheory.Functor` `CategoryTheory.Functor.category` `CategoryTheory.Functor.const` `CategoryTheory.Limits.Cocone.pt` `CategoryTheory.NatTrans.app` `CategoryTheory.Limits.Cocone.ι` `CategoryTheory.Comma.hom` `CategoryTheory.Discrete` `CategoryTheory.discreteCategory` `CategoryTheory.Functor.id` `CategoryTheory.Functor.fromPUnit` `CategoryTheory.ObjectProperty.FullSubcategory.obj`	`CategoryTheory.Limits.Cocone.pt` `CategoryTheory.Functor.comp` `CategoryTheory.MonoOver` `CategoryTheory.ObjectProperty.FullSubcategory.category` `CategoryTheory.Over` `CategoryTheory.instCategoryOver` `CategoryTheory.Over.isMono` `CategoryTheory.MonoOver.forget` `CategoryTheory.Over.forget` `mono_of_isColimit_monoOver` `iSup` `CategoryTheory.Subobject` `ConditionallyCompletePartialOrderSup.toSupSet` `ConditionallyCompletePartialOrder.toConditionallyCompletePartialOrderSup` `ConditionallyCompleteLattice.toConditionallyCompletePartialOrder` `CompleteLattice.toConditionallyCompleteLattice` `CategoryTheory.Subobject.instCompleteLattice` `locallySmall` `wellPowered` `CategoryTheory.Limits.hasLimitsOfShapeOfHasLimits` `CategoryTheory.Limits.WidePullbackShape` `CategoryTheory.Limits.WidePullbackShape.category` `hasLimits` `CategoryTheory.Limits.hasImages_of_hasStrongEpiMonoFactorisations` `CategoryTheory.Abelian.instHasStrongEpiMonoFactorisations` `CategoryTheory.Limits.hasColimitsOfShapeOfHasColimitsOfSize` `CategoryTheory.Discrete` `CategoryTheory.discreteCategory` `hasColimits` `CategoryTheory.Limits.HasZeroObject.initialMonoClass` `CategoryTheory.Abelian.hasZeroObject` `CategoryTheory.Functor.obj` `CategoryTheory.Functor.id` `CategoryTheory.Comma.left` `CategoryTheory.Functor.fromPUnit` `CategoryTheory.ObjectProperty.FullSubcategory.obj` `CategoryTheory.Comma.hom` `CategoryTheory.MonoOver.mono`	—	`le_antisymm` `mono_of_isColimit_monoOver` `locallySmall` `wellPowered` `CategoryTheory.Limits.hasLimitsOfShapeOfHasLimits` `hasLimits` `CategoryTheory.Limits.hasImages_of_hasStrongEpiMonoFactorisations` `CategoryTheory.Abelian.instHasStrongEpiMonoFactorisations` `CategoryTheory.Limits.hasColimitsOfShapeOfHasColimitsOfSize` `hasColimits` `CategoryTheory.Limits.HasZeroObject.initialMonoClass` `CategoryTheory.Abelian.hasZeroObject` `CategoryTheory.MonoOver.mono` `le_iSup_iff` `CategoryTheory.Subobject.ind` `CategoryTheory.Category.comp_id` `CategoryTheory.cancel_mono` `CategoryTheory.Category.assoc` `CategoryTheory.Subobject.ofMkLEMk_comp` `CategoryTheory.MonoOver.w` `CategoryTheory.Subobject.mk_le_mk_of_comm` `CategoryTheory.Limits.IsColimit.hom_ext` `CategoryTheory.Limits.IsColimit.fac_assoc` `iSup_le_iff`

---

← Back to Index