Theorems · Theorem · commutative algebra

IsLocalization.smul_mem_finsetIntegerMultiple_span

∀ {R : Type u_1} {S : Type u_2} [inst : CommSemiring R] [inst_1 : CommSemiring S] (M : Submonoid R) (S' : Type u_4)
  [inst_2 : CommSemiring S'] [inst_3 : Algebra S S'] [inst_4 : Algebra R S] [inst_5 : Algebra R S']
  [IsScalarTower R S S'] [inst_7 : IsLocalization (Submonoid.map (algebraMap R S) M) S'] (x : S) (s : Finset S'),
  (algebraMap S S') x ∈ Submodule.span R ↑s →
    ∃ m, m • x ∈ Submodule.span R ↑(IsLocalization.finsetIntegerMultiple (Submonoid.map (algebraMap R S) M) s)

Let S be an R-algebra, M a submonoid of R, and S' = M⁻¹S. If the image of some x : S falls in the span of some finite s ⊆ S' over R, then there exists some m : M such that m • x falls in the span of IsLocalization.finsetIntegerMultiple _ s over R.

Defined in

Mathlib.RingTheory.Localization.Finiteness

Cited by

1 results in Mathlib

Foundations

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

Assumes

CommSemiringCommSemiringCommSemiringAlgebraAlgebraAlgebraIsScalarTowerIsLocalization