Mathlib Map

Theorems · Theorem · category theory

Module.injective_module_of_injective_object

∀ (R : Type u) (M : Type v) [inst : Ring R] [inst_1 : AddCommGroup M] [inst_2 : Module R M]
  [inj : CategoryTheory.Injective (ModuleCat.of R M)], Module.Injective R M
Defined in
Mathlib.Algebra.Category.ModuleCat.Injective
Cited by
2 results in Mathlib
Foundations
Depth 71 from the axioms · uses propext, Classical.choice, Quot.sound
Assumes
RingAddCommGroupModuleCategoryTheory.Injective
Mathlib docsSourceLoogleLeanSearch

Around this declaration

Dashed lines are statement dependencies; solid lines are citations in proofs.

Module.injective_iff_injective_object · cited by 3Module.injective_iff_inje…ModuleCat.hasInjectiveDimensionLE_iff_forall_maximalSpectrum · cited by 2ModuleCat.hasInjectiveDim…DFunLike.coe · cited by 62936DFunLike.coeQuiver.Hom · cited by 32603Quiver.HomModule · cited by 20661ModuleRingHom.id · cited by 18349RingHom.idCategoryTheory.CategoryStruct.comp · cited by 17999CategoryStruct.compAddCommGroup · cited by 12871AddCommGroupLinearMap · cited by 10215LinearMapRing · cited by 7463RingModuleCat · cited by 1429ModuleCatCategoryTheory.Mono · cited by 893CategoryTheory.MonoModuleCat.of · cited by 594ModuleCat.ofModuleCat.Hom.hom · cited by 341Hom.homModuleCat.ofHom · cited by 200ModuleCat.ofHomCategoryTheory.Injective · cited by 70CategoryTheory.InjectiveModuleCat.mono_iff_injective · cited by 21ModuleCat.mono_iff_inject…Module.injective_module_of_in…CITED BYCITES

Cites18

Mathlib declarations this one mentions in its statement or cites explicitly in its proof. Plumbing is filtered out.

Cited by2

Results whose statement or proof uses this declaration.