Documentation Verification Report

Sheafification

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

Statistics

Metric	Count
Definitions `sheafification`, `sheafificationAdjunction`, `sheafificationCompForgetCompToPresheaf`, `sheafificationCompToSheaf`, `sheafificationHomEquiv`	5
Theorems `instFaithfulSheafOfModulesCompObjFunctorOppositeRingCatIsSheafForgetRestrictScalars`, `instFullSheafOfModulesCompObjFunctorOppositeRingCatIsSheafForgetRestrictScalars`, `instIsIsoFunctorSheafOfModulesCounitSheafificationAdjunction`, `instIsLeftAdjointSheafOfModulesSheafification`, `instPreservesFiniteLimitsSheafAddCommGrpCatCompSheafOfModulesSheafificationToSheaf`, `instPreservesFiniteLimitsSheafOfModulesSheafification`, `instReflectsFiniteLimitsSheafOfModulesSheafAddCommGrpCatToSheaf`, `instReflectsIsomorphismsSheafOfModulesSheafAddCommGrpCatToSheaf`, `instReflectsIsomorphismsSheafOfModulesSheafAddCommGrpCatToSheaf_1`, `sheafificationAdjunction_homEquiv_apply`, `sheafification_map`, `toPresheaf_map_sheafificationAdjunction_unit_app`, `toPresheaf_map_sheafificationHomEquiv`, `toPresheaf_map_sheafificationHomEquiv_def`, `toSheaf_map_sheafificationAdjunction_counit_app`, `toSheaf_map_sheafificationHomEquiv_symm`	16
Total	21

PresheafOfModules

Definitions

