Documentation Verification Report

ColimCoyoneda

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

Statistics

Metric	Count
Definitions `F`, `f`, `g`, `F`, `f`	5
Theorems `injectivity`, `injectivity₀`, `F_map`, `F_obj`, `epi_f`, `g_app`, `hf`, `surjectivity`, `F_map`, `F_obj`, `epi_f`, `hf`, `isIso_f`, `preservesColimit_coyoneda_obj_of_mono`	14
Total	19

CategoryTheory.IsGrothendieckAbelian

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`preservesColimit_coyoneda_obj_of_mono` 📖	mathematical	`HasCardinalLT` `CategoryTheory.Subobject` `CategoryTheory.Mono` `CategoryTheory.Functor.obj` `CategoryTheory.Functor.map`	`CategoryTheory.Limits.PreservesColimit` `CategoryTheory.types` `Opposite` `CategoryTheory.Category.opposite` `CategoryTheory.Functor` `CategoryTheory.Functor.category` `CategoryTheory.coyoneda` `Opposite.op`	—	`CategoryTheory.isFiltered_of_isCardinalFiltered` `CategoryTheory.IsFiltered.toIsFilteredOrEmpty` `IsPresentable.surjectivity` `IsPresentable.injectivity`

CategoryTheory.IsGrothendieckAbelian.IsPresentable

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`injectivity` 📖	mathematical	`HasCardinalLT` `CategoryTheory.Subobject` `CategoryTheory.CategoryStruct.comp` `CategoryTheory.Category.toCategoryStruct` `CategoryTheory.Functor.obj` `CategoryTheory.Functor` `CategoryTheory.Functor.category` `CategoryTheory.Functor.const` `CategoryTheory.Limits.Cocone.pt` `CategoryTheory.NatTrans.app` `CategoryTheory.Limits.Cocone.ι`	`CategoryTheory.Functor.map`	—	`injectivity₀` `CategoryTheory.Preadditive.sub_comp` `sub_eq_zero`
`injectivity₀` 📖	mathematical	`HasCardinalLT` `CategoryTheory.Subobject` `CategoryTheory.CategoryStruct.comp` `CategoryTheory.Category.toCategoryStruct` `CategoryTheory.Functor.obj` `CategoryTheory.Functor` `CategoryTheory.Functor.category` `CategoryTheory.Functor.const` `CategoryTheory.Limits.Cocone.pt` `CategoryTheory.NatTrans.app` `CategoryTheory.Limits.Cocone.ι` `Quiver.Hom` `CategoryTheory.CategoryStruct.toQuiver` `CategoryTheory.Limits.HasZeroMorphisms.zero` `CategoryTheory.Preadditive.preadditiveHasZeroMorphisms` `CategoryTheory.Abelian.toPreadditive`	`CategoryTheory.Functor.map`	—	`CategoryTheory.isFiltered_of_isCardinalFiltered` `CategoryTheory.IsGrothendieckAbelian.exists_isIso_of_functor_from_monoOver` `CategoryTheory.isCardinalFiltered_under` `CategoryTheory.Limits.functorCategoryHasLimit` `CategoryTheory.Limits.hasLimitOfHasLimitsOfShape` `CategoryTheory.Abelian.hasEqualizers` `CategoryTheory.Limits.hasColimitOfHasColimitsOfShape` `CategoryTheory.Limits.hasColimitsOfShape_of_has_filtered_colimits` `CategoryTheory.IsGrothendieckAbelian.hasFilteredColimitsOfSize` `CategoryTheory.IsFiltered.under` `CategoryTheory.IsFiltered.toIsFilteredOrEmpty` `injectivity₀.hf` `injectivity₀.epi_f` `CategoryTheory.cancel_epi` `CategoryTheory.epi_of_effectiveEpi` `CategoryTheory.instEffectiveEpiOfIsIso` `CategoryTheory.Limits.comp_zero` `CategoryTheory.NatTrans.congr_app` `CategoryTheory.Limits.kernel.condition`
`surjectivity` 📖	mathematical	`CategoryTheory.Mono` `CategoryTheory.Functor.obj` `CategoryTheory.Functor.map` `HasCardinalLT` `CategoryTheory.Subobject`	`CategoryTheory.CategoryStruct.comp` `CategoryTheory.Category.toCategoryStruct` `CategoryTheory.Functor` `CategoryTheory.Functor.category` `CategoryTheory.Functor.const` `CategoryTheory.Limits.Cocone.pt` `CategoryTheory.NatTrans.app` `CategoryTheory.Limits.Cocone.ι`	—	`CategoryTheory.isFiltered_of_isCardinalFiltered` `CategoryTheory.Limits.IsColimit.mono_ι_app_of_isFiltered` `CategoryTheory.NatTrans.mono_of_mono_app` `CategoryTheory.Limits.hasColimitsOfShape_of_has_filtered_colimits` `CategoryTheory.IsGrothendieckAbelian.hasFilteredColimitsOfSize` `CategoryTheory.IsFiltered.under` `CategoryTheory.IsFiltered.toIsFilteredOrEmpty` `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` `CategoryTheory.IsGrothendieckAbelian.ab5OfSize` `CategoryTheory.Functor.preservesHomologyOfExact` `CategoryTheory.Limits.PreservesColimits.preservesFiniteColimits` `CategoryTheory.Adjunction.colim_preservesColimits` `CategoryTheory.IsGrothendieckAbelian.exists_isIso_of_functor_from_monoOver` `CategoryTheory.Limits.hasColimitOfHasColimitsOfShape` `surjectivity.hf` `surjectivity.epi_f` `CategoryTheory.Category.assoc` `CategoryTheory.IsIso.eq_inv_comp` `CategoryTheory.NatTrans.comp_app` `CategoryTheory.Limits.pullback.condition` `CategoryTheory.Functor.const_map_app`

