toSpec — Mathlib

English

Compatibility of preimage under the ToSpec map with the ProjectiveSpectrum basic opens.

Русский

Совместимость предобраза под отображением ToSpec с базовыми открытыми в ProjectiveSpectrum.

LaTeX

$$$\text{preimage}(ToSpec) = \text{basicOpen}$$$

Lean4

/-- The continuous function from the basic open set `D(f)` in `Proj`
to the corresponding basic open set in `Spec A⁰_f`. -/
@[simps! -isSimp hom_apply_asIdeal]
def toSpec (f : A) : (Proj.T| pbo f) ⟶ Spec.T A⁰_ f :=
  TopCat.ofHom
    { toFun := ToSpec.toFun f
      continuous_toFun := by
        rw [PrimeSpectrum.isTopologicalBasis_basic_opens.continuous_iff]
        rintro _ ⟨x, rfl⟩
        obtain ⟨x, rfl⟩ := Quotient.mk''_surjective x
        rw [ToSpec.preimage_basicOpen]
        exact (pbo x.num).2.preimage continuous_subtype_val }

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