ChangeOfRings

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

Statistics

Metric	Count
Definitions restrictHomEquivOfIsLocallySurjective, restrictScalars	2
Theorems instAdditiveRestrictScalars, restrictScalars_map_val, restrictScalars_obj_val	3
Total	5

PresheafOfModules

Definitions

Name	Category	Theorems
restrictHomEquivOfIsLocallySurjective 📖	CompOp	—

SheafOfModules

Definitions

Name	Category	Theorems
restrictScalars 📖	CompOp	3 math math: instAdditiveRestrictScalars, restrictScalars_obj_val, restrictScalars_map_val

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
instAdditiveRestrictScalars 📖	mathematical	—	CategoryTheory.Functor.Additive SheafOfModules instCategory instPreadditive restrictScalars	—	—
restrictScalars_map_val 📖	mathematical	—	Hom.val CategoryTheory.Functor.obj PresheafOfModules CategoryTheory.Sheaf.val RingCat RingCat.instCategory PresheafOfModules.instCategory PresheafOfModules.restrictScalars CategoryTheory.Sheaf.Hom.val val isSheaf CategoryTheory.Functor.map SheafOfModules instCategory restrictScalars	—	isSheaf
restrictScalars_obj_val 📖	mathematical	—	val CategoryTheory.Functor.obj SheafOfModules instCategory restrictScalars PresheafOfModules CategoryTheory.Sheaf.val RingCat RingCat.instCategory PresheafOfModules.instCategory PresheafOfModules.restrictScalars CategoryTheory.Sheaf.Hom.val	—	—

---

← Back to Index