toFun — Mathlib

English

The homogeneous structure is compatible with the carrier and 𝒜.

Русский

Однородная структура согласована с carrier и 𝒜.

LaTeX

$$$(carrier.asIdeal f_deg hm q).IsHomogeneous 𝒜$$$

Lean4

/-- The function `Spec A⁰_f → Proj|D(f)` sending `q` to `{a | aᵢᵐ/fⁱ ∈ q}`. -/
def toFun : (Spec.T A⁰_ f) → Proj.T| pbo f := fun q =>
  ⟨⟨carrier.asHomogeneousIdeal f_deg hm q, carrier.asIdeal.prime f_deg hm q, carrier.relevant f_deg hm q⟩,
    (ProjectiveSpectrum.mem_basicOpen _ f _).mp <| carrier.denom_notMem f_deg hm q⟩

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