pullbackAwayιIso_hom_SpecMap_awayMap_right

English

The preimage of a basic open under the awayι map equals the basic open of the associated localization element, i.e. awayι^{-1} (basicOpen 𝒜 g) = PrimeSpectrum.basicOpen (Away.isLocalizationElem f_deg g_deg).

Русский

Предобраз под awayι равен базовому открытому множеству соответствующего локализационного элемента: awayι^{-1}(basicOpen 𝒜 g) = PrimeSpectrum.basicOpen(Away.isLocalizationElem ...).

LaTeX

$$$\\text{awayι 𝒜 f f_deg hm }^{-1} \\text{ basicOpen 𝒜 g} = \\text{PrimeSpectrum.basicOpen}(Away.isLocalizationElem f_deg g_deg)$$$

Lean4

@[reassoc (attr := simp)]
theorem pullbackAwayιIso_hom_SpecMap_awayMap_right :
    (pullbackAwayιIso 𝒜 f_deg hm g_deg hm' hx).hom ≫
        Spec.map (CommRingCat.ofHom (awayMap 𝒜 f_deg (hx.trans (mul_comm _ _)))) =
      Limits.pullback.snd _ _ :=
  by
  rw [← cancel_mono (awayι 𝒜 g g_deg hm'), ← Limits.pullback.condition, ←
    pullbackAwayιIso_hom_awayι 𝒜 f_deg hm g_deg hm' hx, Category.assoc, SpecMap_awayMap_awayι]
  rfl

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