basicOpenToSpec_SpecMap_awayMap — Mathlib

English

The Spec map composed with the awayMap equals the open immersion map to Proj, reflecting the compatibility of the away construction with global sections.

Русский

Отображение Spec, композиция со awayMap эквивалентно открытию в Proj, отражая совместимость Away с секциями.

LaTeX

$$Spec.map (CommRingCat.ofHom (awayMap 𝒜 g_deg hx)) ≫ awayι 𝒜 f f_deg hm = awayι 𝒜 x (...)$$

Lean4

@[reassoc]
theorem basicOpenToSpec_SpecMap_awayMap :
    basicOpenToSpec 𝒜 x ≫ Spec.map (CommRingCat.ofHom (awayMap 𝒜 g_deg hx)) =
      (Proj 𝒜).homOfLE (basicOpen_mono _ _ _ ⟨_, hx⟩) ≫ basicOpenToSpec 𝒜 f :=
  by
  rw [basicOpenToSpec, Category.assoc, ← Spec.map_comp, awayMap_awayToSection, Spec.map_comp,
    Scheme.Opens.toSpecΓ_SpecMap_map_assoc]
  rfl

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