English
If f belongs to 𝒜 m, then for any element z in Away 𝒜 f, the powers of f acting on z eventually land in the image of 𝒜 (n • m) under the algebra map.
Русский
Если f ∈ 𝒜 m, то для любого z ∈ Away 𝒜 f пределом будет, что f^n действует на z и в итоге попадает в образ 𝒜 (n • m) через отображение алгебры.
LaTeX
$$$$ \forall m, \; f \in 𝒜 m \; \Rightarrow \; \forall z \in \mathrm{Away}(\mathcal{A}, f), \; \text{eventually } n, \; f^{n} \cdot z.val \in \mathrm{algebraMap}\;\_\;\_ ''(𝒜 (n \cdot m):\, \mathrm{Set} A). $$$$
Lean4
theorem eventually_smul_mem {m} (hf : f ∈ 𝒜 m) (z : Away 𝒜 f) :
∀ᶠ n in Filter.atTop, f ^ n • z.val ∈ algebraMap _ _ '' (𝒜 (n • m) : Set A) :=
by
obtain ⟨k, hk : f ^ k = _⟩ := z.den_mem
apply Filter.mem_of_superset (Filter.Ici_mem_atTop k)
rintro k' (hk' : k ≤ k')
simp only [Set.mem_image, SetLike.mem_coe, Set.mem_setOf_eq]
by_cases hfk : f ^ k = 0
· refine ⟨0, zero_mem _, ?_⟩
rw [← tsub_add_cancel_of_le hk', map_zero, pow_add, hfk, mul_zero, zero_smul]
rw [← tsub_add_cancel_of_le hk', pow_add, mul_smul, hk, den_smul_val, Algebra.smul_def, ← map_mul]
rw [← smul_eq_mul, add_smul,
DirectSum.degree_eq_of_mem_mem 𝒜 (SetLike.pow_mem_graded _ hf) (hk.symm ▸ z.den_mem_deg) hfk]
exact ⟨_, SetLike.mul_mem_graded (SetLike.pow_mem_graded _ hf) z.num_mem_deg, rfl⟩