CategoryTheory.IsGrothendieckAbelian.IsPresentable.injectivity₀

Definitions

Name	Category	Theorems
`F` 📖	CompOp	2 math math: `F_obj`, `F_map`
`f` 📖	CompOp	2 math math: `hf`, `epi_f`
`g` 📖	CompOp	5 math math: `F_obj`, `g_app`, `F_map`, `hf`, `epi_f`

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`F_map` 📖	mathematical	—	`CategoryTheory.Functor.map` `CategoryTheory.Under` `CategoryTheory.instCategoryUnder` `CategoryTheory.MonoOver` `CategoryTheory.ObjectProperty.FullSubcategory.category` `CategoryTheory.Over` `CategoryTheory.instCategoryOver` `CategoryTheory.Over.isMono` `F` `CategoryTheory.MonoOver.homMk` `CategoryTheory.Functor.obj` `CategoryTheory.Limits.kernel` `CategoryTheory.Functor` `CategoryTheory.Functor.category` `CategoryTheory.Limits.instHasZeroMorphismsFunctor` `CategoryTheory.Preadditive.preadditiveHasZeroMorphisms` `CategoryTheory.Abelian.toPreadditive` `CategoryTheory.Functor.const` `CategoryTheory.Functor.comp` `CategoryTheory.Under.forget` `g` `CategoryTheory.NatTrans.app` `CategoryTheory.Limits.kernel.ι`	—	—
`F_obj` 📖	mathematical	—	`CategoryTheory.Functor.obj` `CategoryTheory.Under` `CategoryTheory.instCategoryUnder` `CategoryTheory.MonoOver` `CategoryTheory.ObjectProperty.FullSubcategory.category` `CategoryTheory.Over` `CategoryTheory.instCategoryOver` `CategoryTheory.Over.isMono` `F` `CategoryTheory.Limits.kernel` `CategoryTheory.Functor` `CategoryTheory.Functor.category` `CategoryTheory.Limits.instHasZeroMorphismsFunctor` `CategoryTheory.Preadditive.preadditiveHasZeroMorphisms` `CategoryTheory.Abelian.toPreadditive` `CategoryTheory.Functor.const` `CategoryTheory.Functor.comp` `CategoryTheory.Under.forget` `g` `CategoryTheory.NatTrans.app` `CategoryTheory.Limits.kernel.ι`	—	—
`epi_f` 📖	mathematical	`CategoryTheory.CategoryStruct.comp` `CategoryTheory.Category.toCategoryStruct` `CategoryTheory.Functor.obj` `CategoryTheory.Functor` `CategoryTheory.Functor.category` `CategoryTheory.Functor.const` `CategoryTheory.Limits.Cocone.pt` `CategoryTheory.NatTrans.app` `CategoryTheory.Limits.Cocone.ι` `Quiver.Hom` `CategoryTheory.CategoryStruct.toQuiver` `CategoryTheory.Limits.HasZeroMorphisms.zero` `CategoryTheory.Preadditive.preadditiveHasZeroMorphisms` `CategoryTheory.Abelian.toPreadditive`	`CategoryTheory.Epi` `CategoryTheory.Limits.colimit` `CategoryTheory.Under` `CategoryTheory.instCategoryUnder` `CategoryTheory.Limits.kernel` `CategoryTheory.Limits.instHasZeroMorphismsFunctor` `CategoryTheory.Functor.comp` `CategoryTheory.Under.forget` `g` `CategoryTheory.Limits.functorCategoryHasLimit` `CategoryTheory.Limits.WalkingParallelPair` `CategoryTheory.Limits.walkingParallelPairHomCategory` `CategoryTheory.Limits.parallelPair` `CategoryTheory.Limits.hasLimitOfHasLimitsOfShape` `CategoryTheory.Abelian.hasEqualizers` `CategoryTheory.Functor.flip` `CategoryTheory.Limits.hasColimitOfHasColimitsOfShape` `CategoryTheory.Limits.hasColimitsOfShapeOfHasColimitsOfSize` `CategoryTheory.IsGrothendieckAbelian.hasColimits` `f`	—	`CategoryTheory.ShortComplex.Exact.epi_f` `CategoryTheory.Limits.functorCategoryHasLimit` `CategoryTheory.Limits.hasLimitOfHasLimitsOfShape` `CategoryTheory.Abelian.hasEqualizers` `CategoryTheory.Limits.kernel.condition` `CategoryTheory.Limits.hasColimitOfHasColimitsOfShape` `CategoryTheory.Limits.hasColimitsOfShape_of_has_filtered_colimits` `CategoryTheory.IsGrothendieckAbelian.hasFilteredColimitsOfSize` `CategoryTheory.IsFiltered.under` `CategoryTheory.IsFiltered.toIsFilteredOrEmpty` `CategoryTheory.Category.comp_id` `hf` `CategoryTheory.Limits.comp_zero` `CategoryTheory.Category.assoc` `CategoryTheory.NatTrans.naturality` `CategoryTheory.Limits.colim.exact_mapShortComplex` `CategoryTheory.AB5OfSize.ofShape` `CategoryTheory.IsGrothendieckAbelian.ab5OfSize` `CategoryTheory.ShortComplex.exact_of_f_is_kernel` `CategoryTheory.CategoryWithHomology.hasHomology` `CategoryTheory.categoryWithHomology_of_abelian` `CategoryTheory.IsFiltered.isConnected` `CategoryTheory.Under.final_forget`
`g_app` 📖	mathematical	—	`CategoryTheory.NatTrans.app` `CategoryTheory.Under` `CategoryTheory.instCategoryUnder` `CategoryTheory.Functor.obj` `CategoryTheory.Functor` `CategoryTheory.Functor.category` `CategoryTheory.Functor.const` `CategoryTheory.Functor.comp` `CategoryTheory.Under.forget` `g` `CategoryTheory.CategoryStruct.comp` `CategoryTheory.Category.toCategoryStruct` `CategoryTheory.Functor.map` `CategoryTheory.Comma.hom` `CategoryTheory.Discrete` `CategoryTheory.discreteCategory` `CategoryTheory.Functor.fromPUnit` `CategoryTheory.Functor.id`	—	—
`hf` 📖	mathematical	—	`CategoryTheory.CategoryStruct.comp` `CategoryTheory.Category.toCategoryStruct` `CategoryTheory.Functor.obj` `CategoryTheory.Under` `CategoryTheory.instCategoryUnder` `CategoryTheory.Limits.kernel` `CategoryTheory.Functor` `CategoryTheory.Functor.category` `CategoryTheory.Limits.instHasZeroMorphismsFunctor` `CategoryTheory.Preadditive.preadditiveHasZeroMorphisms` `CategoryTheory.Abelian.toPreadditive` `CategoryTheory.Functor.const` `CategoryTheory.Functor.comp` `CategoryTheory.Under.forget` `g` `CategoryTheory.Limits.functorCategoryHasLimit` `CategoryTheory.Limits.WalkingParallelPair` `CategoryTheory.Limits.walkingParallelPairHomCategory` `CategoryTheory.Limits.parallelPair` `Quiver.Hom` `CategoryTheory.CategoryStruct.toQuiver` `CategoryTheory.Limits.HasZeroMorphisms.zero` `CategoryTheory.Limits.hasLimitOfHasLimitsOfShape` `CategoryTheory.Abelian.hasEqualizers` `CategoryTheory.Functor.flip` `CategoryTheory.Limits.colimit` `CategoryTheory.Limits.hasColimitOfHasColimitsOfShape` `CategoryTheory.Limits.hasColimitsOfShapeOfHasColimitsOfSize` `CategoryTheory.IsGrothendieckAbelian.hasColimits` `CategoryTheory.Limits.colimit.ι` `f` `CategoryTheory.NatTrans.app` `CategoryTheory.Limits.kernel.ι`	—	`CategoryTheory.Limits.functorCategoryHasLimit` `CategoryTheory.Limits.hasLimitOfHasLimitsOfShape` `CategoryTheory.Abelian.hasEqualizers` `CategoryTheory.Limits.hasColimitOfHasColimitsOfShape` `CategoryTheory.Limits.hasColimitsOfShapeOfHasColimitsOfSize` `CategoryTheory.IsGrothendieckAbelian.hasColimits` `CategoryTheory.Limits.IsColimit.ι_map` `CategoryTheory.Category.comp_id`

