English
Let f_deg be a degenerate element of the graded submodule 𝒜 at degree m, and q a prime in the localized structure. If a and b are elements of the carrier at q, then their sum a + b is also in the carrier at q.
Русский
Пусть f_deg ∈ 𝒜(m) и q — простой идеал в локализации. Если a и b принадлежат носителю carrier f_deg q, то и a + b принадлежит 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) \ {a,b : A}, a \in carrier(f_{deg},q) \to b \in carrier(f_{deg},q) \to a + b \in carrier(f_{deg},q)$.$$
Lean4
theorem add_mem (q : Spec.T A⁰_ f) {a b : A} (ha : a ∈ carrier f_deg q) (hb : b ∈ carrier f_deg q) :
a + b ∈ carrier f_deg q := by
refine fun i => (q.2.mem_or_mem ?_).elim id id
change (HomogeneousLocalization.mk ⟨_, _, _, _⟩ : A⁰_ f) ∈ q.1; dsimp only [Subtype.coe_mk]
simp_rw [← pow_add, map_add, add_pow, mul_comm, ← nsmul_eq_mul]
let g : ℕ → A⁰_ f := fun j =>
(m + m).choose j •
if h2 : m + m < j then (0 : A⁰_ f)
else
if h1 : j ≤ m then
(HomogeneousLocalization.mk
⟨m * i, ⟨proj 𝒜 i a ^ j * proj 𝒜 i b ^ (m - j), ?_⟩, ⟨_, by rw [mul_comm]; mem_tac⟩, ⟨i, rfl⟩⟩ :
A⁰_ f) *
(HomogeneousLocalization.mk
⟨m * i, ⟨proj 𝒜 i b ^ m, by rw [← smul_eq_mul]; mem_tac⟩, ⟨_, by rw [mul_comm]; mem_tac⟩, ⟨i, rfl⟩⟩ :
A⁰_ f)
else
(HomogeneousLocalization.mk
⟨m * i, ⟨proj 𝒜 i a ^ m, by rw [← smul_eq_mul]; mem_tac⟩, ⟨_, by rw [mul_comm]; mem_tac⟩, ⟨i, rfl⟩⟩ :
A⁰_ f) *
(HomogeneousLocalization.mk
⟨m * i, ⟨proj 𝒜 i a ^ (j - m) * proj 𝒜 i b ^ (m + m - j), ?_⟩, ⟨_, by rw [mul_comm]; mem_tac⟩,
⟨i, rfl⟩⟩ :
A⁰_ f)
rotate_left
· rw [(_ : m * i = _)]
apply GradedMonoid.toGradedMul.mul_mem <;> mem_tac_aux
rw [← add_smul, Nat.add_sub_of_le h1]; rfl
· rw [(_ : m * i = _)]
apply GradedMonoid.toGradedMul.mul_mem (i := (j - m) • i) (j := (m + m - j) • i) <;> mem_tac_aux
rw [← add_smul]; congr; cutsat
convert_to ∑ i ∈ range (m + m + 1), g i ∈ q.1; swap
· refine q.1.sum_mem fun j _ => nsmul_mem ?_ _; split_ifs
exacts [q.1.zero_mem, q.1.mul_mem_left _ (hb i), q.1.mul_mem_right _ (ha i)]
rw [HomogeneousLocalization.ext_iff_val, HomogeneousLocalization.val_mk]
change _ = (algebraMap (HomogeneousLocalization.Away 𝒜 f) (Localization.Away f)) _
dsimp only [Subtype.coe_mk]; rw [map_sum, mk_sum]
apply Finset.sum_congr rfl fun j hj => _
intro j hj
change _ = HomogeneousLocalization.val _
rw [HomogeneousLocalization.val_smul]
split_ifs with h2 h1
· exact ((Finset.mem_range.1 hj).not_ge h2).elim
all_goals simp only [HomogeneousLocalization.val_mul, HomogeneousLocalization.val_mk, Localization.mk_mul, ← smul_mk];
congr 2
· dsimp; rw [mul_assoc, ← pow_add, add_comm (m - j), Nat.add_sub_assoc h1]
· simp_rw [pow_add]; rfl
· dsimp; rw [← mul_assoc, ← pow_add, Nat.add_sub_of_le (le_of_not_ge h1)]
· simp_rw [pow_add]; rfl
