Freeness of QuotSMulTop by a regular element #
Let M be a finitely presented module over a commutative ring R. If x is in the
Jacobson radical of R and x is M-regular, then M/xM is free over R/(x) if and only if
M is free over R.
instance
instFreeQuotientIdealSpanSingletonSetQuotSMulTop
(R : Type u_1)
[CommRing R]
(M : Type u_2)
[AddCommGroup M]
[Module R M]
[Module.Free R M]
(x : R)
:
Module.Free (R ⧸ Ideal.span {x}) (QuotSMulTop x M)
theorem
Module.free_quotSMulTop_iff_free
(R : Type u_1)
[CommRing R]
(M : Type u_2)
[AddCommGroup M]
[Module R M]
[FinitePresentation R M]
{x : R}
(mem : x ∈ ⊥.jacobson)
(reg : IsSMulRegular M x)
: