basicOpenIsoSpec_inv_ι — Mathlib

English

The composition of the open immersion awayι with the structure morphism to Spec 𝒜0 equals the canonical Spec map induced by the localization at 0.

Русский

Состав открытого вложения awayι и структуры к Spec 𝒜0 равен каноническому отображению Spec, индуцированному локализацией в 0.

LaTeX

$$awayι 𝒜 f f_deg hm ≫ toSpecZero 𝒜 = \operatorname{Spec.map}(\operatorname{ofHom}(\operatorname{fromZeroRingHom} 𝒜 _))$$

Lean4

@[reassoc]
theorem basicOpenIsoSpec_inv_ι : (basicOpenIsoSpec 𝒜 f f_deg hm).inv ≫ (Proj.basicOpen 𝒜 f).ι = awayι 𝒜 f f_deg hm :=
  rfl

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