English
The ideal I = carrier.asIdeal f_deg hm q is a prime ideal of A.
Русский
Идеал I = carrier.asIdeal f_deg hm q является простым.
LaTeX
$$$I := carrier.asIdeal f_{deg} hm q \quad \Rightarrow\quad I \text{ isPrime in } A$$$
Lean4
theorem prime : (carrier.asIdeal f_deg hm q).IsPrime :=
(carrier.asIdeal.homogeneous f_deg hm q).isPrime_of_homogeneous_mem_or_mem (carrier.asIdeal.ne_top f_deg hm q)
fun {x y} ⟨nx, hnx⟩ ⟨ny, hny⟩ hxy =>
show (∀ _, _ ∈ _) ∨ ∀ _, _ ∈ _
by
rw [← and_forall_ne nx, and_iff_left, ← and_forall_ne ny, and_iff_left]
· apply q.2.mem_or_mem; convert hxy (nx + ny) using 1
dsimp
simp_rw [decompose_of_mem_same 𝒜 hnx, decompose_of_mem_same 𝒜 hny,
decompose_of_mem_same 𝒜 (SetLike.GradedMonoid.toGradedMul.mul_mem hnx hny), mul_pow, pow_add]
simp only [HomogeneousLocalization.ext_iff_val, HomogeneousLocalization.val_mk, HomogeneousLocalization.val_mul,
Localization.mk_mul]
simp only [Submonoid.mk_mul_mk, mk_eq_monoidOf_mk']
all_goals
intro n hn; convert q.1.zero_mem using 1
rw [HomogeneousLocalization.ext_iff_val, HomogeneousLocalization.val_mk, HomogeneousLocalization.val_zero];
simp_rw [proj_apply]
convert mk_zero (S := Submonoid.powers f) _
rw [decompose_of_mem_ne 𝒜 _ hn.symm, zero_pow hm.ne']
·
first
| exact hnx
| exact hny
