Some basic lemmas for manipulating Ext over ModuleCat

theorem CategoryTheory.Abelian.Ext.postcomp_smul_id_eq_zero_of_mem_annihilator {R : Type u} [CommRing R] [Small.{v, u} R] {M N : ModuleCat R} {r : R} (mem_ann : r ∈ Module.annihilator R ↑N) (n : ℕ) : AddCommGrpCat.ofHom ((mk₀ (r • CategoryStruct.id M)).postcomp N ⋯) = 0

If r • N = 0, then r • 𝟙 M induces the zero endomorphism on Ext M N n.

theorem CategoryTheory.Abelian.Ext.postcomp_smul_id_mono_iff {R : Type u} [CommRing R] [Small.{v, u} R] {M N : ModuleCat R} (r : R) (i : ℕ) : Mono (AddCommGrpCat.ofHom ((mk₀ (r • CategoryStruct.id M)).postcomp N ⋯)) ↔ IsSMulRegular (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.