English
For a homogeneous ideal I, I is prime if and only if I ≠ ⊤ and the homogeneous elements behave like a prime test under multiplication.
Русский
Для гомогенного идеала I: I — первый тогда и только тогда, когда I ≠ ⊤ и гомогенные элементы ведут себя как тест на простоту при умножении.
LaTeX
$$$$ I \ IsHomogeneous 𝒜 \; \Rightarrow \; I \ IsPrime \ \iff\ \ I \neq \top \land (\forall x,y, \ IsHomogeneousElem 𝒜 x \land IsHomogeneousElem 𝒜 y \land xy \in I \Rightarrow x \in I \lor y \in I). $$$$
Lean4
theorem isPrime_iff {I : Ideal A} (h : I.IsHomogeneous 𝒜) :
I.IsPrime ↔ I ≠ ⊤ ∧ ∀ {x y : A}, IsHomogeneousElem 𝒜 x → IsHomogeneousElem 𝒜 y → x * y ∈ I → x ∈ I ∨ y ∈ I :=
⟨fun HI => ⟨HI.ne_top, fun _ _ hxy => Ideal.IsPrime.mem_or_mem HI hxy⟩, fun ⟨I_ne_top, homogeneous_mem_or_mem⟩ =>
h.isPrime_of_homogeneous_mem_or_mem I_ne_top @homogeneous_mem_or_mem⟩