Name	Category	Theorems
`sheafification` 📖	CompOp	13 math math: `instIsLeftAdjointSheafOfModulesSheafification`, `toSheaf_map_sheafificationAdjunction_counit_app`, `sheafification_map`, `toSheaf_map_sheafificationHomEquiv_symm`, `instIsIsoFunctorSheafOfModulesCounitSheafificationAdjunction`, `inverseImage_W_toPresheaf_eq_inverseImage_isomorphisms`, `instIsLocalizationSheafOfModulesSheafificationInverseImageFunctorOppositeAbWToPresheaf`, `sheafificationAdjunction_homEquiv_apply`, `toPresheaf_map_sheafificationAdjunction_unit_app`, `toPresheaf_map_sheafificationHomEquiv_def`, `toPresheaf_map_sheafificationHomEquiv`, `instPreservesFiniteLimitsSheafOfModulesSheafification`, `instPreservesFiniteLimitsSheafAddCommGrpCatCompSheafOfModulesSheafificationToSheaf`
`sheafificationAdjunction` 📖	CompOp	4 math math: `toSheaf_map_sheafificationAdjunction_counit_app`, `instIsIsoFunctorSheafOfModulesCounitSheafificationAdjunction`, `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
`instFaithfulSheafOfModulesCompObjFunctorOppositeRingCatIsSheafForgetRestrictScalars` 📖	mathematical	—	`CategoryTheory.Functor.Faithful` `SheafOfModules` `SheafOfModules.instCategory` `PresheafOfModules` `instCategory` `CategoryTheory.Functor.comp` `CategoryTheory.ObjectProperty.FullSubcategory.obj` `CategoryTheory.Functor` `Opposite` `CategoryTheory.Category.opposite` `RingCat` `RingCat.instCategory` `CategoryTheory.Functor.category` `CategoryTheory.Presheaf.IsSheaf` `SheafOfModules.forget` `restrictScalars`	—	`CategoryTheory.Functor.FullyFaithful.faithful` `instIsIsoFunctorSheafOfModulesCounitSheafificationAdjunction`
`instFullSheafOfModulesCompObjFunctorOppositeRingCatIsSheafForgetRestrictScalars` 📖	mathematical	—	`CategoryTheory.Functor.Full` `SheafOfModules` `SheafOfModules.instCategory` `PresheafOfModules` `instCategory` `CategoryTheory.Functor.comp` `CategoryTheory.ObjectProperty.FullSubcategory.obj` `CategoryTheory.Functor` `Opposite` `CategoryTheory.Category.opposite` `RingCat` `RingCat.instCategory` `CategoryTheory.Functor.category` `CategoryTheory.Presheaf.IsSheaf` `SheafOfModules.forget` `restrictScalars`	—	`CategoryTheory.Functor.FullyFaithful.full` `instIsIsoFunctorSheafOfModulesCounitSheafificationAdjunction`
`instIsIsoFunctorSheafOfModulesCounitSheafificationAdjunction` 📖	mathematical	—	`CategoryTheory.IsIso` `CategoryTheory.Functor` `SheafOfModules` `SheafOfModules.instCategory` `CategoryTheory.Functor.category` `CategoryTheory.Functor.comp` `PresheafOfModules` `instCategory` `CategoryTheory.ObjectProperty.FullSubcategory.obj` `Opposite` `CategoryTheory.Category.opposite` `RingCat` `RingCat.instCategory` `CategoryTheory.Presheaf.IsSheaf` `SheafOfModules.forget` `restrictScalars` `sheafification` `CategoryTheory.Functor.id` `CategoryTheory.Adjunction.counit` `sheafificationAdjunction`	—	`CategoryTheory.NatTrans.isIso_iff_isIso_app` `CategoryTheory.isIso_iff_of_reflects_iso` `instReflectsIsomorphismsSheafOfModulesSheafAddCommGrpCatToSheaf` `toSheaf_map_sheafificationAdjunction_counit_app` `CategoryTheory.isIso_sheafificationAdjunction_counit`
`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.ObjectProperty.FullSubcategory.category` `CategoryTheory.Functor` `Opposite` `CategoryTheory.Category.opposite` `CategoryTheory.Functor.category` `CategoryTheory.Presheaf.IsSheaf` `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.ObjectProperty.FullSubcategory.category` `CategoryTheory.Functor` `Opposite` `CategoryTheory.Category.opposite` `CategoryTheory.Functor.category` `CategoryTheory.Presheaf.IsSheaf` `SheafOfModules.toSheaf`	—	`CategoryTheory.Limits.ReflectsFiniteLimits.reflects` `CategoryTheory.Limits.reflectsFiniteLimits_of_reflectsIsomorphisms` `instReflectsIsomorphismsSheafOfModulesSheafAddCommGrpCatToSheaf_1` `SheafOfModules.Finite.hasFiniteLimits` `SheafOfModules.instPreservesFiniteLimitsSheafAddCommGrpCatToSheaf`
`instReflectsIsomorphismsSheafOfModulesSheafAddCommGrpCatToSheaf` 📖	mathematical	—	`CategoryTheory.Functor.ReflectsIsomorphisms` `SheafOfModules` `SheafOfModules.instCategory` `CategoryTheory.Sheaf` `AddCommGrpCat` `AddCommGrpCat.instCategory` `CategoryTheory.ObjectProperty.FullSubcategory.category` `CategoryTheory.Functor` `Opposite` `CategoryTheory.Category.opposite` `CategoryTheory.Functor.category` `CategoryTheory.Presheaf.IsSheaf` `SheafOfModules.toSheaf`	—	`CategoryTheory.reflectsIsomorphisms_of_comp`
`instReflectsIsomorphismsSheafOfModulesSheafAddCommGrpCatToSheaf_1` 📖	mathematical	—	`CategoryTheory.Functor.ReflectsIsomorphisms` `SheafOfModules` `SheafOfModules.instCategory` `CategoryTheory.Sheaf` `AddCommGrpCat` `AddCommGrpCat.instCategory` `CategoryTheory.ObjectProperty.FullSubcategory.category` `CategoryTheory.Functor` `Opposite` `CategoryTheory.Category.opposite` `CategoryTheory.Functor.category` `CategoryTheory.Presheaf.IsSheaf` `SheafOfModules.toSheaf`	—	`CategoryTheory.reflectsIsomorphisms_of_comp` `CategoryTheory.reflectsIsomorphisms_comp` `instReflectsIsomorphismsSheafOfModulesSheafAddCommGrpCatToSheaf` `CategoryTheory.reflectsIsomorphisms_of_full_and_faithful` `CategoryTheory.ObjectProperty.full_ι` `CategoryTheory.ObjectProperty.faithful_ι`
`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.ObjectProperty.FullSubcategory.obj` `CategoryTheory.Functor` `Opposite` `CategoryTheory.Category.opposite` `RingCat` `RingCat.instCategory` `CategoryTheory.Functor.category` `CategoryTheory.Presheaf.IsSheaf` `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.ObjectProperty.FullSubcategory.category` `CategoryTheory.Presheaf.IsSheaf` `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.ObjectProperty.FullSubcategory.obj` `RingCat` `RingCat.instCategory` `CategoryTheory.Presheaf.IsSheaf` `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.ObjectProperty.FullSubcategory.obj` `RingCat` `RingCat.instCategory` `CategoryTheory.Presheaf.IsSheaf` `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.ObjectProperty.FullSubcategory.category` `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.ObjectProperty.FullSubcategory.obj` `RingCat` `RingCat.instCategory` `CategoryTheory.Presheaf.IsSheaf` `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_sheafificationAdjunction_counit_app` 📖	mathematical	—	`CategoryTheory.Functor.map` `SheafOfModules` `SheafOfModules.instCategory` `CategoryTheory.Sheaf` `AddCommGrpCat` `AddCommGrpCat.instCategory` `CategoryTheory.ObjectProperty.FullSubcategory.category` `CategoryTheory.Functor` `Opposite` `CategoryTheory.Category.opposite` `CategoryTheory.Functor.category` `CategoryTheory.Presheaf.IsSheaf` `SheafOfModules.toSheaf` `CategoryTheory.Functor.obj` `CategoryTheory.Functor.comp` `PresheafOfModules` `instCategory` `CategoryTheory.ObjectProperty.FullSubcategory.obj` `RingCat` `RingCat.instCategory` `SheafOfModules.forget` `restrictScalars` `sheafification` `CategoryTheory.Functor.id` `CategoryTheory.NatTrans.app` `CategoryTheory.Adjunction.counit` `sheafificationAdjunction` `CategoryTheory.sheafToPresheaf` `CategoryTheory.presheafToSheaf` `CategoryTheory.sheafificationAdjunction`	—	`toSheaf_map_sheafificationHomEquiv_symm` `CategoryTheory.Adjunction.homEquiv_symm_id`
`toSheaf_map_sheafificationHomEquiv_symm` 📖	mathematical	—	`CategoryTheory.Functor.map` `SheafOfModules` `SheafOfModules.instCategory` `CategoryTheory.Sheaf` `AddCommGrpCat` `AddCommGrpCat.instCategory` `CategoryTheory.ObjectProperty.FullSubcategory.category` `CategoryTheory.Functor` `Opposite` `CategoryTheory.Category.opposite` `CategoryTheory.Functor.category` `CategoryTheory.Presheaf.IsSheaf` `SheafOfModules.toSheaf` `CategoryTheory.Functor.obj` `PresheafOfModules` `instCategory` `sheafification` `DFunLike.coe` `Equiv` `Quiver.Hom` `CategoryTheory.CategoryStruct.toQuiver` `CategoryTheory.Category.toCategoryStruct` `CategoryTheory.ObjectProperty.FullSubcategory.obj` `RingCat` `RingCat.instCategory` `restrictScalars` `SheafOfModules.forget` `EquivLike.toFunLike` `Equiv.instEquivLike` `Equiv.symm` `sheafificationHomEquiv` `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