preimage_basicOpen — Mathlib

English

A variant of the mem_carrier lemma: if hm>0 and a ∈ 𝒜(nm), then a belongs to the carrier iff the localized expression lies in q.asIdeal.

Русский

Вариант леммы mem_carrier: если hm>0 и a ∈ 𝒜(nm), тогда a ∈ carrier тогда и только тогда, когда локализованное выражение лежит в q.asIdeal.

LaTeX

$$$a\in 𝒜(nm) \Rightarrow (a\in carrier f_deg q) \Leftrightarrow (HomogeneousLocalization.mk(...)) \in q.asIdeal$$$

Lean4

theorem preimage_basicOpen (z : HomogeneousLocalization.NumDenSameDeg 𝒜 (.powers f)) :
    toFun f ⁻¹' (sbo (HomogeneousLocalization.mk z) : Set (PrimeSpectrum (A⁰_ f))) =
      Subtype.val ⁻¹' (pbo z.num.1 : Set (ProjectiveSpectrum 𝒜)) :=
  Set.ext fun y ↦ (mk_mem_carrier y z).not

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