MonoOver

📁 Source: Mathlib/CategoryTheory/Subobject/MonoOver.lean

Statistics

Metric	Count
Definitions MonoOver, arrow, coconeOfHasStrongEpiMonoFactorisation, exists, existsIsoMap, existsPullbackAdj, forget, forgetImage, fullyFaithfulForget, homMk, image, imageForgetAdj, imageMonoOver, instCoeOut, isColimitCoconeOfHasStrongEpiMonoFactorisation, isoMk, liftComp, liftId, liftIso, liftStructOfHasStrongEpiMonoFactorisation, map, mapComp, mapId, mapIso, mapPullbackAdj, mk, mk', mk'ArrowIso, mkArrowIso, pullback, pullbackComp, pullbackId, pullbackMapSelf, pullbackObjIsoOfIsPullback, reflective, slice, strongEpiMonoFactorisationSigmaDesc, isMono	38
Theorems commSqOfHasStrongEpiMonoFactorisation, congr_counitIso, congr_functor, congr_inverse, congr_unitIso, faithful_exists, faithful_map, forget_obj_hom, forget_obj_left, full_map, hasColimitsOfSize_of_hasStrongEpiMonoFactorisations, hasFiniteLimits, hasLimit, hasLimitsOfShape, hasLimitsOfSize, imageMonoOver_arrow, image_map, image_obj, instIsClosedUnderLimitsOfShapeOverIsMono, instIsIsoLeftDiscretePUnitHomFullSubcategoryOverIsMono, instIsRightAdjointOverForget, instMonoHomDiscretePUnitObjOverForget, isIso_iff_isIso_hom_left, isIso_iff_isIso_left, isThin, isoMk_hom, isoMk_inv, lift_comm, lift_map_hom, lift_obj_arrow, lift_obj_obj, mapIso_counitIso, mapIso_functor, mapIso_inverse, mapIso_unitIso, map_obj_arrow, map_obj_left, mk'_arrow, mk'_coe', mkArrowIso_hom_hom_left, mkArrowIso_inv_hom_left, mk_arrow, mk_coe, mk_obj, mono, mono_obj_hom, pullback_obj_arrow, pullback_obj_left, w, w_assoc	50
Total	88

CategoryTheory

Definitions

Name	Category	Theorems
MonoOver 📖	CompOp	90 math math: Subobject.factors_iff, MonoOver.congr_unitIso, IsGrothendieckAbelian.IsPresentable.injectivity₀.F_obj, MonoOver.mapIso_functor, MonoOver.hasColimitsOfSize_of_hasStrongEpiMonoFactorisations, MonoOver.instIsRightAdjointOverForget, MonoOver.isIso_iff_subobjectMk_eq, Classifier.SubobjectRepresentableBy.iso_inv_hom_left_comp, MonoOver.isoMk_inv, MonoOver.mapIso_unitIso, IsGrothendieckAbelian.IsPresentable.surjectivity.F_map, MonoOver.mapIso_counitIso, Types.monoOverEquivalenceSet_inverse_map, MonoOver.mkArrowIso_hom_hom_left, MonoOver.map_obj_left, essentiallySmall_monoOver, MonoOver.pullback_obj_arrow, Subfunctor.equivalenceMonoOver_inverse_map, MonoOver.image_map, Subfunctor.equivalenceMonoOver_functor_map, Subobject.inf_eq_map_pullback', monoOver_terminal_to_subterminals_comp, MonoOver.image_obj, Subfunctor.equivalenceMonoOver_inverse_obj, MonoOver.bot_left, MonoOver.bot_arrow, MonoOver.map_obj_arrow, subterminalsEquivMonoOverTerminal_inverse_map, Subobject.lower_comm, MonoOver.bot_arrow_eq_zero, MonoOver.hasFiniteLimits, Subfunctor.equivalenceMonoOver_functor_obj, IsGrothendieckAbelian.IsPresentable.injectivity₀.F_map, isEventuallyConstant_of_isArtinianObject, MonoOver.forget_obj_left, Subobject.instIsEquivalenceMonoOverRepresentative, Types.monoOverEquivalenceSet_functor_map, subterminalsEquivMonoOverTerminal_inverse_obj_obj, Types.monoOverEquivalenceSet_functor_obj, MonoOver.hasLimitsOfShape, MonoOver.congr_functor, MonoOver.isIso_iff_isIso_hom_left, MonoOver.congr_inverse, MonoOver.isoMk_hom, Classifier.SubobjectRepresentableBy.iso_inv_left_π_assoc, Subobject.lowerEquivalence_counitIso, subterminalsEquivMonoOverTerminal_functor_map, MonoOver.top_arrow, IsGrothendieckAbelian.generatingMonomorphisms.functorToMonoOver_map, MonoOver.inf_map_app, MonoOver.isThin, MonoOver.mkArrowIso_inv_hom_left, Classifier.SubobjectRepresentableBy.iso_inv_hom_left_comp_assoc, MonoOver.pullback_obj_left, Subobject.lowerEquivalence_unitIso, Subfunctor.equivalenceMonoOver_unitIso, subterminalsEquivMonoOverTerminal_unitIso, MonoOver.forget_obj_hom, Classifier.SubobjectRepresentableBy.iso_inv_left_comp, MonoOver.commSqOfHasStrongEpiMonoFactorisation, subterminalsEquivMonoOverTerminal_counitIso, Classifier.SubobjectRepresentableBy.iso_inv_left_π, Types.monoOverEquivalenceSet_inverse_obj, MonoOver.hasLimit, MonoOver.instMonoHomDiscretePUnitObjOverForget, IsGrothendieckAbelian.IsPresentable.surjectivity.F_obj, MonoOver.inf_obj, MonoOver.top_left, Types.monoOverEquivalenceSet_unitIso, IsGrothendieckAbelian.generatingMonomorphisms.functorToMonoOver_obj, Subobject.representative_coe, MonoOver.full_map, Subobject.inf_eq_map_pullback, MonoOver.mapIso_inverse, MonoOver.congr_counitIso, Subobject.lowerEquivalence_inverse, Subobject.lowerEquivalence_functor, isEventuallyConstant_of_isNoetherianObject, MonoOver.faithful_exists, isNoetherianObject_iff_isEventuallyConstant, Types.monoOverEquivalenceSet_counitIso, subterminalsEquivMonoOverTerminal_functor_obj_obj, isArtinianObject_iff_isEventuallyConstant, MonoOver.faithful_map, MonoOver.hasLimitsOfSize, subterminals_to_monoOver_terminal_comp_forget, Subobject.representative_arrow, Subfunctor.equivalenceMonoOver_counitIso, MonoOver.isIso_iff_isIso_left, essentiallySmall_monoOver_iff_small_subobject

