English
If x lies in the adjoin of a finite set in a localized ring, then there exists m in M such that m•x lies in the adjoin generated by the images of that finite set under the localization map.
Русский
Если элемент лежит в адъое конечного множества в локализованном кольце, то существует m в M такое, что m·x лежит в адъоя, порождаемом образами этого множества в локализации.
LaTeX
$$$\exists m\in M, m\cdot x \in \operatorname{adjoin}_R(\text{IsLocalization.finsetIntegerMultiple }(M)\,s)$$$
Lean4
/-- 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`.
-/
theorem lift_mem_adjoin_finsetIntegerMultiple [Algebra R S'] [IsScalarTower R S S']
[IsLocalization (M.map (algebraMap R S)) S'] (x : S) (s : Finset S')
(hx : algebraMap S S' x ∈ Algebra.adjoin R (s : Set S')) :
∃ m : M, m • x ∈ Algebra.adjoin R (IsLocalization.finsetIntegerMultiple (M.map (algebraMap R S)) s : Set S) :=
by
obtain ⟨⟨_, a, ha, rfl⟩, e⟩ :=
IsLocalization.exists_smul_mem_of_mem_adjoin (M.map (algebraMap R S)) x s (Algebra.adjoin R _) Algebra.subset_adjoin
(by rintro _ ⟨a, _, rfl⟩; exact Subalgebra.algebraMap_mem _ a) hx
refine ⟨⟨a, ha⟩, ?_⟩
simpa only [Submonoid.smul_def, algebraMap_smul] using e
