Localization

📁 Source: Mathlib/Algebra/Category/ModuleCat/Sheaf/Localization.lean

Statistics

Metric	Count
Definitions	0
Theorems instIsLocalizationSheafOfModulesSheafificationInverseImageFunctorOppositeAbWToPresheaf, inverseImage_W_toPresheaf_eq_inverseImage_isomorphisms	2
Total	2

PresheafOfModules

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
instIsLocalizationSheafOfModulesSheafificationInverseImageFunctorOppositeAbWToPresheaf 📖	mathematical	—	CategoryTheory.Functor.IsLocalization PresheafOfModules SheafOfModules instCategory SheafOfModules.instCategory sheafification CategoryTheory.MorphismProperty.inverseImage CategoryTheory.Functor Opposite CategoryTheory.Category.opposite Ab AddCommGrpCat.instCategory CategoryTheory.Functor.category CategoryTheory.GrothendieckTopology.W toPresheaf	—	inverseImage_W_toPresheaf_eq_inverseImage_isomorphisms CategoryTheory.Adjunction.isLocalization instFullSheafOfModulesCompObjFunctorOppositeRingCatIsSheafForgetRestrictScalars instFaithfulSheafOfModulesCompObjFunctorOppositeRingCatIsSheafForgetRestrictScalars
inverseImage_W_toPresheaf_eq_inverseImage_isomorphisms 📖	mathematical	—	CategoryTheory.MorphismProperty.inverseImage PresheafOfModules instCategory CategoryTheory.Functor Opposite CategoryTheory.Category.opposite Ab AddCommGrpCat.instCategory CategoryTheory.Functor.category CategoryTheory.GrothendieckTopology.W toPresheaf SheafOfModules SheafOfModules.instCategory CategoryTheory.MorphismProperty.isomorphisms sheafification	—	CategoryTheory.GrothendieckTopology.W_eq_inverseImage_isomorphisms CategoryTheory.MorphismProperty.ext CategoryTheory.isIso_iff_of_reflects_iso instReflectsIsomorphismsSheafOfModulesSheafAddCommGrpCatToSheaf_1 CategoryTheory.MorphismProperty.arrow_mk_iso_iff CategoryTheory.MorphismProperty.RespectsIso.isomorphisms

---

← Back to Index