English
Let r ∈ A, s ⊆ B, B' ⊆ B be a subalgebra, and hs r•s ⊆ B'. If x ∈ adjoin_R s and hr: algebraMap_A_B r ∈ B', then there exists n0 such that for all n ≥ n0, r^n • x ∈ B'.
Русский
Пусть r ∈ A, s ⊆ B, B' ⊆ B; если r·s ⊆ B' и x ∈ adjoin_R s и hr: algebraMap_A_B r ∈ B', то существует n0:ℕ, такое что для всех n ≥ n0 выполняется r^n · x ∈ B'.
LaTeX
$$$\\exists n_0:\\mathbb{N},\\ \\forall n \\ge n_0,\\ r^{n}\\cdot x \\in B'$$$
Lean4
theorem pow_smul_mem_of_smul_subset_of_mem_adjoin [CommSemiring B] [Algebra R B] [Algebra A B] [IsScalarTower R A B]
(r : A) (s : Set B) (B' : Subalgebra R B) (hs : r • s ⊆ B') {x : B} (hx : x ∈ adjoin R s)
(hr : algebraMap A B r ∈ B') : ∃ n₀ : ℕ, ∀ n ≥ n₀, r ^ n • x ∈ B' :=
by
change x ∈ Subalgebra.toSubmodule (adjoin R s) at hx
rw [adjoin_eq_span, Finsupp.mem_span_iff_linearCombination] at hx
rcases hx with ⟨l, rfl : (l.sum fun (i : Submonoid.closure s) (c : R) => c • (i : B)) = x⟩
choose n₁ n₂ using fun x : Submonoid.closure s => Submonoid.pow_smul_mem_closure_smul r s x.prop
use l.support.sup n₁
intro n hn
rw [Finsupp.smul_sum]
refine B'.toSubmodule.sum_mem ?_
intro a ha
have : n ≥ n₁ a := le_trans (Finset.le_sup ha) hn
dsimp only
rw [← tsub_add_cancel_of_le this, pow_add, ← smul_smul, ← IsScalarTower.algebraMap_smul A (l a) (a : B),
smul_smul (r ^ n₁ a), mul_comm, ← smul_smul, smul_def, map_pow, IsScalarTower.algebraMap_smul]
apply Subalgebra.mul_mem _ (Subalgebra.pow_mem _ hr _) _
refine Subalgebra.smul_mem _ ?_ _
change _ ∈ B'.toSubmonoid
rw [← Submonoid.closure_eq B'.toSubmonoid]
apply Submonoid.closure_mono hs (n₂ a)
