pullbackAwayιIso_inv_fst — Mathlib

English

The open cover of Proj defined via away/multiplicative data equals the natural affine open cover determined by basic opens for the map f that sends irrelevant elements to top.

Русский

Открытое покрытие Proj, определяемое через away/множители, равно естественному аффинному открытому покрытию, задаваемому базовыми открытыми множествами для отображения f, отправляющего нерелевантный идеал в топ.

LaTeX

$$$X.\\OpenCover = X.openCoverOfIsOpenCover (\\text{fun ir} \\mapsto X.basicOpen (f ir.2.1)) hf$$$

Lean4

@[reassoc (attr := simp)]
theorem pullbackAwayιIso_inv_fst :
    (pullbackAwayιIso 𝒜 f_deg hm g_deg hm' hx).inv ≫ Limits.pullback.fst _ _ =
      Spec.map (CommRingCat.ofHom (awayMap 𝒜 g_deg hx)) :=
  by rw [← pullbackAwayιIso_hom_SpecMap_awayMap_left, Iso.inv_hom_id_assoc]

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