CategoryTheory.IsGrothendieckAbelian.IsPresentable.surjectivity

Definitions

Name	Category	Theorems
`F` 📖	CompOp	2 math math: `F_map`, `F_obj`
`f` 📖	CompOp	3 math math: `hf`, `isIso_f`, `epi_f`

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`F_map` 📖	mathematical	—	`CategoryTheory.Functor.map` `CategoryTheory.MonoOver` `CategoryTheory.ObjectProperty.FullSubcategory.category` `CategoryTheory.Over` `CategoryTheory.instCategoryOver` `CategoryTheory.Over.isMono` `F` `CategoryTheory.MonoOver.homMk` `CategoryTheory.Functor.obj` `CategoryTheory.Limits.pullback` `CategoryTheory.Functor` `CategoryTheory.Functor.category` `CategoryTheory.Functor.const` `CategoryTheory.Limits.Cocone.pt` `CategoryTheory.Limits.Cocone.ι` `CategoryTheory.NatTrans.app` `CategoryTheory.Limits.pullback.snd`	—	—
`F_obj` 📖	mathematical	—	`CategoryTheory.Functor.obj` `CategoryTheory.MonoOver` `CategoryTheory.ObjectProperty.FullSubcategory.category` `CategoryTheory.Over` `CategoryTheory.instCategoryOver` `CategoryTheory.Over.isMono` `F` `CategoryTheory.Limits.pullback` `CategoryTheory.Functor` `CategoryTheory.Functor.category` `CategoryTheory.Functor.const` `CategoryTheory.Limits.Cocone.pt` `CategoryTheory.Limits.Cocone.ι` `CategoryTheory.Functor.map` `CategoryTheory.NatTrans.app` `CategoryTheory.Limits.pullback.snd`	—	—
`epi_f` 📖	mathematical	—	`CategoryTheory.Epi` `CategoryTheory.Limits.colimit` `CategoryTheory.Limits.pullback` `CategoryTheory.Functor` `CategoryTheory.Functor.category` `CategoryTheory.Functor.obj` `CategoryTheory.Functor.const` `CategoryTheory.Limits.Cocone.pt` `CategoryTheory.Limits.Cocone.ι` `CategoryTheory.Functor.map` `CategoryTheory.Limits.functorCategoryHasLimit` `CategoryTheory.Limits.WalkingCospan` `CategoryTheory.Limits.WidePullbackShape.category` `CategoryTheory.Limits.WalkingPair` `CategoryTheory.Limits.cospan` `CategoryTheory.Limits.hasLimitOfHasLimitsOfShape` `CategoryTheory.Limits.hasLimitsOfShape_widePullbackShape` `Finite.of_fintype` `CategoryTheory.Limits.fintypeWalkingPair` `CategoryTheory.Limits.hasFiniteWidePullbacks_of_hasFiniteLimits` `CategoryTheory.Abelian.hasFiniteLimits` `CategoryTheory.Functor.flip` `CategoryTheory.Limits.hasColimitOfHasColimitsOfShape` `CategoryTheory.Limits.hasColimitsOfShapeOfHasColimitsOfSize` `CategoryTheory.IsGrothendieckAbelian.hasColimits` `f`	—	`CategoryTheory.Limits.functorCategoryHasLimit` `CategoryTheory.Limits.hasLimitOfHasLimitsOfShape` `CategoryTheory.Limits.hasLimitsOfShape_widePullbackShape` `Finite.of_fintype` `CategoryTheory.Limits.hasFiniteWidePullbacks_of_hasFiniteLimits` `CategoryTheory.Abelian.hasFiniteLimits` `CategoryTheory.Limits.hasColimitOfHasColimitsOfShape` `CategoryTheory.Limits.hasColimitsOfShapeOfHasColimitsOfSize` `CategoryTheory.IsGrothendieckAbelian.hasColimits` `isIso_f` `CategoryTheory.epi_of_effectiveEpi` `CategoryTheory.instEffectiveEpiOfIsIso`
`hf` 📖	mathematical	—	`CategoryTheory.CategoryStruct.comp` `CategoryTheory.Category.toCategoryStruct` `CategoryTheory.Functor.obj` `CategoryTheory.Limits.pullback` `CategoryTheory.Functor` `CategoryTheory.Functor.category` `CategoryTheory.Functor.const` `CategoryTheory.Limits.Cocone.pt` `CategoryTheory.Limits.Cocone.ι` `CategoryTheory.Functor.map` `CategoryTheory.Limits.functorCategoryHasLimit` `CategoryTheory.Limits.WalkingCospan` `CategoryTheory.Limits.WidePullbackShape.category` `CategoryTheory.Limits.WalkingPair` `CategoryTheory.Limits.cospan` `CategoryTheory.Limits.hasLimitOfHasLimitsOfShape` `CategoryTheory.Limits.hasLimitsOfShape_widePullbackShape` `Finite.of_fintype` `CategoryTheory.Limits.fintypeWalkingPair` `CategoryTheory.Limits.hasFiniteWidePullbacks_of_hasFiniteLimits` `CategoryTheory.Abelian.hasFiniteLimits` `CategoryTheory.Functor.flip` `CategoryTheory.Limits.colimit` `CategoryTheory.Limits.hasColimitOfHasColimitsOfShape` `CategoryTheory.Limits.hasColimitsOfShapeOfHasColimitsOfSize` `CategoryTheory.IsGrothendieckAbelian.hasColimits` `CategoryTheory.Limits.colimit.ι` `f` `CategoryTheory.NatTrans.app` `CategoryTheory.Limits.pullback.snd`	—	`CategoryTheory.Limits.colimit.ι_desc` `CategoryTheory.Limits.functorCategoryHasLimit` `CategoryTheory.Limits.hasLimitOfHasLimitsOfShape` `CategoryTheory.Limits.hasLimitsOfShape_widePullbackShape` `Finite.of_fintype` `CategoryTheory.Limits.hasFiniteWidePullbacks_of_hasFiniteLimits` `CategoryTheory.Abelian.hasFiniteLimits` `CategoryTheory.Limits.hasColimitOfHasColimitsOfShape` `CategoryTheory.Limits.hasColimitsOfShapeOfHasColimitsOfSize` `CategoryTheory.IsGrothendieckAbelian.hasColimits`
`isIso_f` 📖	mathematical	—	`CategoryTheory.IsIso` `CategoryTheory.Limits.colimit` `CategoryTheory.Limits.pullback` `CategoryTheory.Functor` `CategoryTheory.Functor.category` `CategoryTheory.Functor.obj` `CategoryTheory.Functor.const` `CategoryTheory.Limits.Cocone.pt` `CategoryTheory.Limits.Cocone.ι` `CategoryTheory.Functor.map` `CategoryTheory.Limits.functorCategoryHasLimit` `CategoryTheory.Limits.WalkingCospan` `CategoryTheory.Limits.WidePullbackShape.category` `CategoryTheory.Limits.WalkingPair` `CategoryTheory.Limits.cospan` `CategoryTheory.Limits.hasLimitOfHasLimitsOfShape` `CategoryTheory.Limits.hasLimitsOfShape_widePullbackShape` `Finite.of_fintype` `CategoryTheory.Limits.fintypeWalkingPair` `CategoryTheory.Limits.hasFiniteWidePullbacks_of_hasFiniteLimits` `CategoryTheory.Abelian.hasFiniteLimits` `CategoryTheory.Functor.flip` `CategoryTheory.Limits.hasColimitOfHasColimitsOfShape` `CategoryTheory.Limits.hasColimitsOfShapeOfHasColimitsOfSize` `CategoryTheory.IsGrothendieckAbelian.hasColimits` `f`	—	`CategoryTheory.Limits.hasColimitsOfShape_of_has_filtered_colimits` `CategoryTheory.IsGrothendieckAbelian.hasFilteredColimitsOfSize` `CategoryTheory.Limits.functorCategoryHasLimit` `CategoryTheory.Limits.hasLimitOfHasLimitsOfShape` `CategoryTheory.Limits.hasLimitsOfShape_widePullbackShape` `Finite.of_fintype` `CategoryTheory.Limits.hasFiniteWidePullbacks_of_hasFiniteLimits` `CategoryTheory.Abelian.hasFiniteLimits` `CategoryTheory.Limits.hasColimitOfHasColimitsOfShape` `CategoryTheory.Limits.hasColimitsOfShapeOfHasColimitsOfSize` `CategoryTheory.IsGrothendieckAbelian.hasColimits` `CategoryTheory.MorphismProperty.arrow_mk_iso_iff` `CategoryTheory.MorphismProperty.RespectsIso.isomorphisms` `CategoryTheory.IsFiltered.isConnected` `CategoryTheory.Limits.colimit.hom_ext` `CategoryTheory.Category.id_comp` `CategoryTheory.Limits.ι_colimMap_assoc` `CategoryTheory.Limits.colimit.comp_coconePointUniqueUpToIso_hom` `CategoryTheory.Limits.constCocone_ι` `CategoryTheory.NatTrans.id_app` `CategoryTheory.Category.comp_id` `hf` `CategoryTheory.MorphismProperty.of_isPullback` `CategoryTheory.MorphismProperty.IsStableUnderBaseChange.isomorphisms` `CategoryTheory.IsPullback.map` `CategoryTheory.Limits.PreservesLimitsOfShape.preservesLimit` `CategoryTheory.Limits.PreservesFiniteLimits.preservesFiniteLimits` `CategoryTheory.HasExactColimitsOfShape.preservesFiniteLimits` `CategoryTheory.AB5OfSize.ofShape` `CategoryTheory.IsGrothendieckAbelian.ab5OfSize` `CategoryTheory.IsPullback.of_hasPullback` `CategoryTheory.IsIso.id`

---

← Back to Index