CategoryTheory.MonoOver

Definitions

Name	Category	Theorems
arrow 📖	CompOp	26 math math: mk_arrow, mkArrowIso_hom_hom_left, pullback_obj_arrow, CategoryTheory.Subfunctor.equivalenceMonoOver_inverse_map, CategoryTheory.Subobject.inf_eq_map_pullback', lift_obj_arrow, CategoryTheory.Subfunctor.equivalenceMonoOver_inverse_obj, bot_arrow, map_obj_arrow, w, bot_arrow_eq_zero, imageMonoOver_arrow, mono, top_arrow, inf_map_app, mkArrowIso_inv_hom_left, mk'_arrow, w_assoc, pullback_obj_left, CategoryTheory.Subfunctor.equivalenceMonoOver_unitIso, forget_obj_hom, commSqOfHasStrongEpiMonoFactorisation, inf_obj, CategoryTheory.Subobject.inf_eq_map_pullback, CategoryTheory.Subobject.representative_arrow, CategoryTheory.Subfunctor.equivalenceMonoOver_counitIso
coconeOfHasStrongEpiMonoFactorisation 📖	CompOp	—
exists 📖	CompOp	1 math math: faithful_exists
existsIsoMap 📖	CompOp	—
existsPullbackAdj 📖	CompOp	—
forget 📖	CompOp	9 math math: instIsRightAdjointOverForget, pullback_obj_arrow, image_map, CategoryTheory.monoOver_terminal_to_subterminals_comp, forget_obj_left, inf_map_app, forget_obj_hom, instMonoHomDiscretePUnitObjOverForget, CategoryTheory.subterminals_to_monoOver_terminal_comp_forget
forgetImage 📖	CompOp	—
fullyFaithfulForget 📖	CompOp	—
homMk 📖	CompOp	15 math math: isoMk_inv, CategoryTheory.IsGrothendieckAbelian.IsPresentable.surjectivity.F_map, Types.monoOverEquivalenceSet_inverse_map, CategoryTheory.Subfunctor.equivalenceMonoOver_functor_map, CategoryTheory.IsGrothendieckAbelian.IsPresentable.injectivity₀.F_map, isoMk_hom, CategoryTheory.subterminalsEquivMonoOverTerminal_functor_map, CategoryTheory.IsGrothendieckAbelian.generatingMonomorphisms.functorToMonoOver_map, inf_map_app, CategoryTheory.Subfunctor.equivalenceMonoOver_unitIso, CategoryTheory.subterminalsEquivMonoOverTerminal_unitIso, CategoryTheory.subterminalsEquivMonoOverTerminal_counitIso, Types.monoOverEquivalenceSet_unitIso, Types.monoOverEquivalenceSet_counitIso, CategoryTheory.Subfunctor.equivalenceMonoOver_counitIso
image 📖	CompOp	2 math math: image_map, image_obj
imageForgetAdj 📖	CompOp	—
imageMonoOver 📖	CompOp	3 math math: image_map, image_obj, imageMonoOver_arrow
instCoeOut 📖	CompOp	—
isColimitCoconeOfHasStrongEpiMonoFactorisation 📖	CompOp	—
isoMk 📖	CompOp	7 math math: congr_unitIso, isoMk_inv, isoMk_hom, CategoryTheory.subterminalsEquivMonoOverTerminal_counitIso, Types.monoOverEquivalenceSet_unitIso, congr_counitIso, CategoryTheory.Subfunctor.equivalenceMonoOver_counitIso
liftComp 📖	CompOp	—
liftId 📖	CompOp	—
liftIso 📖	CompOp	—
liftStructOfHasStrongEpiMonoFactorisation 📖	CompOp	—
map 📖	CompOp	10 math math: mapIso_functor, mapIso_unitIso, mapIso_counitIso, map_obj_left, map_obj_arrow, inf_map_app, inf_obj, full_map, mapIso_inverse, faithful_map
mapComp 📖	CompOp	2 math math: mapIso_unitIso, mapIso_counitIso
mapId 📖	CompOp	2 math math: mapIso_unitIso, mapIso_counitIso
mapIso 📖	CompOp	7 math math: congr_unitIso, mapIso_functor, mapIso_unitIso, mapIso_counitIso, congr_inverse, mapIso_inverse, congr_counitIso
mapPullbackAdj 📖	CompOp	—
mk 📖	CompOp	—
mk' 📖	CompOp	—
mk'ArrowIso 📖	CompOp	—
mkArrowIso 📖	CompOp	2 math math: mkArrowIso_hom_hom_left, mkArrowIso_inv_hom_left
pullback 📖	CompOp	4 math math: pullback_obj_arrow, inf_map_app, pullback_obj_left, inf_obj
pullbackComp 📖	CompOp	—
pullbackId 📖	CompOp	—
pullbackMapSelf 📖	CompOp	—
pullbackObjIsoOfIsPullback 📖	CompOp	—
reflective 📖	CompOp	—
slice 📖	CompOp	—
strongEpiMonoFactorisationSigmaDesc 📖	CompOp	1 math math: commSqOfHasStrongEpiMonoFactorisation

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
commSqOfHasStrongEpiMonoFactorisation 📖	mathematical	CategoryTheory.Limits.HasCoproducts	CategoryTheory.CommSq CategoryTheory.Limits.sigmaObj 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.MonoOver CategoryTheory.ObjectProperty.FullSubcategory.category CategoryTheory.Limits.hasColimitOfHasColimitsOfShape CategoryTheory.Discrete.functor CategoryTheory.Limits.Cocone.pt CategoryTheory.Limits.MonoFactorisation.I CategoryTheory.Limits.Sigma.desc arrow CategoryTheory.Limits.StrongEpiMonoFactorisation.toMonoFactorisation strongEpiMonoFactorisationSigmaDesc CategoryTheory.CommaMorphism.left CategoryTheory.Functor CategoryTheory.Functor.category CategoryTheory.Functor.const CategoryTheory.InducedCategory.Hom.hom CategoryTheory.ObjectProperty.FullSubcategory CategoryTheory.NatTrans.app CategoryTheory.Limits.Cocone.ι CategoryTheory.Limits.MonoFactorisation.e CategoryTheory.Limits.MonoFactorisation.m	—	CategoryTheory.Limits.hasColimitOfHasColimitsOfShape CategoryTheory.Limits.MonoFactorisation.fac CategoryTheory.Limits.Sigma.hom_ext CategoryTheory.Limits.colimit.ι_desc_assoc CategoryTheory.Over.w CategoryTheory.Limits.colimit.ι_desc
congr_counitIso 📖	mathematical	—	CategoryTheory.Equivalence.counitIso CategoryTheory.MonoOver CategoryTheory.Functor.obj CategoryTheory.Equivalence.functor CategoryTheory.ObjectProperty.FullSubcategory.category CategoryTheory.Over CategoryTheory.instCategoryOver CategoryTheory.Over.isMono congr CategoryTheory.NatIso.ofComponents CategoryTheory.Functor.comp CategoryTheory.Equivalence.inverse lift CategoryTheory.Over.post CategoryTheory.Functor.id mapIso CategoryTheory.Iso.app CategoryTheory.Iso.symm CategoryTheory.Functor CategoryTheory.Functor.category CategoryTheory.Equivalence.unitIso isoMk CategoryTheory.Comma.left CategoryTheory.Discrete CategoryTheory.discreteCategory CategoryTheory.Functor.fromPUnit CategoryTheory.ObjectProperty.FullSubcategory.obj	—	—
congr_functor 📖	mathematical	—	CategoryTheory.Equivalence.functor CategoryTheory.MonoOver CategoryTheory.Functor.obj CategoryTheory.ObjectProperty.FullSubcategory.category CategoryTheory.Over CategoryTheory.instCategoryOver CategoryTheory.Over.isMono congr lift CategoryTheory.Over.post	—	—
congr_inverse 📖	mathematical	—	CategoryTheory.Equivalence.inverse CategoryTheory.MonoOver CategoryTheory.Functor.obj CategoryTheory.Equivalence.functor CategoryTheory.ObjectProperty.FullSubcategory.category CategoryTheory.Over CategoryTheory.instCategoryOver CategoryTheory.Over.isMono congr CategoryTheory.Functor.comp lift CategoryTheory.Over.post CategoryTheory.Functor.id mapIso CategoryTheory.Iso.app CategoryTheory.Iso.symm CategoryTheory.Functor CategoryTheory.Functor.category CategoryTheory.Equivalence.unitIso	—	—
congr_unitIso 📖	mathematical	—	CategoryTheory.Equivalence.unitIso CategoryTheory.MonoOver CategoryTheory.Functor.obj CategoryTheory.Equivalence.functor CategoryTheory.ObjectProperty.FullSubcategory.category CategoryTheory.Over CategoryTheory.instCategoryOver CategoryTheory.Over.isMono congr CategoryTheory.NatIso.ofComponents CategoryTheory.Functor.id CategoryTheory.Functor.comp lift CategoryTheory.Over.post CategoryTheory.Equivalence.inverse mapIso CategoryTheory.Iso.app CategoryTheory.Iso.symm CategoryTheory.Functor CategoryTheory.Functor.category isoMk CategoryTheory.Comma.left CategoryTheory.Discrete CategoryTheory.discreteCategory CategoryTheory.Functor.fromPUnit CategoryTheory.ObjectProperty.FullSubcategory.obj	—	—
faithful_exists 📖	mathematical	—	CategoryTheory.Functor.Faithful CategoryTheory.MonoOver CategoryTheory.ObjectProperty.FullSubcategory.category CategoryTheory.Over CategoryTheory.instCategoryOver CategoryTheory.Over.isMono exists	—	isThin
faithful_map 📖	mathematical	—	CategoryTheory.Functor.Faithful CategoryTheory.MonoOver CategoryTheory.ObjectProperty.FullSubcategory.category CategoryTheory.Over CategoryTheory.instCategoryOver CategoryTheory.Over.isMono map	—	isThin
forget_obj_hom 📖	mathematical	—	CategoryTheory.Comma.hom CategoryTheory.Discrete CategoryTheory.discreteCategory CategoryTheory.Functor.id CategoryTheory.Functor.fromPUnit CategoryTheory.Functor.obj CategoryTheory.MonoOver CategoryTheory.ObjectProperty.FullSubcategory.category CategoryTheory.Over CategoryTheory.instCategoryOver CategoryTheory.Over.isMono forget arrow	—	—
forget_obj_left 📖	mathematical	—	CategoryTheory.Comma.left CategoryTheory.Discrete CategoryTheory.discreteCategory CategoryTheory.Functor.id CategoryTheory.Functor.fromPUnit CategoryTheory.Functor.obj CategoryTheory.MonoOver CategoryTheory.ObjectProperty.FullSubcategory.category CategoryTheory.Over CategoryTheory.instCategoryOver CategoryTheory.Over.isMono forget CategoryTheory.ObjectProperty.FullSubcategory.obj	—	—
full_map 📖	mathematical	—	CategoryTheory.Functor.Full CategoryTheory.MonoOver CategoryTheory.ObjectProperty.FullSubcategory.category CategoryTheory.Over CategoryTheory.instCategoryOver CategoryTheory.Over.isMono map	—	CategoryTheory.cancel_mono CategoryTheory.Category.assoc w
hasColimitsOfSize_of_hasStrongEpiMonoFactorisations 📖	mathematical	CategoryTheory.Limits.HasCoproducts	CategoryTheory.Limits.HasColimitsOfSize CategoryTheory.MonoOver CategoryTheory.ObjectProperty.FullSubcategory.category CategoryTheory.Over CategoryTheory.instCategoryOver CategoryTheory.Over.isMono	—	—
hasFiniteLimits 📖	mathematical	—	CategoryTheory.Limits.HasFiniteLimits CategoryTheory.MonoOver CategoryTheory.ObjectProperty.FullSubcategory.category CategoryTheory.Over CategoryTheory.instCategoryOver CategoryTheory.Over.isMono	—	hasLimitsOfShape CategoryTheory.Limits.hasLimitsOfShape_of_hasFiniteLimits
hasLimit 📖	mathematical	—	CategoryTheory.Limits.HasLimit CategoryTheory.MonoOver CategoryTheory.ObjectProperty.FullSubcategory.category CategoryTheory.Over CategoryTheory.instCategoryOver CategoryTheory.Over.isMono	—	CategoryTheory.Limits.hasLimit_of_closedUnderLimits instIsClosedUnderLimitsOfShapeOverIsMono
hasLimitsOfShape 📖	mathematical	—	CategoryTheory.Limits.HasLimitsOfShape CategoryTheory.MonoOver CategoryTheory.ObjectProperty.FullSubcategory.category CategoryTheory.Over CategoryTheory.instCategoryOver CategoryTheory.Over.isMono	—	hasLimit CategoryTheory.Limits.hasLimitOfHasLimitsOfShape
hasLimitsOfSize 📖	mathematical	—	CategoryTheory.Limits.HasLimitsOfSize CategoryTheory.MonoOver CategoryTheory.ObjectProperty.FullSubcategory.category CategoryTheory.Over CategoryTheory.instCategoryOver CategoryTheory.Over.isMono	—	hasLimitsOfShape CategoryTheory.Limits.hasLimitsOfShapeOfHasLimits
imageMonoOver_arrow 📖	mathematical	—	arrow imageMonoOver CategoryTheory.Limits.image.ι	—	—
image_map 📖	mathematical	—	CategoryTheory.Functor.map CategoryTheory.Over CategoryTheory.instCategoryOver CategoryTheory.MonoOver CategoryTheory.ObjectProperty.FullSubcategory.category CategoryTheory.Over.isMono image CategoryTheory.Functor.preimage imageMonoOver CategoryTheory.Functor.obj CategoryTheory.Functor.id CategoryTheory.Comma.left CategoryTheory.Discrete CategoryTheory.discreteCategory CategoryTheory.Functor.fromPUnit CategoryTheory.Comma.hom forget CategoryTheory.Over.homMk CategoryTheory.Limits.image.lift CategoryTheory.Comma.right CategoryTheory.Limits.image CategoryTheory.Limits.image.ι CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct CategoryTheory.CommaMorphism.left CategoryTheory.Limits.factorThruImage	—	—
image_obj 📖	mathematical	—	CategoryTheory.Functor.obj CategoryTheory.Over CategoryTheory.instCategoryOver CategoryTheory.MonoOver CategoryTheory.ObjectProperty.FullSubcategory.category CategoryTheory.Over.isMono image imageMonoOver CategoryTheory.Functor.id CategoryTheory.Comma.left CategoryTheory.Discrete CategoryTheory.discreteCategory CategoryTheory.Functor.fromPUnit CategoryTheory.Comma.hom	—	—
instIsClosedUnderLimitsOfShapeOverIsMono 📖	mathematical	—	CategoryTheory.ObjectProperty.IsClosedUnderLimitsOfShape CategoryTheory.Over CategoryTheory.instCategoryOver CategoryTheory.Over.isMono	—	CategoryTheory.Limits.IsLimit.hom_ext CategoryTheory.cancel_mono CategoryTheory.Category.assoc CategoryTheory.Over.w
instIsIsoLeftDiscretePUnitHomFullSubcategoryOverIsMono 📖	mathematical	—	CategoryTheory.IsIso 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.CommaMorphism.left CategoryTheory.InducedCategory.Hom.hom CategoryTheory.ObjectProperty.FullSubcategory	—	CategoryTheory.Functor.map_isIso
instIsRightAdjointOverForget 📖	mathematical	—	CategoryTheory.Functor.IsRightAdjoint CategoryTheory.Over CategoryTheory.instCategoryOver CategoryTheory.MonoOver CategoryTheory.ObjectProperty.FullSubcategory.category CategoryTheory.Over.isMono forget	—	—
instMonoHomDiscretePUnitObjOverForget 📖	mathematical	—	CategoryTheory.Mono CategoryTheory.Functor.obj CategoryTheory.Functor.id CategoryTheory.Comma.left CategoryTheory.Discrete CategoryTheory.discreteCategory CategoryTheory.Functor.fromPUnit CategoryTheory.MonoOver CategoryTheory.ObjectProperty.FullSubcategory.category CategoryTheory.Over CategoryTheory.instCategoryOver CategoryTheory.Over.isMono forget CategoryTheory.Comma.right CategoryTheory.Comma.hom	—	mono
isIso_iff_isIso_hom_left 📖	mathematical	—	CategoryTheory.IsIso CategoryTheory.MonoOver CategoryTheory.ObjectProperty.FullSubcategory.category CategoryTheory.Over CategoryTheory.instCategoryOver CategoryTheory.Over.isMono CategoryTheory.Comma.left CategoryTheory.Discrete CategoryTheory.discreteCategory CategoryTheory.Functor.id CategoryTheory.Functor.fromPUnit CategoryTheory.ObjectProperty.FullSubcategory.obj CategoryTheory.CommaMorphism.left CategoryTheory.InducedCategory.Hom.hom CategoryTheory.ObjectProperty.FullSubcategory	—	CategoryTheory.isIso_iff_of_reflects_iso CategoryTheory.reflectsIsomorphisms_comp CategoryTheory.reflectsIsomorphisms_of_full_and_faithful CategoryTheory.ObjectProperty.full_ι CategoryTheory.ObjectProperty.faithful_ι CategoryTheory.Over.forget_reflects_iso
isIso_iff_isIso_left 📖	mathematical	—	CategoryTheory.IsIso CategoryTheory.MonoOver CategoryTheory.ObjectProperty.FullSubcategory.category CategoryTheory.Over CategoryTheory.instCategoryOver CategoryTheory.Over.isMono CategoryTheory.Comma.left CategoryTheory.Discrete CategoryTheory.discreteCategory CategoryTheory.Functor.id CategoryTheory.Functor.fromPUnit CategoryTheory.ObjectProperty.FullSubcategory.obj CategoryTheory.CommaMorphism.left CategoryTheory.InducedCategory.Hom.hom CategoryTheory.ObjectProperty.FullSubcategory	—	isIso_iff_isIso_hom_left
isThin 📖	mathematical	—	Quiver.IsThin CategoryTheory.MonoOver CategoryTheory.CategoryStruct.toQuiver CategoryTheory.Category.toCategoryStruct CategoryTheory.ObjectProperty.FullSubcategory.category CategoryTheory.Over CategoryTheory.instCategoryOver CategoryTheory.Over.isMono	—	CategoryTheory.InducedCategory.hom_ext CategoryTheory.Over.OverMorphism.ext CategoryTheory.cancel_mono mono CategoryTheory.Over.w
isoMk_hom 📖	mathematical	Quiver.Hom CategoryTheory.CategoryStruct.toQuiver 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.CategoryStruct.comp CategoryTheory.Iso.hom arrow	CategoryTheory.MonoOver CategoryTheory.ObjectProperty.FullSubcategory.category isoMk homMk	—	—
isoMk_inv 📖	mathematical	Quiver.Hom CategoryTheory.CategoryStruct.toQuiver 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.CategoryStruct.comp CategoryTheory.Iso.hom arrow	CategoryTheory.Iso.inv CategoryTheory.MonoOver CategoryTheory.ObjectProperty.FullSubcategory.category isoMk homMk	—	—
lift_comm 📖	mathematical	CategoryTheory.Mono CategoryTheory.Functor.obj CategoryTheory.Functor.id CategoryTheory.Comma.left CategoryTheory.Discrete CategoryTheory.discreteCategory CategoryTheory.Functor.fromPUnit CategoryTheory.Over CategoryTheory.instCategoryOver CategoryTheory.MonoOver CategoryTheory.ObjectProperty.FullSubcategory.category CategoryTheory.Over.isMono forget CategoryTheory.Comma.right CategoryTheory.Comma.hom	CategoryTheory.Functor.comp lift	—	—
lift_map_hom 📖	mathematical	CategoryTheory.Mono CategoryTheory.Functor.obj CategoryTheory.Functor.id CategoryTheory.Comma.left CategoryTheory.Discrete CategoryTheory.discreteCategory CategoryTheory.Functor.fromPUnit CategoryTheory.Over CategoryTheory.instCategoryOver CategoryTheory.MonoOver CategoryTheory.ObjectProperty.FullSubcategory.category CategoryTheory.Over.isMono forget CategoryTheory.Comma.right CategoryTheory.Comma.hom	CategoryTheory.InducedCategory.Hom.hom CategoryTheory.ObjectProperty.FullSubcategory CategoryTheory.ObjectProperty.FullSubcategory.obj CategoryTheory.Functor.comp CategoryTheory.Functor.map lift	—	—
lift_obj_arrow 📖	mathematical	CategoryTheory.Mono CategoryTheory.Functor.obj CategoryTheory.Functor.id CategoryTheory.Comma.left CategoryTheory.Discrete CategoryTheory.discreteCategory CategoryTheory.Functor.fromPUnit CategoryTheory.Over CategoryTheory.instCategoryOver CategoryTheory.MonoOver CategoryTheory.ObjectProperty.FullSubcategory.category CategoryTheory.Over.isMono forget CategoryTheory.Comma.right CategoryTheory.Comma.hom	arrow lift	—	—
lift_obj_obj 📖	mathematical	CategoryTheory.Mono CategoryTheory.Functor.obj CategoryTheory.Functor.id CategoryTheory.Comma.left CategoryTheory.Discrete CategoryTheory.discreteCategory CategoryTheory.Functor.fromPUnit CategoryTheory.Over CategoryTheory.instCategoryOver CategoryTheory.MonoOver CategoryTheory.ObjectProperty.FullSubcategory.category CategoryTheory.Over.isMono forget CategoryTheory.Comma.right CategoryTheory.Comma.hom	CategoryTheory.ObjectProperty.FullSubcategory.obj lift	—	—
mapIso_counitIso 📖	mathematical	—	CategoryTheory.Equivalence.counitIso CategoryTheory.MonoOver CategoryTheory.ObjectProperty.FullSubcategory.category CategoryTheory.Over CategoryTheory.instCategoryOver CategoryTheory.Over.isMono mapIso CategoryTheory.Iso.trans CategoryTheory.Functor CategoryTheory.Functor.category CategoryTheory.Functor.comp map CategoryTheory.Iso.inv CategoryTheory.Iso.hom CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct CategoryTheory.Functor.id CategoryTheory.Iso.symm mapComp CategoryTheory.CategoryStruct.id CategoryTheory.instMonoId CategoryTheory.eqToIso mapId	—	—
mapIso_functor 📖	mathematical	—	CategoryTheory.Equivalence.functor CategoryTheory.MonoOver CategoryTheory.ObjectProperty.FullSubcategory.category CategoryTheory.Over CategoryTheory.instCategoryOver CategoryTheory.Over.isMono mapIso map CategoryTheory.Iso.hom	—	—
mapIso_inverse 📖	mathematical	—	CategoryTheory.Equivalence.inverse CategoryTheory.MonoOver CategoryTheory.ObjectProperty.FullSubcategory.category CategoryTheory.Over CategoryTheory.instCategoryOver CategoryTheory.Over.isMono mapIso map CategoryTheory.Iso.inv	—	—
mapIso_unitIso 📖	mathematical	—	CategoryTheory.Equivalence.unitIso CategoryTheory.MonoOver CategoryTheory.ObjectProperty.FullSubcategory.category CategoryTheory.Over CategoryTheory.instCategoryOver CategoryTheory.Over.isMono mapIso CategoryTheory.Iso.symm CategoryTheory.Functor CategoryTheory.Functor.category CategoryTheory.Functor.comp map CategoryTheory.Iso.hom CategoryTheory.Iso.inv CategoryTheory.Functor.id CategoryTheory.Iso.trans CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct mapComp CategoryTheory.CategoryStruct.id CategoryTheory.instMonoId CategoryTheory.eqToIso mapId	—	—
map_obj_arrow 📖	mathematical	—	arrow CategoryTheory.Functor.obj CategoryTheory.MonoOver CategoryTheory.ObjectProperty.FullSubcategory.category CategoryTheory.Over CategoryTheory.instCategoryOver CategoryTheory.Over.isMono map CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct CategoryTheory.Comma.left CategoryTheory.Discrete CategoryTheory.discreteCategory CategoryTheory.Functor.id CategoryTheory.Functor.fromPUnit CategoryTheory.ObjectProperty.FullSubcategory.obj	—	—
map_obj_left 📖	mathematical	—	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.MonoOver CategoryTheory.ObjectProperty.FullSubcategory.category map	—	—
mk'_arrow 📖	mathematical	—	arrow	—	mk_arrow
mk'_coe' 📖	mathematical	—	CategoryTheory.Comma.left CategoryTheory.Discrete CategoryTheory.discreteCategory CategoryTheory.Functor.id CategoryTheory.Functor.fromPUnit CategoryTheory.ObjectProperty.FullSubcategory.obj CategoryTheory.Over CategoryTheory.instCategoryOver CategoryTheory.Over.isMono	—	mk_coe
mkArrowIso_hom_hom_left 📖	mathematical	—	CategoryTheory.CommaMorphism.left CategoryTheory.Discrete CategoryTheory.discreteCategory CategoryTheory.Functor.id CategoryTheory.Functor.fromPUnit CategoryTheory.ObjectProperty.FullSubcategory.obj CategoryTheory.Over CategoryTheory.instCategoryOver CategoryTheory.Over.isMono CategoryTheory.Comma.left arrow mono CategoryTheory.InducedCategory.Hom.hom CategoryTheory.ObjectProperty.FullSubcategory CategoryTheory.Iso.hom CategoryTheory.MonoOver CategoryTheory.ObjectProperty.FullSubcategory.category mkArrowIso CategoryTheory.CategoryStruct.id CategoryTheory.Category.toCategoryStruct	—	mono
mkArrowIso_inv_hom_left 📖	mathematical	—	CategoryTheory.CommaMorphism.left CategoryTheory.Discrete CategoryTheory.discreteCategory CategoryTheory.Functor.id CategoryTheory.Functor.fromPUnit CategoryTheory.ObjectProperty.FullSubcategory.obj CategoryTheory.Over CategoryTheory.instCategoryOver CategoryTheory.Over.isMono CategoryTheory.Comma.left arrow mono CategoryTheory.InducedCategory.Hom.hom CategoryTheory.ObjectProperty.FullSubcategory CategoryTheory.Iso.inv CategoryTheory.MonoOver CategoryTheory.ObjectProperty.FullSubcategory.category mkArrowIso CategoryTheory.CategoryStruct.id CategoryTheory.Category.toCategoryStruct	—	mono
mk_arrow 📖	mathematical	—	arrow	—	—
mk_coe 📖	mathematical	—	CategoryTheory.Comma.left CategoryTheory.Discrete CategoryTheory.discreteCategory CategoryTheory.Functor.id CategoryTheory.Functor.fromPUnit CategoryTheory.ObjectProperty.FullSubcategory.obj CategoryTheory.Over CategoryTheory.instCategoryOver CategoryTheory.Over.isMono	—	—
mk_obj 📖	mathematical	—	CategoryTheory.ObjectProperty.FullSubcategory.obj CategoryTheory.Over CategoryTheory.instCategoryOver CategoryTheory.Over.isMono	—	—
mono 📖	mathematical	—	CategoryTheory.Mono CategoryTheory.Comma.left CategoryTheory.Discrete CategoryTheory.discreteCategory CategoryTheory.Functor.id CategoryTheory.Functor.fromPUnit CategoryTheory.ObjectProperty.FullSubcategory.obj CategoryTheory.Over CategoryTheory.instCategoryOver CategoryTheory.Over.isMono arrow	—	CategoryTheory.ObjectProperty.FullSubcategory.property
mono_obj_hom 📖	mathematical	—	CategoryTheory.Mono 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.Comma.right CategoryTheory.Comma.hom	—	CategoryTheory.ObjectProperty.FullSubcategory.property
pullback_obj_arrow 📖	mathematical	—	arrow CategoryTheory.Functor.obj CategoryTheory.MonoOver CategoryTheory.ObjectProperty.FullSubcategory.category CategoryTheory.Over CategoryTheory.instCategoryOver CategoryTheory.Over.isMono pullback CategoryTheory.Limits.pullback.snd CategoryTheory.Functor.id CategoryTheory.Comma.left CategoryTheory.Discrete CategoryTheory.discreteCategory CategoryTheory.Functor.fromPUnit forget CategoryTheory.Comma.right CategoryTheory.Comma.hom	—	—
pullback_obj_left 📖	mathematical	—	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.MonoOver CategoryTheory.ObjectProperty.FullSubcategory.category pullback CategoryTheory.Limits.pullback arrow CategoryTheory.Limits.hasLimitOfHasLimitsOfShape CategoryTheory.Limits.WalkingCospan CategoryTheory.Limits.WidePullbackShape.category CategoryTheory.Limits.WalkingPair CategoryTheory.Limits.cospan	—	—
w 📖	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.CommaMorphism.left CategoryTheory.InducedCategory.Hom.hom CategoryTheory.ObjectProperty.FullSubcategory arrow	—	CategoryTheory.Over.w
w_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.CommaMorphism.left CategoryTheory.InducedCategory.Hom.hom CategoryTheory.ObjectProperty.FullSubcategory arrow	—	CategoryTheory.Category.assoc Mathlib.Tactic.Reassoc.eq_whisker' w

