Categorical constructions for IsSMulRegular

theorem LinearMap.exact_smul_id_smul_top_mkQ {R : Type u} [CommRing R] (M : Type v) [AddCommGroup M] [Module R M] (r : R) : Function.Exact ⇑(r • id) ⇑(r • ⊤).mkQ

def ModuleCat.smulShortComplex {R : Type u} [CommRing R] (M : ModuleCat R) (r : R) : CategoryTheory.ShortComplex (ModuleCat R)

The short (exact) complex M → M → M⧸xM obtain from the scalar multiple of x : R on M.

@[simp]

theorem ModuleCat.smulShortComplex_X₂ {R : Type u} [CommRing R] (M : ModuleCat R) (r : R) : (M.smulShortComplex r).X₂ = M

@[simp]

theorem ModuleCat.smulShortComplex_X₃_carrier {R : Type u} [CommRing R] (M : ModuleCat R) (r : R) : ↑(M.smulShortComplex r).X₃ = QuotSMulTop r ↑M

@[simp]

theorem ModuleCat.smulShortComplex_f {R : Type u} [CommRing R] (M : ModuleCat R) (r : R) : (M.smulShortComplex r).f = ofHom (r • LinearMap.id)

@[simp]

theorem ModuleCat.smulShortComplex_X₃_isModule {R : Type u} [CommRing R] (M : ModuleCat R) (r : R) : (M.smulShortComplex r).X₃.isModule = Submodule.Quotient.module (r • ⊤)

@[simp]

theorem ModuleCat.smulShortComplex_X₁ {R : Type u} [CommRing R] (M : ModuleCat R) (r : R) : (M.smulShortComplex r).X₁ = M

@[simp]

theorem ModuleCat.smulShortComplex_g {R : Type u} [CommRing R] (M : ModuleCat R) (r : R) : (M.smulShortComplex r).g = ofHom (r • ⊤).mkQ

@[simp]

theorem ModuleCat.smulShortComplex_X₃_isAddCommGroup {R : Type u} [CommRing R] (M : ModuleCat R) (r : R) : (M.smulShortComplex r).X₃.isAddCommGroup = Submodule.Quotient.addCommGroup (r • ⊤)

theorem ModuleCat.smulShortComplex_exact {R : Type u} [CommRing R] (M : ModuleCat R) (r : R) : (M.smulShortComplex r).Exact

instance ModuleCat.smulShortComplex_g_epi {R : Type u} [CommRing R] (M : ModuleCat R) (r : R) : CategoryTheory.Epi (M.smulShortComplex r).g

theorem IsSMulRegular.smulShortComplex_shortExact {R : Type u} [CommRing R] {M : ModuleCat R} {r : R} (reg : IsSMulRegular (↑M) r) : (M.smulShortComplex r).ShortExact