ChangeOfRings

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

Statistics

Metric	Count
Definitions restrictScalars, restrictScalarsCompToPresheaf, restrictScalarsObj	3
Theorems instAdditiveRestrictScalars, instFaithfulRestrictScalars, instFullRestrictScalarsIdFunctorOppositeRingCat, restrictScalarsObj_map, restrictScalarsObj_obj, restrictScalars_map_app, restrictScalars_obj	7
Total	10

PresheafOfModules

Definitions

Name	Category	Theorems
restrictScalars 📖	CompOp	18 math math: instAdditiveRestrictScalars, instIsLocallySurjectiveToSheafify, restrictScalars_map_app, toSheafify_app_apply', toPresheaf_map_toSheafify, SheafOfModules.restrictScalars_obj_val, toSheaf_map_sheafificationHomEquiv_symm, SheafOfModules.restrictScalars_map_val, restrictScalars_obj, instFaithfulRestrictScalars, comp_toPresheaf_map_sheafifyHomEquiv'_symm_hom, sheafificationAdjunction_homEquiv_apply, toPresheaf_map_sheafificationAdjunction_unit_app, instIsLocallyInjectiveToSheafify, toPresheaf_map_sheafificationHomEquiv_def, instFullRestrictScalarsIdFunctorOppositeRingCat, toSheafify_app_apply, toPresheaf_map_sheafificationHomEquiv
restrictScalarsCompToPresheaf 📖	CompOp	—
restrictScalarsObj 📖	CompOp	4 math math: restrictScalars_map_app, restrictScalarsObj_map, restrictScalarsObj_obj, restrictScalars_obj

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
instAdditiveRestrictScalars 📖	mathematical	—	CategoryTheory.Functor.Additive PresheafOfModules instCategory instPreadditive restrictScalars	—	—
instFaithfulRestrictScalars 📖	mathematical	—	CategoryTheory.Functor.Faithful PresheafOfModules instCategory restrictScalars	—	CategoryTheory.Functor.map_injective instFaithfulFunctorOppositeAbToPresheaf CategoryTheory.Functor.congr_map
instFullRestrictScalarsIdFunctorOppositeRingCat 📖	mathematical	—	CategoryTheory.Functor.Full PresheafOfModules instCategory restrictScalars CategoryTheory.CategoryStruct.id CategoryTheory.Functor Opposite CategoryTheory.Category.opposite RingCat RingCat.instCategory CategoryTheory.Category.toCategoryStruct CategoryTheory.Functor.category	—	CategoryTheory.Functor.Full.id
restrictScalarsObj_map 📖	mathematical	—	map restrictScalarsObj ModuleCat.ofHom RingCat.carrier CategoryTheory.Functor.obj Opposite CategoryTheory.Category.opposite RingCat RingCat.instCategory RingCat.ring ModuleCat.carrier ModuleCat ModuleCat.moduleCategory ModuleCat.restrictScalars RingCat.Hom.hom CategoryTheory.NatTrans.app obj CategoryTheory.Functor.map ModuleCat.isAddCommGroup Module.compHom Ring.toSemiring AddCommGroup.toAddCommMonoid ModuleCat.isModule RingHom.id Semiring.toNonAssocSemiring AddCommMagma.toAdd AddCommSemigroup.toAddCommMagma AddCommMonoid.toAddCommSemigroup DFunLike.coe CategoryTheory.ConcreteCategory.hom LinearMap LinearMap.instFunLike ModuleCat.instConcreteCategoryLinearMapIdCarrier	—	—
restrictScalarsObj_obj 📖	mathematical	—	obj restrictScalarsObj CategoryTheory.Functor.obj ModuleCat RingCat.carrier Opposite CategoryTheory.Category.opposite RingCat RingCat.instCategory RingCat.ring ModuleCat.moduleCategory ModuleCat.restrictScalars RingCat.Hom.hom CategoryTheory.NatTrans.app	—	—
restrictScalars_map_app 📖	mathematical	—	Hom.app restrictScalarsObj CategoryTheory.Functor.map PresheafOfModules instCategory restrictScalars ModuleCat RingCat.carrier CategoryTheory.Functor.obj Opposite CategoryTheory.Category.opposite RingCat RingCat.instCategory RingCat.ring ModuleCat.moduleCategory ModuleCat.restrictScalars RingCat.Hom.hom CategoryTheory.NatTrans.app obj	—	—
restrictScalars_obj 📖	mathematical	—	CategoryTheory.Functor.obj PresheafOfModules instCategory restrictScalars restrictScalarsObj	—	—

---

← Back to Index