CategoryTheory.Over

Definitions

Name	Category	Theorems
isMono 📖	CompOp	98 math math: CategoryTheory.Subobject.factors_iff, CategoryTheory.MonoOver.mk_coe, CategoryTheory.MonoOver.congr_unitIso, CategoryTheory.IsGrothendieckAbelian.IsPresentable.injectivity₀.F_obj, CategoryTheory.MonoOver.mapIso_functor, CategoryTheory.MonoOver.mk_obj, CategoryTheory.MonoOver.isIso_left_iff_subobjectMk_eq, CategoryTheory.MonoOver.hasColimitsOfSize_of_hasStrongEpiMonoFactorisations, CategoryTheory.MonoOver.instIsRightAdjointOverForget, CategoryTheory.MonoOver.isIso_iff_subobjectMk_eq, CategoryTheory.Classifier.SubobjectRepresentableBy.iso_inv_hom_left_comp, CategoryTheory.MonoOver.mapIso_unitIso, CategoryTheory.IsGrothendieckAbelian.IsPresentable.surjectivity.F_map, CategoryTheory.MonoOver.mapIso_counitIso, Types.monoOverEquivalenceSet_inverse_map, CategoryTheory.MonoOver.mkArrowIso_hom_hom_left, CategoryTheory.MonoOver.map_obj_left, CategoryTheory.MonoOver.isIso_hom_left_iff_subobjectMk_eq, CategoryTheory.essentiallySmall_monoOver, CategoryTheory.MonoOver.pullback_obj_arrow, CategoryTheory.Subfunctor.equivalenceMonoOver_inverse_map, CategoryTheory.MonoOver.image_map, CategoryTheory.Subfunctor.equivalenceMonoOver_functor_map, CategoryTheory.Subobject.inf_eq_map_pullback', CategoryTheory.monoOver_terminal_to_subterminals_comp, CategoryTheory.MonoOver.image_obj, CategoryTheory.Subfunctor.equivalenceMonoOver_inverse_obj, CategoryTheory.MonoOver.bot_left, CategoryTheory.MonoOver.map_obj_arrow, CategoryTheory.subterminalsEquivMonoOverTerminal_inverse_map, CategoryTheory.Subobject.lower_comm, CategoryTheory.MonoOver.w, CategoryTheory.MonoOver.bot_arrow_eq_zero, CategoryTheory.MonoOver.hasFiniteLimits, CategoryTheory.Subfunctor.equivalenceMonoOver_functor_obj, CategoryTheory.IsGrothendieckAbelian.IsPresentable.injectivity₀.F_map, CategoryTheory.isEventuallyConstant_of_isArtinianObject, CategoryTheory.MonoOver.mk'_coe', CategoryTheory.MonoOver.mono, CategoryTheory.MonoOver.forget_obj_left, CategoryTheory.Subobject.instIsEquivalenceMonoOverRepresentative, Types.monoOverEquivalenceSet_functor_map, CategoryTheory.subterminalsEquivMonoOverTerminal_inverse_obj_obj, Types.monoOverEquivalenceSet_functor_obj, CategoryTheory.MonoOver.hasLimitsOfShape, CategoryTheory.MonoOver.congr_functor, CategoryTheory.MonoOver.isIso_iff_isIso_hom_left, CategoryTheory.MonoOver.congr_inverse, CategoryTheory.Classifier.SubobjectRepresentableBy.iso_inv_left_π_assoc, CategoryTheory.Subobject.lowerEquivalence_counitIso, CategoryTheory.subterminalsEquivMonoOverTerminal_functor_map, CategoryTheory.IsGrothendieckAbelian.generatingMonomorphisms.functorToMonoOver_map, CategoryTheory.MonoOver.inf_map_app, CategoryTheory.MonoOver.isThin, CategoryTheory.MonoOver.mkArrowIso_inv_hom_left, CategoryTheory.MonoOver.w_assoc, CategoryTheory.Classifier.SubobjectRepresentableBy.iso_inv_hom_left_comp_assoc, CategoryTheory.MonoOver.pullback_obj_left, CategoryTheory.Subobject.lowerEquivalence_unitIso, CategoryTheory.Subfunctor.equivalenceMonoOver_unitIso, CategoryTheory.MonoOver.subobjectMk_le_mk_of_hom, CategoryTheory.subterminalsEquivMonoOverTerminal_unitIso, CategoryTheory.MonoOver.forget_obj_hom, CategoryTheory.Classifier.SubobjectRepresentableBy.iso_inv_left_comp, CategoryTheory.MonoOver.commSqOfHasStrongEpiMonoFactorisation, CategoryTheory.subterminalsEquivMonoOverTerminal_counitIso, CategoryTheory.Classifier.SubobjectRepresentableBy.iso_inv_left_π, Types.monoOverEquivalenceSet_inverse_obj, CategoryTheory.MonoOver.hasLimit, CategoryTheory.MonoOver.instMonoHomDiscretePUnitObjOverForget, CategoryTheory.IsGrothendieckAbelian.IsPresentable.surjectivity.F_obj, CategoryTheory.MonoOver.inf_obj, CategoryTheory.MonoOver.top_left, Types.monoOverEquivalenceSet_unitIso, CategoryTheory.IsGrothendieckAbelian.generatingMonomorphisms.functorToMonoOver_obj, CategoryTheory.Subobject.representative_coe, CategoryTheory.MonoOver.full_map, CategoryTheory.Subobject.inf_eq_map_pullback, CategoryTheory.MonoOver.mapIso_inverse, CategoryTheory.MonoOver.congr_counitIso, CategoryTheory.Subobject.lowerEquivalence_inverse, CategoryTheory.Subobject.lowerEquivalence_functor, CategoryTheory.isEventuallyConstant_of_isNoetherianObject, CategoryTheory.MonoOver.faithful_exists, CategoryTheory.isNoetherianObject_iff_isEventuallyConstant, Types.monoOverEquivalenceSet_counitIso, CategoryTheory.subterminalsEquivMonoOverTerminal_functor_obj_obj, CategoryTheory.isArtinianObject_iff_isEventuallyConstant, CategoryTheory.MonoOver.faithful_map, CategoryTheory.MonoOver.hasLimitsOfSize, CategoryTheory.subterminals_to_monoOver_terminal_comp_forget, CategoryTheory.Subobject.representative_arrow, CategoryTheory.Subfunctor.equivalenceMonoOver_counitIso, CategoryTheory.MonoOver.mono_obj_hom, CategoryTheory.MonoOver.instIsClosedUnderLimitsOfShapeOverIsMono, CategoryTheory.MonoOver.isIso_iff_isIso_left, CategoryTheory.MonoOver.instIsIsoLeftDiscretePUnitHomFullSubcategoryOverIsMono, CategoryTheory.essentiallySmall_monoOver_iff_small_subobject

---

← Back to Index