Theorems · Theorem · commutative algebra

IsLocalization.exists_smul_mem_of_mem_adjoin

∀ {R : Type u_1} {S : Type u_2} [inst : CommRing R] [inst_1 : CommRing S] [inst_2 : Algebra R S] {S' : Type u_4}
  [inst_3 : CommRing S'] [inst_4 : Algebra S S'] [inst_5 : Algebra R S'] [IsScalarTower R S S'] (M : Submonoid S)
  [inst_7 : IsLocalization M S'] (x : S) (s : Finset S') (A : Subalgebra R S),
  ↑(IsLocalization.finsetIntegerMultiple M s) ⊆ ↑A →
    M ≤ A.toSubmonoid → (algebraMap S S') x ∈ Algebra.adjoin R ↑s → ∃ m, m • x ∈ A

Let S be an R-algebra, M a submonoid of S, S' = M⁻¹S. Suppose the image of some x : S falls in the adjoin of some finite s ⊆ S' over R, and A is an R-subalgebra of S containing both M and the numerators of s. Then, there exists some m : M such that m • x falls in A.

Defined in

Mathlib.RingTheory.Finiteness.FiniteTypeLocal

Cited by

2 results in Mathlib

Foundations

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

Assumes

CommRingCommRingAlgebraCommRingAlgebraAlgebraIsScalarTowerIsLocalization