SpecMap_awayMap_awayι — Mathlib

English

The pullback of the open immersions awayι at f and g is isomorphic to the affine open D_+(fg) lying over the sum of degrees m and m'.

Русский

Вычисление вытяжки открытых вложений Away: равенство близкое к открытому D_+(fg) над суммой степеней m и m'.

LaTeX

$$pullbackAwayιIso 𝒜 f_deg hm g_deg hm' hx ≅ Spec (.of <| Away 𝒜 x)$$

Lean4

@[reassoc]
theorem SpecMap_awayMap_awayι :
    Spec.map (CommRingCat.ofHom (awayMap 𝒜 g_deg hx)) ≫ awayι 𝒜 f f_deg hm =
      awayι 𝒜 x (hx ▸ SetLike.mul_mem_graded f_deg g_deg) (hm.trans_le (m.le_add_right m')) :=
  by
  rw [awayι, awayι, Iso.eq_inv_comp, basicOpenIsoSpec_hom, basicOpenToSpec_SpecMap_awayMap_assoc, ←
    basicOpenIsoSpec_hom _ _ f_deg hm, Iso.hom_inv_id_assoc, Scheme.homOfLE_ι]

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