English
For any c ∈ A and x ∈ carrier f_deg q, the product c • x lies in carrier f_deg q.
Русский
Для любого скаляра c ∈ A и элемента x ∈ carrier f_deg q верно c · x ∈ carrier f_deg q.
LaTeX
$$$\forall R A [\text{CommRing } R] [\text{CommRing } A] [\text{Algebra } R A] \{𝒜 : \mathbb{N} \to \text{Submodule } R A\} [\text{GradedAlgebra } 𝒜] \{f : A\} {m : \mathbb{N}}(f_{deg} : f \in 𝒜(m)) \ (q : Spec.T A_f^0) \forall c \in A, x \in carrier(f_{deg},q), c • x \in carrier(f_{deg},q).$$$
Lean4
theorem smul_mem (c x : A) (hx : x ∈ carrier f_deg q) : c • x ∈ carrier f_deg q :=
by
revert c
refine DirectSum.Decomposition.inductionOn 𝒜 ?_ ?_ ?_
· rw [zero_smul]; exact carrier.zero_mem f_deg hm _
· rintro n ⟨a, ha⟩ i
simp_rw [proj_apply, smul_eq_mul, coe_decompose_mul_of_left_mem 𝒜 i ha]
let product : A⁰_ f :=
(HomogeneousLocalization.mk ⟨_, ⟨a ^ m, pow_mem_graded m ha⟩, ⟨_, ?_⟩, ⟨n, rfl⟩⟩ : A⁰_ f) *
(HomogeneousLocalization.mk ⟨_, ⟨proj 𝒜 (i - n) x ^ m, by mem_tac⟩, ⟨_, ?_⟩, ⟨i - n, rfl⟩⟩ : A⁰_ f)
· split_ifs with h
· convert_to product ∈ q.1
· dsimp [product]
rw [HomogeneousLocalization.ext_iff_val, HomogeneousLocalization.val_mk, HomogeneousLocalization.val_mul,
HomogeneousLocalization.val_mk, HomogeneousLocalization.val_mk]
· simp_rw [mul_pow]; rw [Localization.mk_mul]
· congr; rw [← pow_add, Nat.add_sub_of_le h]
· apply Ideal.mul_mem_left (α := A⁰_ f) _ _ (hx _)
rw [(_ : m • n = _)]
· mem_tac
· simp only [smul_eq_mul, mul_comm]
· simpa only [map_zero, zero_pow hm.ne'] using zero_mem f_deg hm q i
rw [(_ : m • (i - n) = _)]
· mem_tac
· simp only [smul_eq_mul, mul_comm]
· simp_rw [add_smul]; exact fun _ _ => carrier.add_mem f_deg q
