Considering a module as over a quotient ring

Stream: Is there code for X?

[Brendan Seamas Murphy]

If $B = A/I$ then the underlying additive group of any $A$-module annihilated by $I$ acquires a $B$-module structure (whose restriction of scalars is the original module). Is this construction already in mathlib? In particular I would like to view $M/IM$ as a $A/I$-module. Extension of scalars is in mathlib but when working with elements it can be convenient to keep the original underlying type instead of tensoring.

If this is not in mathlib (as I suspect), how would people feel about the $A/I$-module structure on $M/IM$ being added as a scoped instance? The use case I have in mind is for writing down an induction principle of regular sequences. The "naive" one involves successive quotienting by regular elements but keeping the same ring, but sometimes we want a more refined version where the motive depends on both the module and the ring it's over (eg if $M$ starts out as free then $M/xM$ is still free over $A/x$ but not over $A$, and sometimes we want to propogate this)

[Johan Commelin]

A scoped instance is certainly fine!

[Kevin Buzzard]

And definitely +1 from me for regular sequences!

[Markus Himmel]

Are docs#Module.IsTorsionBySet.module and docs#Module.instModuleQuotientIdealToSemiringToCommSemiringInstHasQuotientIdealToSemiringToCommSemiringQuotientSubmoduleToAddCommMonoidHasQuotientToRingHSMulInstHSMulHasSMul'TopInstTopSubmoduleCommRingAddCommGroup what you are looking for?

[Brendan Seamas Murphy]

Yes! Thanks so much

[Brendan Seamas Murphy]

Kevin Buzzard said:

And definitely +1 from me for regular sequences!

The first checkpoint/goal I have in mind for the patching stuff is the Auslander-Buchsbaum formula

[Kevin Buzzard]

I need pd_R(S)+depth_R(S)=depth_R(R) for the modularity lifting theorem in the route to FLT I'm taking (here R is noetherian local). This was needed in a post-Wiles optimisation of the argument by Diamond.

[Brendan Seamas Murphy]

Oh great

[Brendan Seamas Murphy]

I will be adding a dependence on the derived categories branch for regular sequence/depth stuff, but that should be merged soon?

[Ruben Van de Velde]

Do we want some way to track PRs on the way to FLT?

[Kevin Buzzard]

It might be a better idea to track the PRs which are unnecessary for FLT.

[Yaël Dillies]

You mean my PRs :neutral:

[Kevin Buzzard]

Your PRs which rearrange the library are I'm sure very helpful for FLT! The combi ones perhaps less so :-)