English
In a graded ring graded by a canonically ordered additive monoid, the irrelevant ideal is the subideal consisting of all elements with zero zero-th component, equivalently the direct sum of all positive-degree components.
Русский
В градуированном кольце, градуированном по канонически упорядоченному аддитивному полю, иррелевантный идеал — это подидеал, состоящий из элементов с нулевой нулевой компонентой, то есть равен прямой сумме всех компонент степени > 0.
LaTeX
$$$$ (\operatorname{irrelevant}_{\mathcal{A}})^{\text{toIdeal}} = \ker(\mathrm{GradedRing.projZeroRingHom} \mathcal{A}) = \{ a \in \bigoplus_i \mathcal{A}_i \,|\, a_0 = 0 \} = \bigoplus_{i>0} \mathcal{A}_i. $$$$
Lean4
/-- For a graded ring `⨁ᵢ 𝒜ᵢ` graded by a `CanonicallyOrderedAddCommMonoid ι`, the irrelevant ideal
refers to `⨁_{i>0} 𝒜ᵢ`, or equivalently `{a | a₀ = 0}`. This definition is used in `Proj`
construction where `ι` is always `ℕ` so the irrelevant ideal is simply elements with `0` as
0-th coordinate.
# Future work
Here in the definition, `ι` is assumed to be `CanonicallyOrderedAddCommMonoid`. However, the notion
of irrelevant ideal makes sense in a more general setting by defining it as the ideal of elements
with `0` as i-th coordinate for all `i ≤ 0`, i.e. `{a | ∀ (i : ι), i ≤ 0 → aᵢ = 0}`.
-/
def irrelevant : HomogeneousIdeal 𝒜 :=
⟨RingHom.ker (GradedRing.projZeroRingHom 𝒜), fun i r (hr : (decompose 𝒜 r 0 : A) = 0) =>
by
change (decompose 𝒜 (decompose 𝒜 r _ : A) 0 : A) = 0
by_cases h : i = 0
· rw [h, hr, decompose_zero, zero_apply, ZeroMemClass.coe_zero]
· rw [decompose_of_mem_ne 𝒜 (SetLike.coe_mem _) h]⟩
