Sheafification

📁 Source: Mathlib/Algebra/Category/ModuleCat/Presheaf/Sheafification.lean

Statistics

Metric	Count
Definitions sheafification, sheafificationAdjunction, sheafificationCompForgetCompToPresheaf, sheafificationCompToSheaf, sheafificationHomEquiv	5
Theorems instIsLeftAdjointSheafOfModulesSheafification, instPreservesFiniteLimitsSheafAddCommGrpCatCompSheafOfModulesSheafificationToSheaf, instPreservesFiniteLimitsSheafOfModulesSheafification, instReflectsFiniteLimitsSheafOfModulesSheafAddCommGrpCatToSheaf, instReflectsIsomorphismsSheafOfModulesFunctorOppositeAddCommGrpCatCompSheafToSheafSheafToPresheaf, instReflectsIsomorphismsSheafOfModulesSheafAddCommGrpCatToSheaf, sheafificationAdjunction_homEquiv_apply, sheafification_map, toPresheaf_map_sheafificationAdjunction_unit_app, toPresheaf_map_sheafificationHomEquiv, toPresheaf_map_sheafificationHomEquiv_def, toSheaf_map_sheafificationHomEquiv_symm	12
Total	17

PresheafOfModules

Definitions

Name	Category	Theorems
sheafification 📖	CompOp	9 math math: instIsLeftAdjointSheafOfModulesSheafification, sheafification_map, toSheaf_map_sheafificationHomEquiv_symm, sheafificationAdjunction_homEquiv_apply, toPresheaf_map_sheafificationAdjunction_unit_app, toPresheaf_map_sheafificationHomEquiv_def, toPresheaf_map_sheafificationHomEquiv, instPreservesFiniteLimitsSheafOfModulesSheafification, instPreservesFiniteLimitsSheafAddCommGrpCatCompSheafOfModulesSheafificationToSheaf
sheafificationAdjunction 📖	CompOp	2 math math: sheafificationAdjunction_homEquiv_apply, toPresheaf_map_sheafificationAdjunction_unit_app
sheafificationCompForgetCompToPresheaf 📖	CompOp	—
sheafificationCompToSheaf 📖	CompOp	—
sheafificationHomEquiv 📖	CompOp	4 math math: toSheaf_map_sheafificationHomEquiv_symm, sheafificationAdjunction_homEquiv_apply, toPresheaf_map_sheafificationHomEquiv_def, toPresheaf_map_sheafificationHomEquiv

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
instIsLeftAdjointSheafOfModulesSheafification 📖	mathematical	—	CategoryTheory.Functor.IsLeftAdjoint PresheafOfModules instCategory SheafOfModules SheafOfModules.instCategory sheafification	—	CategoryTheory.Adjunction.isLeftAdjoint
instPreservesFiniteLimitsSheafAddCommGrpCatCompSheafOfModulesSheafificationToSheaf 📖	mathematical	—	CategoryTheory.Limits.PreservesFiniteLimits PresheafOfModules instCategory CategoryTheory.Sheaf AddCommGrpCat AddCommGrpCat.instCategory CategoryTheory.Sheaf.instCategorySheaf CategoryTheory.Functor.comp SheafOfModules SheafOfModules.instCategory sheafification CategoryTheory.instHasWeakSheafifyOfHasSheafify SheafOfModules.toSheaf	—	CategoryTheory.Limits.comp_preservesFiniteLimits CategoryTheory.instHasWeakSheafifyOfHasSheafify toPresheaf_preservesFiniteLimits CategoryTheory.instPreservesFiniteLimitsFunctorOppositeSheafPresheafToSheaf
instPreservesFiniteLimitsSheafOfModulesSheafification 📖	mathematical	—	CategoryTheory.Limits.PreservesFiniteLimits PresheafOfModules instCategory SheafOfModules SheafOfModules.instCategory sheafification CategoryTheory.instHasWeakSheafifyOfHasSheafify AddCommGrpCat AddCommGrpCat.instCategory	—	CategoryTheory.Limits.preservesFiniteLimits_of_reflects_of_preserves CategoryTheory.instHasWeakSheafifyOfHasSheafify instPreservesFiniteLimitsSheafAddCommGrpCatCompSheafOfModulesSheafificationToSheaf instReflectsFiniteLimitsSheafOfModulesSheafAddCommGrpCatToSheaf
instReflectsFiniteLimitsSheafOfModulesSheafAddCommGrpCatToSheaf 📖	mathematical	—	CategoryTheory.Limits.ReflectsFiniteLimits SheafOfModules SheafOfModules.instCategory CategoryTheory.Sheaf AddCommGrpCat AddCommGrpCat.instCategory CategoryTheory.Sheaf.instCategorySheaf SheafOfModules.toSheaf	—	CategoryTheory.Limits.ReflectsFiniteLimits.reflects CategoryTheory.Limits.reflectsFiniteLimits_of_reflectsIsomorphisms instReflectsIsomorphismsSheafOfModulesSheafAddCommGrpCatToSheaf SheafOfModules.Finite.hasFiniteLimits SheafOfModules.instPreservesFiniteLimitsSheafAddCommGrpCatToSheaf
instReflectsIsomorphismsSheafOfModulesFunctorOppositeAddCommGrpCatCompSheafToSheafSheafToPresheaf 📖	mathematical	—	CategoryTheory.Functor.ReflectsIsomorphisms SheafOfModules SheafOfModules.instCategory CategoryTheory.Functor Opposite CategoryTheory.Category.opposite AddCommGrpCat AddCommGrpCat.instCategory CategoryTheory.Functor.category CategoryTheory.Functor.comp CategoryTheory.Sheaf CategoryTheory.Sheaf.instCategorySheaf SheafOfModules.toSheaf CategoryTheory.sheafToPresheaf	—	CategoryTheory.reflectsIsomorphisms_comp SheafOfModules.instReflectsIsomorphismsPresheafOfModulesValRingCatForget CategoryTheory.reflectsIsomorphisms_of_reflectsMonomorphisms_of_reflectsEpimorphisms CategoryTheory.balanced_of_strongMonoCategory CategoryTheory.strongMonoCategory_of_regularMonoCategory CategoryTheory.regularMonoCategoryOfNormalMonoCategory instIsNormalMonoCategory CategoryTheory.Functor.reflectsMonomorphisms_of_faithful instFaithfulFunctorOppositeAbToPresheaf CategoryTheory.Functor.reflectsEpimorphisms_of_faithful
instReflectsIsomorphismsSheafOfModulesSheafAddCommGrpCatToSheaf 📖	mathematical	—	CategoryTheory.Functor.ReflectsIsomorphisms SheafOfModules SheafOfModules.instCategory CategoryTheory.Sheaf AddCommGrpCat AddCommGrpCat.instCategory CategoryTheory.Sheaf.instCategorySheaf SheafOfModules.toSheaf	—	CategoryTheory.reflectsIsomorphisms_of_comp instReflectsIsomorphismsSheafOfModulesFunctorOppositeAddCommGrpCatCompSheafToSheafSheafToPresheaf
sheafificationAdjunction_homEquiv_apply 📖	mathematical	—	DFunLike.coe Equiv Quiver.Hom SheafOfModules CategoryTheory.CategoryStruct.toQuiver CategoryTheory.Category.toCategoryStruct SheafOfModules.instCategory CategoryTheory.Functor.obj PresheafOfModules instCategory sheafification CategoryTheory.Functor.comp CategoryTheory.Sheaf.val RingCat RingCat.instCategory SheafOfModules.forget restrictScalars EquivLike.toFunLike Equiv.instEquivLike CategoryTheory.Adjunction.homEquiv sheafificationAdjunction sheafificationHomEquiv	—	—
sheafification_map 📖	mathematical	—	CategoryTheory.Functor.map PresheafOfModules instCategory SheafOfModules SheafOfModules.instCategory sheafification sheafifyMap CategoryTheory.Functor.obj CategoryTheory.Functor Opposite CategoryTheory.Category.opposite Ab AddCommGrpCat.instCategory CategoryTheory.Functor.category CategoryTheory.Sheaf CategoryTheory.Sheaf.instCategorySheaf CategoryTheory.presheafToSheaf presheaf CategoryTheory.toSheafify AddCommGrpCat toPresheaf	—	—
toPresheaf_map_sheafificationAdjunction_unit_app 📖	mathematical	—	CategoryTheory.Functor.map PresheafOfModules instCategory CategoryTheory.Functor Opposite CategoryTheory.Category.opposite Ab AddCommGrpCat.instCategory CategoryTheory.Functor.category toPresheaf CategoryTheory.Functor.obj CategoryTheory.Functor.id CategoryTheory.Functor.comp SheafOfModules SheafOfModules.instCategory sheafification CategoryTheory.Sheaf.val RingCat RingCat.instCategory SheafOfModules.forget restrictScalars CategoryTheory.NatTrans.app CategoryTheory.Adjunction.unit sheafificationAdjunction CategoryTheory.toSheafify presheaf	—	—
toPresheaf_map_sheafificationHomEquiv 📖	mathematical	—	CategoryTheory.Functor.map PresheafOfModules instCategory CategoryTheory.Functor Opposite CategoryTheory.Category.opposite Ab AddCommGrpCat.instCategory CategoryTheory.Functor.category toPresheaf CategoryTheory.Functor.obj CategoryTheory.Sheaf.val RingCat RingCat.instCategory restrictScalars SheafOfModules SheafOfModules.instCategory SheafOfModules.forget DFunLike.coe Equiv Quiver.Hom CategoryTheory.CategoryStruct.toQuiver CategoryTheory.Category.toCategoryStruct sheafification EquivLike.toFunLike Equiv.instEquivLike sheafificationHomEquiv CategoryTheory.Sheaf AddCommGrpCat CategoryTheory.Sheaf.instCategorySheaf CategoryTheory.presheafToSheaf presheaf SheafOfModules.toSheaf CategoryTheory.sheafToPresheaf CategoryTheory.Adjunction.homEquiv CategoryTheory.sheafificationAdjunction	—	toPresheaf_map_sheafificationHomEquiv_def CategoryTheory.Adjunction.homEquiv_unit
toPresheaf_map_sheafificationHomEquiv_def 📖	mathematical	—	CategoryTheory.Functor.map PresheafOfModules instCategory CategoryTheory.Functor Opposite CategoryTheory.Category.opposite Ab AddCommGrpCat.instCategory CategoryTheory.Functor.category toPresheaf CategoryTheory.Functor.obj CategoryTheory.Sheaf.val RingCat RingCat.instCategory restrictScalars SheafOfModules SheafOfModules.instCategory SheafOfModules.forget DFunLike.coe Equiv Quiver.Hom CategoryTheory.CategoryStruct.toQuiver CategoryTheory.Category.toCategoryStruct sheafification EquivLike.toFunLike Equiv.instEquivLike sheafificationHomEquiv CategoryTheory.CategoryStruct.comp presheaf CategoryTheory.sheafify SheafOfModules.val CategoryTheory.toSheafify SheafOfModules.Hom.val	—	—
toSheaf_map_sheafificationHomEquiv_symm 📖	mathematical	—	CategoryTheory.Functor.map SheafOfModules SheafOfModules.instCategory CategoryTheory.Sheaf AddCommGrpCat AddCommGrpCat.instCategory CategoryTheory.Sheaf.instCategorySheaf SheafOfModules.toSheaf CategoryTheory.Functor.obj PresheafOfModules instCategory sheafification DFunLike.coe Equiv Quiver.Hom CategoryTheory.CategoryStruct.toQuiver CategoryTheory.Category.toCategoryStruct CategoryTheory.Sheaf.val RingCat RingCat.instCategory restrictScalars SheafOfModules.forget EquivLike.toFunLike Equiv.instEquivLike Equiv.symm sheafificationHomEquiv CategoryTheory.Functor Opposite CategoryTheory.Category.opposite CategoryTheory.Functor.category presheaf CategoryTheory.sheafToPresheaf CategoryTheory.presheafToSheaf CategoryTheory.Adjunction.homEquiv CategoryTheory.sheafificationAdjunction Ab toPresheaf	—	Equiv.surjective Equiv.injective Equiv.apply_symm_apply CategoryTheory.Adjunction.homEquiv_unit Equiv.symm_apply_apply

---

← Back to Index