English
Let S be an R-algebra, M a submonoid of S, and A an R-subalgebra of S containing M and numerators from an adjoin; then there exists m in M with m•x ∈ A for certain x.
Русский
Пусть S — R-алгебра, M — подподгруппа подмоной в S, а A — R-подалгебра S, содержащая M и числители элементов адъоя; тогда существует m в M такое, что m·x ∈ A для некоторых x.
LaTeX
$$$\exists m∈M, m\cdot x \in A$ under the stated adjoin and containment hypotheses.$$
Lean4
/-- 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`.
-/
theorem exists_smul_mem_of_mem_adjoin [Algebra R S'] [IsScalarTower R S S'] (M : Submonoid S) [IsLocalization M S']
(x : S) (s : Finset S') (A : Subalgebra R S) (hA₁ : (IsLocalization.finsetIntegerMultiple M s : Set S) ⊆ A)
(hA₂ : M ≤ A.toSubmonoid) (hx : algebraMap S S' x ∈ Algebra.adjoin R (s : Set S')) : ∃ m : M, m • x ∈ A :=
by
let g : S →ₐ[R] S' := IsScalarTower.toAlgHom R S S'
let y := IsLocalization.commonDenomOfFinset M s
have hx₁ : (y : S) • (s : Set S') = g '' _ := (IsLocalization.finsetIntegerMultiple_image _ s).symm
obtain ⟨n, hn⟩ :=
Algebra.pow_smul_mem_of_smul_subset_of_mem_adjoin (y : S) (s : Set S') (A.map g)
(by rw [hx₁]; exact Set.image_mono hA₁) hx (Set.mem_image_of_mem _ (hA₂ y.2))
obtain ⟨x', hx', hx''⟩ := hn n (le_of_eq rfl)
rw [Algebra.smul_def, ← map_mul] at hx''
obtain ⟨a, ha₂⟩ := (IsLocalization.eq_iff_exists M S').mp hx''
use a * y ^ n
convert A.mul_mem hx' (hA₂ a.prop) using 1
rw [Submonoid.smul_def, smul_eq_mul, Submonoid.coe_mul, SubmonoidClass.coe_pow, mul_assoc, ← ha₂, mul_comm]
