Theorems · Theorem · category theory

CategoryTheory.Abelian.Ext.postcomp_smul_id_mono_iff

∀ {R : Type u} [inst : CommRing R] [inst_1 : Small.{v, u} R] {M N : ModuleCat R} (r : R) (i : ℕ),
  CategoryTheory.Mono
      (AddCommGrpCat.ofHom ((CategoryTheory.Abelian.Ext.mk₀ (r • CategoryTheory.CategoryStruct.id M)).postcomp N ⋯)) ↔
    IsSMulRegular (CategoryTheory.Abelian.Ext N M i) r

r • 𝟙 M induces a monomorphism in Ext M N n if and only if scalar multiplication by r is faithful on Ext M N n.

Defined in

Mathlib.Algebra.Category.ModuleCat.Ext.Basic

Cited by

1 results in Mathlib

Foundations

Depth 121 from the axioms · uses propext, Classical.choice, Quot.sound

Assumes

CommRingSmall