mk_mem_toSpec_base_apply — Mathlib

English

A criterion for membership in the base ideal is that the numerator belongs to the homogeneous ideal of the point x; the localization symbol mk preserves this correspondence.

Русский

Критерий принадлежности элемента базовому идеалу: числитель принадлежит однородному идеалу точки x; локализация сохраняет это соответствие.

LaTeX

$$$\text{HomogeneousLocalization.mk}\,z \in ((toSpec\;\mathcal{A}f).base\;x).asIdeal \iff z.num.1 \in x.1.asHomogeneousIdeal$$$

Lean4

theorem mk_mem_toSpec_base_apply {f} (x : Proj| pbo f) (z : NumDenSameDeg 𝒜 (.powers f)) :
    HomogeneousLocalization.mk z ∈ ((toSpec 𝒜 f).base x).asIdeal ↔ z.num.1 ∈ x.1.asHomogeneousIdeal :=
  (toSpec_base_apply_eq 𝒜 x).symm ▸ ProjIsoSpecTopComponent.ToSpec.mk_mem_carrier _ _

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