Theorems · Theorem · commutative algebra

Module.flat_of_isLocalized_span

∀ {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] (s : Set S),
  Ideal.span s = ⊤ →
    ∀ (Mₛ : ↑s → Type u_5) [inst_7 : (r : ↑s) → AddCommMonoid (Mₛ r)] [inst_8 : (r : ↑s) → Module R (Mₛ r)]
      [inst_9 : (r : ↑s) → Module S (Mₛ r)] [∀ (r : ↑s), IsScalarTower R S (Mₛ r)] (g : (r : ↑s) → M →ₗ[S] Mₛ r)
      [∀ (r : ↑s), IsLocalizedModule.Away (↑r) (g r)], (∀ (r : ↑s), Module.Flat R (Mₛ r)) → 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.Away