Documentation

Mathlib.RingTheory.Regular.Category

Categorical constructions for IsSMulRegular #

source
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
source
@[deprecated LinearMap.exact_lsmul_mkQ_smul_top (since := "2026-04-13")]
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 ⇑((lsmul R M) r) ⇑(r • ⊤).mkQ

Alias of LinearMap.exact_lsmul_mkQ_smul_top.

source
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
Instances For
    source
    @[simp]
    theorem ModuleCat.smulShortComplex_X₃_carrier {R : Type u} [CommRing R] (M : ModuleCat R) (r : R) :
    ↑(M.smulShortComplex r).X₃ = (↑M ⧸ r • ⊤)
    source
    @[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✝
    source
    @[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✝
    source
    @[simp]
    theorem ModuleCat.smulShortComplex_X₂_carrier {R : Type u} [CommRing R] (M : ModuleCat R) (r : R) :
    ↑(M.smulShortComplex r).X₂ = ↑M
    source
    @[simp]
    theorem ModuleCat.smulShortComplex_X₁_carrier {R : Type u} [CommRing R] (M : ModuleCat R) (r : R) :
    ↑(M.smulShortComplex r).X₁ = ↑M
    source
    @[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
    source
    theorem ModuleCat.smulShortComplex_exact {R : Type u} [CommRing R] (M : ModuleCat R) (r : R) :
    (M.smulShortComplex r).Exact
    source
    instance ModuleCat.smulShortComplex_g_epi {R : Type u} [CommRing R] (M : ModuleCat R) (r : R) :
    CategoryTheory.Epi (M.smulShortComplex r).g
    source
    theorem IsSMulRegular.smulShortComplex_shortExact {R : Type u} [CommRing R] {M : ModuleCat R} {r : R} (reg : IsSMulRegular (↑M) r) :
    (M.smulShortComplex r).ShortExact