Commit 2023-07-07 06:10 caec9984

View on Github →

feat: port Algebra.Category.Module.ChangeOfRings (#4300)

Estimated changes

Modified Mathlib.lean

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

added def CategoryTheory.ModuleCat.CoextendScalars.map'

added theorem CategoryTheory.ModuleCat.CoextendScalars.map_apply

added def CategoryTheory.ModuleCat.CoextendScalars.obj'

added theorem CategoryTheory.ModuleCat.CoextendScalars.smul_apply'

added theorem CategoryTheory.ModuleCat.CoextendScalars.smul_apply

added def CategoryTheory.ModuleCat.ExtendRestrictScalarsAdj.Counit.map

added def CategoryTheory.ModuleCat.ExtendRestrictScalarsAdj.HomEquiv.evalAt

added def CategoryTheory.ModuleCat.ExtendRestrictScalarsAdj.HomEquiv.fromExtendScalars

added def CategoryTheory.ModuleCat.ExtendRestrictScalarsAdj.HomEquiv.toRestrictScalars

added def CategoryTheory.ModuleCat.ExtendRestrictScalarsAdj.Unit.map

added def CategoryTheory.ModuleCat.ExtendRestrictScalarsAdj.counit

added def CategoryTheory.ModuleCat.ExtendRestrictScalarsAdj.homEquiv

added def CategoryTheory.ModuleCat.ExtendRestrictScalarsAdj.unit

added def CategoryTheory.ModuleCat.ExtendScalars.map'

added theorem CategoryTheory.ModuleCat.ExtendScalars.map'_comp

added theorem CategoryTheory.ModuleCat.ExtendScalars.map'_id

added theorem CategoryTheory.ModuleCat.ExtendScalars.map_tmul

added def CategoryTheory.ModuleCat.ExtendScalars.obj'

added def CategoryTheory.ModuleCat.RestrictScalars.map'

added def CategoryTheory.ModuleCat.RestrictScalars.obj'

added def CategoryTheory.ModuleCat.RestrictionCoextensionAdj.HomEquiv.fromRestriction

added def CategoryTheory.ModuleCat.RestrictionCoextensionAdj.HomEquiv.toRestriction

added def CategoryTheory.ModuleCat.RestrictionCoextensionAdj.app'

added def CategoryTheory.ModuleCat.coextendScalars

added def CategoryTheory.ModuleCat.extendRestrictScalarsAdj

added def CategoryTheory.ModuleCat.extendScalars

added def CategoryTheory.ModuleCat.restrictCoextendScalarsAdj

added theorem CategoryTheory.ModuleCat.restrictScalars.map_apply

added theorem CategoryTheory.ModuleCat.restrictScalars.smul_def'

added theorem CategoryTheory.ModuleCat.restrictScalars.smul_def

added def CategoryTheory.ModuleCat.restrictScalars