toFun — Mathlib

English

For z in NumDenSameDeg 𝒜, the preimage under toSpec of the basicOpen corresponds to a basic open on ProjectiveSpectrum.

Русский

Для z в NumDenSameDeg 𝒜 предобраз под toSpec базовой открытой соответствует базовой открытой на ProjectiveSpectrum.

LaTeX

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

Lean4

/-- The function between the basic open set `D(f)` in `Proj` to the corresponding basic open set in
`Spec A⁰_f`. This is bundled into a continuous map in `TopComponent.forward`.
-/
@[simps -isSimp]
def toFun (x : Proj.T| pbo f) : Spec.T A⁰_ f :=
  ⟨carrier x, isPrime_carrier x⟩
    /-
    The preimage of basic open set `D(a/f^n)` in `Spec A⁰_f` under the forward map from `Proj A` to
    `Spec A⁰_f` is the basic open set `D(a) ∩ D(f)` in `Proj A`. This lemma is used to prove that the
    forward map is continuous.
    -/

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