image_basicOpen_eq_basicOpen — Mathlib

English

There is a homogeneous ideal that corresponds to the prime spectrum of the localized ring A⁰_f.

Русский

Существует однородный идеал, соответствующий спектру примарно локализованного кольца A⁰_f.

LaTeX

$$$I = carrier.asIdeal f_deg hm q \text{ is homogeneous and prime, giving a bridge to } \Spec(A^0_f)$$$

Lean4

theorem image_basicOpen_eq_basicOpen (a : A) (i : ℕ) :
    toSpec 𝒜 f '' (Subtype.val ⁻¹' (pbo (decompose 𝒜 a i) : Set (ProjectiveSpectrum 𝒜))) =
      (PrimeSpectrum.basicOpen (R := A⁰_ f) <|
          HomogeneousLocalization.mk
            ⟨m * i, ⟨decompose 𝒜 a i ^ m, smul_eq_mul m i ▸ SetLike.pow_mem_graded _ (Submodule.coe_mem _)⟩,
              ⟨f ^ i, by rw [mul_comm]; exact SetLike.pow_mem_graded _ f_deg⟩, ⟨i, rfl⟩⟩).1 :=
  Set.preimage_injective.mpr (toSpec_surjective 𝒜 f_deg hm) <|
    Set.preimage_image_eq _ (toSpec_injective 𝒜 f_deg hm) ▸ by
      rw [Opens.carrier_eq_coe, toSpec_preimage_basicOpen, ProjectiveSpectrum.basicOpen_pow 𝒜 _ m hm]

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