support_eq_zeroLocus — Mathlib

English

Let R be a commutative ring and M a finite R-module. Then the support of M is the zero locus of its annihilator: Supp_R(M) = V(Ann_R(M)).

Русский

Пусть R — коммутативное кольцо, M — конечный модуль над R. Тогда поддержка M равна нулевой множеству аннигилирующего идеала Ann_R(M): Supp_R(M) = V(Ann_R(M)).

LaTeX

$$$\\\\mathrm{Supp}_R(M) = \\mathrm{V}(\\\\mathrm{Ann}_R(M))$$$

Lean4

/-- If `M` is `R`-finite, then `Supp M = Z(Ann(M))`. -/
@[stacks 00L2]
theorem support_eq_zeroLocus : Module.support R M = zeroLocus (Module.annihilator R M) :=
  Set.ext fun _ ↦ mem_support_iff_of_finite

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