Abelian

📁 Source: Mathlib/Topology/Sheaves/Abelian.lean

Statistics

Metric	Count
Definitions instAbelian, instAbelianPresheaf	2
Theorems exact_iff_stalkFunctor_map_exact, instAdditivePresheafForget, instIsGrothendieckAbelian, instPreservesFiniteLimitsCompPresheafForgetStalkFunctor, isZero_iff_stalkFunctor_obj_isZero, instAdditivePresheafStalkFunctor	6
Total	8

TopCat

Definitions

Name	Category	Theorems
instAbelianPresheaf 📖	CompOp	4 math math: Sheaf.exact_iff_stalkFunctor_map_exact, instAdditivePresheafStalkFunctor, Sheaf.instAdditivePresheafForget, Presheaf.sections_exact_of_exact

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
instAdditivePresheafStalkFunctor 📖	mathematical	—	CategoryTheory.Functor.Additive Presheaf instCategoryPresheaf CategoryTheory.Abelian.toPreadditive instAbelianPresheaf Presheaf.stalkFunctor	—	CategoryTheory.Functor.instAdditiveComp instAdditiveFunctorColim

TopCat.Sheaf

Definitions

Name	Category	Theorems
instAbelian 📖	CompOp	6 math math: exact_iff_stalkFunctor_map_exact, IsFlasque.epi_of_shortExact, sections_exact_of_left_exact, instIsGrothendieckAbelian, IsFlasque.of_shortExact_of_isFlasque₁₂, instAdditivePresheafForget

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
exact_iff_stalkFunctor_map_exact 📖	mathematical	—	CategoryTheory.ShortComplex.Exact TopCat.Sheaf TopCat.instCategorySheaf CategoryTheory.Preadditive.preadditiveHasZeroMorphisms CategoryTheory.Abelian.toPreadditive instAbelian CategoryTheory.instHasSheafifyOfPreservesLimitsForgetOfHasFiniteLimitsOfSmallOppositeCover TopologicalSpace.Opens TopCat.carrier TopCat.str Preorder.smallCategory PartialOrder.toPreorder TopologicalSpace.Opens.instPartialOrder Opens.grothendieckTopology CategoryTheory.Limits.hasLimitOfHasLimitsOfShape CategoryTheory.Limits.WalkingMulticospan CategoryTheory.GrothendieckTopology.Cover.shape CategoryTheory.Limits.WalkingMulticospan.instSmallCategory CategoryTheory.Limits.hasLimitsOfShapeOfHasLimits CategoryTheory.Limits.MulticospanIndex.multicospan CategoryTheory.GrothendieckTopology.Cover.index CategoryTheory.Limits.hasColimitsOfShape_of_has_filtered_colimits CategoryTheory.Limits.hasFilteredColimitsOfSize_of_hasColimitsOfSize Opposite CategoryTheory.GrothendieckTopology.Cover CategoryTheory.Category.opposite CategoryTheory.GrothendieckTopology.instPreorderCover CategoryTheory.isFiltered_op_of_isCofiltered CategoryTheory.isCofiltered_of_directed_ge_nonempty SemilatticeInf.instIsCodirectedOrder CategoryTheory.GrothendieckTopology.Cover.instSemilatticeInf CategoryTheory.GrothendieckTopology.Cover.instInhabited CategoryTheory.Limits.PreservesFilteredColimitsOfSize.preserves_filtered_colimits CategoryTheory.types CategoryTheory.forget CategoryTheory.reflectsIsomorphisms_of_reflectsMonomorphisms_of_reflectsEpimorphisms CategoryTheory.balanced_of_strongMonoCategory CategoryTheory.strongMonoCategory_of_regularMonoCategory CategoryTheory.regularMonoCategoryOfNormalMonoCategory CategoryTheory.Abelian.toIsNormalMonoCategory CategoryTheory.Functor.reflectsMonomorphisms_of_faithful CategoryTheory.instFaithfulForget CategoryTheory.Functor.reflectsEpimorphisms_of_faithful CategoryTheory.Limits.PreservesLimitsOfSize.preservesLimitsOfShape CategoryTheory.Limits.hasFiniteLimits_of_hasCountableLimits CategoryTheory.Limits.hasCountableLimits_of_hasLimits Opposite.small UnivLE.small UnivLE.self CategoryTheory.ShortComplex.map CategoryTheory.Functor.comp TopCat.Presheaf TopCat.instCategoryPresheaf forget TopCat.Presheaf.stalkFunctor CategoryTheory.Functor.preservesZeroMorphisms_comp TopCat.instAbelianPresheaf CategoryTheory.Functor.preservesZeroMorphisms_of_additive instAdditivePresheafForget TopCat.instAdditivePresheafStalkFunctor	—	CategoryTheory.instHasSheafifyOfPreservesLimitsForgetOfHasFiniteLimitsOfSmallOppositeCover CategoryTheory.Limits.hasLimitOfHasLimitsOfShape CategoryTheory.Limits.hasLimitsOfShapeOfHasLimits CategoryTheory.Limits.hasColimitsOfShape_of_has_filtered_colimits CategoryTheory.Limits.hasFilteredColimitsOfSize_of_hasColimitsOfSize CategoryTheory.isFiltered_op_of_isCofiltered CategoryTheory.isCofiltered_of_directed_ge_nonempty SemilatticeInf.instIsCodirectedOrder CategoryTheory.Limits.PreservesFilteredColimitsOfSize.preserves_filtered_colimits CategoryTheory.reflectsIsomorphisms_of_reflectsMonomorphisms_of_reflectsEpimorphisms CategoryTheory.balanced_of_strongMonoCategory CategoryTheory.strongMonoCategory_of_regularMonoCategory CategoryTheory.regularMonoCategoryOfNormalMonoCategory CategoryTheory.Abelian.toIsNormalMonoCategory CategoryTheory.Functor.reflectsMonomorphisms_of_faithful CategoryTheory.instFaithfulForget CategoryTheory.Functor.reflectsEpimorphisms_of_faithful CategoryTheory.Limits.PreservesLimitsOfSize.preservesLimitsOfShape CategoryTheory.Limits.hasFiniteLimits_of_hasCountableLimits CategoryTheory.Limits.hasCountableLimits_of_hasLimits Opposite.small UnivLE.small UnivLE.self CategoryTheory.Functor.preservesZeroMorphisms_comp CategoryTheory.Functor.preservesZeroMorphisms_of_additive instAdditivePresheafForget TopCat.instAdditivePresheafStalkFunctor CategoryTheory.Functor.instAdditiveComp List.TFAE.out CategoryTheory.Functor.exact_tfae CategoryTheory.Functor.preservesHomologyOfExact instPreservesFiniteLimitsCompPresheafForgetStalkFunctor CategoryTheory.Limits.PreservesColimits.preservesFiniteColimits CategoryTheory.Functor.instPreservesColimitsOfSizeOfIsLeftAdjoint instIsLeftAdjointSheafCompPresheafForgetStalkFunctor CategoryTheory.Limits.instHasProductsOfShapeOfHasCountableProductsOfCountable CategoryTheory.Limits.hasCountableProducts_of_hasCountableLimits CategoryTheory.CountableCategory.countableObj CategoryTheory.instCountableCategoryOfFinCategory Finite.of_fintype Preorder.subsingleton_hom CategoryTheory.CategoryWithHomology.hasHomology CategoryTheory.categoryWithHomology_of_abelian CategoryTheory.ShortComplex.exact_iff_isZero_homology isZero_iff_stalkFunctor_obj_isZero CategoryTheory.Limits.IsZero.of_iso CategoryTheory.ShortComplex.hasHomology_of_preserves CategoryTheory.Functor.PreservesHomology.preservesLeftHomologyOf CategoryTheory.Functor.PreservesHomology.preservesRightHomologyOf
instAdditivePresheafForget 📖	mathematical	—	CategoryTheory.Functor.Additive TopCat.Sheaf TopCat.Presheaf TopCat.instCategorySheaf TopCat.instCategoryPresheaf CategoryTheory.Abelian.toPreadditive instAbelian TopCat.instAbelianPresheaf forget	—	—
instIsGrothendieckAbelian 📖	mathematical	—	CategoryTheory.IsGrothendieckAbelian TopCat.Sheaf TopCat.instCategorySheaf instAbelian	—	—
instPreservesFiniteLimitsCompPresheafForgetStalkFunctor 📖	mathematical	—	CategoryTheory.Limits.PreservesFiniteLimits TopCat.Sheaf TopCat.instCategorySheaf CategoryTheory.Functor.comp TopCat.Presheaf TopCat.instCategoryPresheaf forget TopCat.Presheaf.stalkFunctor	—	CategoryTheory.instHasSheafifyOfPreservesLimitsForgetOfHasFiniteLimitsOfSmallOppositeCover CategoryTheory.Limits.hasLimitOfHasLimitsOfShape CategoryTheory.Limits.hasLimitsOfShapeOfHasLimits CategoryTheory.Limits.hasColimitsOfShape_of_has_filtered_colimits CategoryTheory.Limits.hasFilteredColimitsOfSize_of_hasColimitsOfSize CategoryTheory.isFiltered_op_of_isCofiltered CategoryTheory.isCofiltered_of_directed_ge_nonempty SemilatticeInf.instIsCodirectedOrder CategoryTheory.Limits.PreservesFilteredColimitsOfSize.preserves_filtered_colimits CategoryTheory.reflectsIsomorphisms_of_reflectsMonomorphisms_of_reflectsEpimorphisms CategoryTheory.balanced_of_strongMonoCategory CategoryTheory.strongMonoCategory_of_regularMonoCategory CategoryTheory.regularMonoCategoryOfNormalMonoCategory CategoryTheory.Abelian.toIsNormalMonoCategory CategoryTheory.Functor.reflectsMonomorphisms_of_faithful CategoryTheory.instFaithfulForget CategoryTheory.Functor.reflectsEpimorphisms_of_faithful CategoryTheory.Limits.PreservesLimitsOfSize.preservesLimitsOfShape CategoryTheory.Limits.hasFiniteLimits_of_hasCountableLimits CategoryTheory.Limits.hasCountableLimits_of_hasLimits Opposite.small UnivLE.small UnivLE.self CategoryTheory.Functor.preservesZeroMorphisms_comp CategoryTheory.Functor.preservesZeroMorphisms_of_additive instAdditivePresheafForget TopCat.instAdditivePresheafStalkFunctor CategoryTheory.Functor.instAdditiveComp List.TFAE.out CategoryTheory.Functor.exact_tfae CategoryTheory.Functor.preservesFiniteColimits_tfae CategoryTheory.Limits.PreservesColimits.preservesFiniteColimits CategoryTheory.Functor.instPreservesColimitsOfSizeOfIsLeftAdjoint instIsLeftAdjointSheafCompPresheafForgetStalkFunctor CategoryTheory.Limits.instHasProductsOfShapeOfHasCountableProductsOfCountable CategoryTheory.Limits.hasCountableProducts_of_hasCountableLimits CategoryTheory.CountableCategory.countableObj CategoryTheory.instCountableCategoryOfFinCategory Finite.of_fintype Preorder.subsingleton_hom CategoryTheory.ShortComplex.ShortExact.mk' CategoryTheory.ShortComplex.ShortExact.mono_f CategoryTheory.Functor.map_mono TopCat.Presheaf.stalkFunctor_preserves_mono CategoryTheory.Functor.preservesFiniteLimits_of_preservesHomology CategoryTheory.Abelian.hasZeroObject CategoryTheory.Limits.hasFiniteProducts_of_hasCountableProducts TopCat.instHasLimitsOfSizeSheafOfHasLimits CategoryTheory.Abelian.has_kernels
isZero_iff_stalkFunctor_obj_isZero 📖	mathematical	—	CategoryTheory.Limits.IsZero TopCat.Sheaf TopCat.instCategorySheaf CategoryTheory.Functor.obj CategoryTheory.Functor.comp TopCat.Presheaf TopCat.instCategoryPresheaf forget TopCat.Presheaf.stalkFunctor	—	CategoryTheory.Functor.map_isZero CategoryTheory.instHasSheafifyOfPreservesLimitsForgetOfHasFiniteLimitsOfSmallOppositeCover CategoryTheory.Limits.hasLimitOfHasLimitsOfShape CategoryTheory.Limits.hasLimitsOfShapeOfHasLimits CategoryTheory.Limits.hasColimitsOfShape_of_has_filtered_colimits CategoryTheory.Limits.hasFilteredColimitsOfSize_of_hasColimitsOfSize CategoryTheory.isFiltered_op_of_isCofiltered CategoryTheory.isCofiltered_of_directed_ge_nonempty SemilatticeInf.instIsCodirectedOrder CategoryTheory.Limits.PreservesFilteredColimitsOfSize.preserves_filtered_colimits CategoryTheory.reflectsIsomorphisms_of_reflectsMonomorphisms_of_reflectsEpimorphisms CategoryTheory.balanced_of_strongMonoCategory CategoryTheory.strongMonoCategory_of_regularMonoCategory CategoryTheory.regularMonoCategoryOfNormalMonoCategory CategoryTheory.Abelian.toIsNormalMonoCategory CategoryTheory.Functor.reflectsMonomorphisms_of_faithful CategoryTheory.instFaithfulForget CategoryTheory.Functor.reflectsEpimorphisms_of_faithful CategoryTheory.Limits.PreservesLimitsOfSize.preservesLimitsOfShape CategoryTheory.Limits.hasFiniteLimits_of_hasCountableLimits CategoryTheory.Limits.hasCountableLimits_of_hasLimits Opposite.small UnivLE.small UnivLE.self CategoryTheory.Functor.preservesZeroMorphisms_comp CategoryTheory.Functor.preservesZeroMorphisms_of_additive instAdditivePresheafForget TopCat.instAdditivePresheafStalkFunctor CategoryTheory.Abelian.hasZeroObject CategoryTheory.Limits.isZero_zero TopCat.Presheaf.isIso_iff_stalkFunctor_map_iso CategoryTheory.Limits.isIso_of_source_target_iso_zero CategoryTheory.Limits.IsZero.of_iso

---

← Back to Index