English
A finite additive combination expressing 1 with elements and coefficients in a subalgebra implies membership of a target element in that subalgebra, given nested smul/power conditions.
Русский
Конечная сумма с единицей, выраженная через элементы и коэффициенты внутри подалгебры, в сочетании с условиями на сглаживания/степени, гарантирует принадлежность искомого элемента подалгебре.
LaTeX
$$$${\\iota'}.sum (\\lambda i, l_i \\cdot s_i) = 1 \\quad\\Rightarrow\\quad (\\forall i, s_i \\in S') \\land (\\forall i, l_i \\in S') \\land (\\forall i, \\exists n, (s_i^n) x \\in S') \\Rightarrow x \\in S'$$$$
Lean4
/-- Suppose we are given `∑ i, lᵢ * sᵢ = 1` ∈ `S`, and `S'` a subalgebra of `S` that contains
`lᵢ` and `sᵢ`. To check that an `x : S` falls in `S'`, we only need to show that
`sᵢ ^ n • x ∈ S'` for some `n` for each `sᵢ`. -/
theorem mem_of_finset_sum_eq_one_of_pow_smul_mem {ι : Type*} (ι' : Finset ι) (s : ι → S) (l : ι → S)
(e : ∑ i ∈ ι', l i * s i = 1) (hs : ∀ i, s i ∈ S') (hl : ∀ i, l i ∈ S') (x : S)
(H : ∀ i, ∃ n : ℕ, (s i ^ n : S) • x ∈ S') : x ∈ S' :=
by
suffices x ∈ Subalgebra.toSubmodule (Algebra.ofId S' S).range
by
obtain ⟨x, rfl⟩ := this
exact x.2
choose n hn using H
let s' : ι → S' := fun x => ⟨s x, hs x⟩
let l' : ι → S' := fun x => ⟨l x, hl x⟩
have e' : ∑ i ∈ ι', l' i * s' i = 1 := by
ext
change S'.subtype (∑ i ∈ ι', l' i * s' i) = 1
simpa only [map_sum, map_mul] using e
have : Ideal.span (s' '' ι') = ⊤ := by
rw [Ideal.eq_top_iff_one, ← e']
apply sum_mem
intro i hi
exact Ideal.mul_mem_left _ _ <| Ideal.subset_span <| Set.mem_image_of_mem s' hi
let N := ι'.sup n
have hN := Ideal.span_pow_eq_top _ this N
apply (Algebra.ofId S' S).range.toSubmodule.mem_of_span_top_of_smul_mem _ hN
rintro ⟨_, _, ⟨i, hi, rfl⟩, rfl⟩
change s' i ^ N • x ∈ _
rw [← tsub_add_cancel_of_le (show n i ≤ N from Finset.le_sup hi), pow_add, mul_smul]
refine Submodule.smul_mem _ (⟨_, pow_mem (hs i) _⟩ : S') ?_
exact ⟨⟨_, hn i⟩, rfl⟩
