toIdeal_irrelevant — Mathlib

English

The ideal associated to the irrelevent homogeneous ideal is exactly the kernel of the zero-degree projection map.

Русский

Идеал, связанный с иррелевантным однородным идеалом, равен ядру отображения проекции на нулевую степень.

LaTeX

$$$$ (\operatorname{irrelevant}_{\mathcal{A}}).toIdeal = \ker( \mathrm{GradedRing.projZeroRingHom} \mathcal{A} ). $$$$

Lean4

@[simp]
theorem toIdeal_irrelevant : (HomogeneousIdeal.irrelevant 𝒜).toIdeal = RingHom.ker (GradedRing.projZeroRingHom 𝒜) :=
  rfl

Похожие утверждения