Commit 2023-09-08 11:01 a17d250d

View on Github →

feat(Algebra/Category/ModuleCat): composition of restriction of scalar functors (#6915) This PR studies the behaviour of restriction of scalars functors with respect to composition.

Estimated changes

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

deleted def CategoryTheory.ModuleCat.CoextendScalars.map'

deleted theorem CategoryTheory.ModuleCat.CoextendScalars.map_apply

deleted def CategoryTheory.ModuleCat.CoextendScalars.obj'

deleted theorem CategoryTheory.ModuleCat.CoextendScalars.smul_apply'

deleted theorem CategoryTheory.ModuleCat.CoextendScalars.smul_apply

deleted def CategoryTheory.ModuleCat.ExtendRestrictScalarsAdj.Counit.map

deleted def CategoryTheory.ModuleCat.ExtendRestrictScalarsAdj.HomEquiv.evalAt

deleted def CategoryTheory.ModuleCat.ExtendRestrictScalarsAdj.HomEquiv.fromExtendScalars

deleted def CategoryTheory.ModuleCat.ExtendRestrictScalarsAdj.HomEquiv.toRestrictScalars

deleted def CategoryTheory.ModuleCat.ExtendRestrictScalarsAdj.Unit.map

deleted def CategoryTheory.ModuleCat.ExtendRestrictScalarsAdj.counit

deleted def CategoryTheory.ModuleCat.ExtendRestrictScalarsAdj.homEquiv

deleted def CategoryTheory.ModuleCat.ExtendRestrictScalarsAdj.unit

deleted def CategoryTheory.ModuleCat.ExtendScalars.map'

deleted theorem CategoryTheory.ModuleCat.ExtendScalars.map'_comp

deleted theorem CategoryTheory.ModuleCat.ExtendScalars.map'_id

deleted theorem CategoryTheory.ModuleCat.ExtendScalars.map_tmul

deleted def CategoryTheory.ModuleCat.ExtendScalars.obj'

deleted def CategoryTheory.ModuleCat.RestrictScalars.map'

deleted def CategoryTheory.ModuleCat.RestrictScalars.obj'

deleted def CategoryTheory.ModuleCat.RestrictionCoextensionAdj.HomEquiv.fromRestriction

deleted def CategoryTheory.ModuleCat.RestrictionCoextensionAdj.HomEquiv.toRestriction

deleted def CategoryTheory.ModuleCat.RestrictionCoextensionAdj.app'

deleted def CategoryTheory.ModuleCat.coextendScalars

deleted def CategoryTheory.ModuleCat.extendRestrictScalarsAdj

deleted def CategoryTheory.ModuleCat.extendScalars

deleted def CategoryTheory.ModuleCat.restrictCoextendScalarsAdj

deleted theorem CategoryTheory.ModuleCat.restrictScalars.map_apply

deleted theorem CategoryTheory.ModuleCat.restrictScalars.smul_def'

deleted theorem CategoryTheory.ModuleCat.restrictScalars.smul_def

deleted def CategoryTheory.ModuleCat.restrictScalars

added def ModuleCat.CoextendScalars.map'

added theorem ModuleCat.CoextendScalars.map_apply

added def ModuleCat.CoextendScalars.obj'

added theorem ModuleCat.CoextendScalars.smul_apply'

added theorem ModuleCat.CoextendScalars.smul_apply

added def ModuleCat.ExtendRestrictScalarsAdj.Counit.map

added def ModuleCat.ExtendRestrictScalarsAdj.HomEquiv.evalAt

added def ModuleCat.ExtendRestrictScalarsAdj.HomEquiv.fromExtendScalars

added def ModuleCat.ExtendRestrictScalarsAdj.HomEquiv.toRestrictScalars

added def ModuleCat.ExtendRestrictScalarsAdj.Unit.map

added def ModuleCat.ExtendRestrictScalarsAdj.counit

added def ModuleCat.ExtendRestrictScalarsAdj.homEquiv

added def ModuleCat.ExtendRestrictScalarsAdj.unit

added def ModuleCat.ExtendScalars.map'

added theorem ModuleCat.ExtendScalars.map'_comp

added theorem ModuleCat.ExtendScalars.map'_id

added theorem ModuleCat.ExtendScalars.map_tmul

added def ModuleCat.ExtendScalars.obj'

added def ModuleCat.RestrictScalars.map'

added def ModuleCat.RestrictScalars.obj'

added def ModuleCat.RestrictionCoextensionAdj.HomEquiv.fromRestriction

added def ModuleCat.RestrictionCoextensionAdj.HomEquiv.toRestriction

added def ModuleCat.RestrictionCoextensionAdj.app'

added def ModuleCat.coextendScalars

added def ModuleCat.extendRestrictScalarsAdj

added def ModuleCat.extendScalars

added def ModuleCat.restrictCoextendScalarsAdj

added theorem ModuleCat.restrictScalars.map_apply

added theorem ModuleCat.restrictScalars.smul_def'

added theorem ModuleCat.restrictScalars.smul_def

added def ModuleCat.restrictScalars

added def ModuleCat.restrictScalarsComp'

added theorem ModuleCat.restrictScalarsComp'_hom_apply

added theorem ModuleCat.restrictScalarsComp'_inv_apply

added def ModuleCat.restrictScalarsId'

added theorem ModuleCat.restrictScalarsId'_hom_apply

added theorem ModuleCat.restrictScalarsId'_inv_apply

added def ModuleCat.semilinearMapAddEquiv