English
Let I be an IsHomogeneous 𝒜-ideal. If I ≠ ⊤ and whenever x,y are homogeneous and xy ∈ I, then x ∈ I or y ∈ I, then I is a prime ideal.
Русский
Пусть I — гомогенный 𝒜-идеал. Если I ≠ ⊤ и для любых однородных x,y из x y ∈ I следует x ∈ I или y ∈ I, то I — первый идеал.
LaTeX
$$$$ I \text{ IsHomogeneous } 𝒜 \; \land \; I \neq \top \; \land \; (\forall x,y, \ IsHomogeneousElem 𝒜 x \land \ IsHomogeneousElem 𝒜 y \land x y \in I \Rightarrow x \in I \lor y \in I) \;\Rightarrow \ I \text{ prime}. $$$$
Lean4
theorem isPrime_of_homogeneous_mem_or_mem {I : Ideal A} (hI : I.IsHomogeneous 𝒜) (I_ne_top : I ≠ ⊤)
(homogeneous_mem_or_mem : ∀ {x y : A}, IsHomogeneousElem 𝒜 x → IsHomogeneousElem 𝒜 y → x * y ∈ I → x ∈ I ∨ y ∈ I) :
Ideal.IsPrime I :=
⟨I_ne_top, by
intro x y hxy
by_contra! rid
obtain ⟨rid₁, rid₂⟩ := rid
classical
/-
The idea of the proof is the following :
since `x * y ∈ I` and `I` homogeneous, then `proj i (x * y) ∈ I` for any `i : ι`.
Then consider two sets `{i ∈ x.support | xᵢ ∉ I}` and `{j ∈ y.support | yⱼ ∉ J}`;
let `max₁, max₂` be the maximum of the two sets, then `proj (max₁ + max₂) (x * y) ∈ I`.
Then, `proj max₁ x ∉ I` and `proj max₂ j ∉ I`
but `proj i x ∈ I` for all `max₁ < i` and `proj j y ∈ I` for all `max₂ < j`.
` proj (max₁ + max₂) (x * y)`
`= ∑ {(i, j) ∈ supports | i + j = max₁ + max₂}, xᵢ * yⱼ`
`= proj max₁ x * proj max₂ y`
` + ∑ {(i, j) ∈ supports \ {(max₁, max₂)} | i + j = max₁ + max₂}, xᵢ * yⱼ`.
This is a contradiction, because both `proj (max₁ + max₂) (x * y) ∈ I` and the sum on the
right-hand side is in `I` however `proj max₁ x * proj max₂ y` is not in `I`.
-/
set set₁ := {i ∈ (decompose 𝒜 x).support | proj 𝒜 i x ∉ I} with set₁_eq
set set₂ := {i ∈ (decompose 𝒜 y).support | proj 𝒜 i y ∉ I} with set₂_eq
have nonempty : ∀ x : A, x ∉ I → {i ∈ (decompose 𝒜 x).support | proj 𝒜 i x ∉ I}.Nonempty :=
by
intro x hx
rw [filter_nonempty_iff]
contrapose! hx
simp_rw [proj_apply] at hx
rw [← sum_support_decompose 𝒜 x]
exact Ideal.sum_mem _ hx
set max₁ := set₁.max' (nonempty x rid₁)
set max₂ := set₂.max' (nonempty y rid₂)
have mem_max₁ : max₁ ∈ set₁ := max'_mem set₁ (nonempty x rid₁)
have mem_max₂ : max₂ ∈ set₂ := max'_mem set₂ (nonempty y rid₂)
replace hxy : proj 𝒜 (max₁ + max₂) (x * y) ∈ I := hI _ hxy
have mem_I : proj 𝒜 max₁ x * proj 𝒜 max₂ y ∈ I :=
by
set antidiag := {z ∈ (decompose 𝒜 x).support ×ˢ (decompose 𝒜 y).support | z.1 + z.2 = max₁ + max₂} with ha
have mem_antidiag : (max₁, max₂) ∈ antidiag :=
by
simp only [antidiag, mem_filter, mem_product]
exact ⟨⟨mem_of_mem_filter _ mem_max₁, mem_of_mem_filter _ mem_max₂⟩, trivial⟩
have eq_add_sum :=
calc
proj 𝒜 (max₁ + max₂) (x * y) = ∑ ij ∈ antidiag, proj 𝒜 ij.1 x * proj 𝒜 ij.2 y := by
simp_rw [ha, proj_apply, DirectSum.decompose_mul, DirectSum.coe_mul_apply 𝒜]
_ = proj 𝒜 max₁ x * proj 𝒜 max₂ y + ∑ ij ∈ antidiag.erase (max₁, max₂), proj 𝒜 ij.1 x * proj 𝒜 ij.2 y :=
(add_sum_erase _ _ mem_antidiag).symm
rw [eq_sub_of_add_eq eq_add_sum.symm]
refine Ideal.sub_mem _ hxy (Ideal.sum_mem _ fun z H => ?_)
rcases z with ⟨i, j⟩
simp only [antidiag, mem_erase, Prod.mk_inj, Ne, mem_filter, mem_product] at H
rcases H with ⟨H₁, ⟨H₂, H₃⟩, H₄⟩
have max_lt : max₁ < i ∨ max₂ < j :=
by
rcases lt_trichotomy max₁ i with (h | rfl | h)
· exact Or.inl h
· refine False.elim (H₁ ⟨rfl, add_left_cancel H₄⟩)
· apply Or.inr
have := add_lt_add_right h j
rw [H₄] at this
exact lt_of_add_lt_add_left this
rcases max_lt with max_lt | max_lt
· -- in this case `max₁ < i`, then `xᵢ ∈ I`; for otherwise `i ∈ set₁` then `i ≤ max₁`.
have notMem : i ∉ set₁ := fun h => lt_irrefl _ ((max'_lt_iff set₁ (nonempty x rid₁)).mp max_lt i h)
rw [set₁_eq] at notMem
simp only [not_and, Classical.not_not, mem_filter] at notMem
exact Ideal.mul_mem_right _ I (notMem H₂)
· -- in this case `max₂ < j`, then `yⱼ ∈ I`; for otherwise `j ∈ set₂`, then `j ≤ max₂`.
have notMem : j ∉ set₂ := fun h => lt_irrefl _ ((max'_lt_iff set₂ (nonempty y rid₂)).mp max_lt j h)
rw [set₂_eq] at notMem
simp only [not_and, Classical.not_not, mem_filter] at notMem
exact Ideal.mul_mem_left I _ (notMem H₃)
have notMem_I : proj 𝒜 max₁ x * proj 𝒜 max₂ y ∉ I :=
by
have neither_mem : proj 𝒜 max₁ x ∉ I ∧ proj 𝒜 max₂ y ∉ I :=
by
rw [mem_filter] at mem_max₁ mem_max₂
exact ⟨mem_max₁.2, mem_max₂.2⟩
intro _rid
rcases homogeneous_mem_or_mem ⟨max₁, SetLike.coe_mem _⟩ ⟨max₂, SetLike.coe_mem _⟩ mem_I with h | h
· apply neither_mem.1 h
· apply neither_mem.2 h
exact notMem_I mem_I⟩
