Freeness of QuotSMulTop by regular element

For finitely generated module M over Noetherian local ring (R, m), if x ∈ m is M-regular, M/xM is free over R/(x) iff M is free over R.

Main Results

• free_iff_quotSMulTop_free : If x ∈ m is M-regular, M/xM is free over R/(x) iff M is free over R.

theorem LinearMap.ker_mapRange_eq_smul_top (R : Type u) [CommRing R] (I : Type u_1) [Finite I] (x : R) : (Finsupp.mapRange.linearMap (Submodule.mkQ (Ideal.span {x}))).ker = x • ⊤

theorem free_iff_quotSMulTop_free (R : Type u) [CommRing R] [IsLocalRing R] [IsNoetherianRing R] (M : Type u_1) [AddCommGroup M] [Module R M] [Module.Finite R M] {x : R} (mem : x ∈ IsLocalRing.maximalIdeal R) (reg : IsSMulRegular M x) : Module.Free (R ⧸ Ideal.span {x}) (QuotSMulTop x M) ↔ Module.Free R M