Commit 2024-12-20 15:50 b95ee76f

View on Github →

feat(Algebra/Category/ModuleCat): the pseudofunctors which send a ring to its category of modules (#18197) In this PR, we construct various pseudofunctors which send a (commutative) ring to its category of modules. Depending on the case, the functoriality is given by the restriction of scalars or by the extension of scalars.

Estimated changes

Modified Mathlib.lean

Modified Mathlib/Algebra/Category/ModuleCat/ChangeOfRings.lean

added theorem ModuleCat.ExtendScalars.hom_ext

added theorem ModuleCat.extendRestrictScalarsAdj_homEquiv_apply

added theorem ModuleCat.extendRestrictScalarsAdj_unit_app_apply

added theorem ModuleCat.extendScalarsComp_hom_app_one_tmul

added theorem ModuleCat.extendScalarsId_hom_app_one_tmul

added theorem ModuleCat.extendScalarsId_inv_app_apply

added theorem ModuleCat.extendScalars_assoc'

added theorem ModuleCat.extendScalars_assoc

added theorem ModuleCat.extendScalars_comp_id

added theorem ModuleCat.extendScalars_id_comp

added theorem ModuleCat.homEquiv_extendScalarsComp

added theorem ModuleCat.homEquiv_extendScalarsId

Created Mathlib/Algebra/Category/ModuleCat/Pseudofunctor.lean