Regular sequences on modules of linear maps #
A regular element on a module N remains regular on M →ₗ[R] N. More generally, a weakly
regular sequence on N of length at most two remains weakly regular on M →ₗ[R] N.
No local-ring, Noetherian, or finiteness hypotheses are needed for these transfer results.
Main results #
IsSMulRegular.linearMap: a regular element remains regular on the module of linear maps.IsSMulRegular.quotSMulTop_linearMap: the second element remains regular after quotienting the module of linear maps by the first regular element.RingTheory.Sequence.IsWeaklyRegular.linearMap: weak regularity of sequences of length at most two passes from the target to the module of linear maps.
theorem
IsSMulRegular.linearMap
{R : Type u_1}
{M : Type u_2}
{N : Type u_3}
[CommSemiring R]
[AddCommMonoid M]
[AddCommMonoid N]
[Module R M]
[Module R N]
{scalar : R}
(regular : IsSMulRegular N scalar)
:
IsSMulRegular (M →ₗ[R] N) scalar
A regular element on the target is regular on the module of linear maps.
theorem
IsSMulRegular.quotSMulTop_linearMap
{R : Type u_1}
{M : Type u_2}
{N : Type u_3}
[CommRing R]
[AddCommGroup M]
[AddCommGroup N]
[Module R M]
[Module R N]
{first second : R}
(regular : IsSMulRegular N first)
(quotientRegular : IsSMulRegular (QuotSMulTop first N) second)
:
IsSMulRegular (QuotSMulTop first (M →ₗ[R] N)) second
The second element of a weakly regular pair on the target remains regular after quotienting the module of linear maps by the first element.
theorem
RingTheory.Sequence.IsWeaklyRegular.linearMap
{R : Type u_1}
{M : Type u_2}
{N : Type u_3}
[CommRing R]
[AddCommGroup M]
[AddCommGroup N]
[Module R M]
[Module R N]
{scalars : List R}
(regular : IsWeaklyRegular N scalars)
(length : scalars.length ≤ 2)
:
IsWeaklyRegular (M →ₗ[R] N) scalars
A weakly regular sequence of length at most two on the target is weakly regular on the module of linear maps.