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.Comma.left CategoryTheory.Comma.right	—	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.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	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 hasColimits CategoryTheory.Limits.HasZeroObject.initialMonoClass CategoryTheory.Abelian.hasZeroObject CategoryTheory.Comma.left 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