Theorems · Theorem · commutative algebra

Module.injective_of_isLocalizedModule

∀ {R : Type u} [inst : CommRing R] {M : Type v} [inst_1 : AddCommGroup M] [inst_2 : Module R M] (S : Submonoid R)
  [Small.{v, u} R] [IsNoetherianRing R] {Rₛ : Type u'} [Small.{v', u'} Rₛ] [inst_6 : CommRing Rₛ]
  [inst_7 : Algebra R Rₛ] {Mₛ : Type v'} [inst_8 : AddCommGroup Mₛ] [inst_9 : Module R Mₛ] [inst_10 : Module Rₛ Mₛ]
  [IsScalarTower R Rₛ Mₛ] (f : M →ₗ[R] Mₛ) [IsLocalization S Rₛ] [IsLocalizedModule S f] [Module.Injective R M],
  Module.Injective Rₛ Mₛ

Defined in

Mathlib.RingTheory.LocalProperties.Injective

Cited by

2 results in Mathlib

Foundations

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

Assumes

CommRingAddCommGroupModuleSmallIsNoetherianRingSmallCommRingAlgebraAddCommGroupModuleModuleIsScalarTowerIsLocalizationIsLocalizedModuleModule.Injective