toOpen_toSpec_val_c_app — Mathlib

English

In the Away localization at a homogeneous prime, one obtains the universal property of localization at the corresponding prime ideal; this manifests as an isomorphism that equates the localized away ring with the algebra induced at the prime.

Русский

В локализации Away по простому идеалу оценивается универсальная характеристика локализации в соответствующем простом идеале; это выражается изоморфизмом, приравнивающим локализованную away-область к алгебре, заданной наprime.

LaTeX

$$$$\text{IsLocalization}(\mathrm{Away}\ 𝒜 f\, , ((toSpec\ 𝒜 f).base x).asIdeal.primeCompl, (AtPrime 𝒜 x.asHomogeneousIdeal.toIdeal), \dots)$$$$

Lean4

@[reassoc]
theorem toOpen_toSpec_val_c_app (f) (U) :
    StructureSheaf.toOpen (A⁰_ f) U.unop ≫ (toSpec 𝒜 f).c.app U =
      awayToΓ 𝒜 f ≫ (Proj| pbo f).presheaf.map (homOfLE le_top).op :=
  Eq.trans (by congr) <| ΓSpec.toOpen_comp_locallyRingedSpaceAdjunction_homEquiv_app _ U

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