Theorems · Theorem · commutative algebra

IsLocalization.lift_mem_adjoin_finsetIntegerMultiple

∀ {R : Type u_1} {S : Type u_2} [inst : CommRing R] [inst_1 : CommRing S] [inst_2 : Algebra R S] (M : Submonoid R)
  {S' : Type u_4} [inst_3 : CommRing S'] [inst_4 : Algebra S 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 ∈ Algebra.adjoin R ↑s →
    ∃ m, m • x ∈ Algebra.adjoin 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 adjoin of some finite s ⊆ S' over R, then there exists some m : M such that m • x falls in the adjoin of IsLocalization.finsetIntegerMultiple _ s over R.

Defined in

Mathlib.RingTheory.Finiteness.FiniteTypeLocal

Cited by

1 results in Mathlib

Foundations

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

Assumes

CommRingCommRingAlgebraCommRingAlgebraAlgebraIsScalarTowerIsLocalization