Presentation of the restriction of scalars of a module

Given a morphism of rings A → B and a B-module M, we obtain a presentation of M as a A-module from a presentation of M as B-module, a presentation of B as a A-module (and some additional data).

TODO

• deduce that if B is a finitely presented as an A-module and M is finitely presented as an B-module, then M is finitely presented as an A-module

@[reducible, inline]

abbrev Module.Presentation.RestrictScalarsData {B : Type u_1} [Ring B] {M : Type u_2} [AddCommGroup M] [Module B M] [DecidableEq B] (presM : Module.Presentation B M) [DecidableEq presM.G] {A : Type u_3} [CommRing A] [Algebra A B] (presB : Module.Presentation A B) : Type (max (max (max u_3 u_6) u_4) u_6 u_5)

The additional data that is necessary in order to obtain a presentation of the restriction of scalars of a module.

Equations

• presM.RestrictScalarsData presB = (presB.finsupp presM.G).CokernelData (↑A presM.map) fun (x : presB.G × presM.R) => match x with | (g, g') => presB.var g • Finsupp.single g' 1

noncomputable def Module.Presentation.restrictScalars {B : Type u_1} [Ring B] {M : Type u_2} [AddCommGroup M] [Module B M] [DecidableEq B] (presM : Module.Presentation B M) [DecidableEq presM.G] {A : Type u_3} [CommRing A] [Algebra A B] [Module A M] [IsScalarTower A B M] (presB : Module.Presentation A B) (data : presM.RestrictScalarsData presB) : Module.Presentation A M

A presentation of the restriction of scalars from B to A of a B-module M, given a presentation of M as a B-module, a presentation of B as an A-module, and an additional data.

Equations

• presM.restrictScalars presB data = (presB.finsupp presM.G).ofExact data ⋯ ⋯ ⋯