Theorems · Theorem · commutative algebra

Module.flat_of_isLocalized_maximal

∀ {R : Type u_1} (S : Type u_2) [inst : CommSemiring R] [inst_1 : CommSemiring S] [inst_2 : Algebra R S] (M : Type u_3)
  [inst_3 : AddCommMonoid M] [inst_4 : Module R M] [inst_5 : Module S M] [IsScalarTower R S M]
  (Mₚ : (P : Ideal S) → [P.IsMaximal] → Type u_4) [inst_7 : (P : Ideal S) → [inst : P.IsMaximal] → AddCommMonoid (Mₚ P)]
  [inst_8 : (P : Ideal S) → [inst_8 : P.IsMaximal] → Module R (Mₚ P)]
  [inst_9 : (P : Ideal S) → [inst : P.IsMaximal] → Module S (Mₚ P)]
  [∀ (P : Ideal S) [inst_10 : P.IsMaximal], IsScalarTower R S (Mₚ P)]
  (f : (P : Ideal S) → [inst : P.IsMaximal] → M →ₗ[S] Mₚ P)
  [∀ (P : Ideal S) [inst : P.IsMaximal], IsLocalizedModule.AtPrime P (f P)],
  (∀ (P : Ideal S) [inst_12 : P.IsMaximal], Module.Flat R (Mₚ P)) → Module.Flat R M

Defined in

Mathlib.RingTheory.Flat.Localization

Cited by

2 results in Mathlib

Foundations

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

Assumes

CommSemiringCommSemiringAlgebraAddCommMonoidModuleModuleIsScalarTowerAddCommMonoidModuleModuleIsScalarTowerIsLocalizedModule.AtPrime