Categorical constructions for IsSMulRegular

theorem LinearMap.exact_lsmul_mkQ_smul_top {R : Type u} [CommRing R] (M : Type v) [AddCommGroup M] [Module R M] (r : R) : Function.Exact ⇑((lsmul R M) r) ⇑(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.

Equations

• M.smulShortComplex r = ModuleCat.shortComplexOfCompEqZero ((LinearMap.lsmul R ↑M) r) (r • ⊤).mkQ ⋯

@[simp]

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

@[simp]

theorem ModuleCat.smulShortComplex_g_hom_apply {R : Type u} [CommRing R] (M : ModuleCat R) (r : R) (a✝ : ↑M) : (Hom.hom (M.smulShortComplex r).g) a✝ = Submodule.Quotient.mk a✝

@[simp]

theorem ModuleCat.smulShortComplex_f_hom_apply {R : Type u} [CommRing R] (M : ModuleCat R) (r : R) (x2✝ : ↑M) : (Hom.hom (M.smulShortComplex r).f) x2✝ = r • x2✝

@[simp]

theorem ModuleCat.smulShortComplex_X₁_carrier {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₃ = (↑M ⧸ r • ⊤)

@[simp]

theorem ModuleCat.smulShortComplex_f_eq_smul_id {R : Type u} [CommRing R] (M : ModuleCat R) (r : R) : (M.smulShortComplex r).f = r • CategoryTheory.CategoryStruct.id M

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