instIsOpenImmersionAwayι — Mathlib

English

Compatibility of Spec maps with the away open immersion: the Spec map associated to the away construction commutes with awayι.

Русский

Совместимость отображений Spec с открытым вложением away: отображение Spec, связанное с Away, коммутирует с awayι.

LaTeX

$$Spec.map (\mathrm{awayMap}\, 𝒜 g_deg hx) ≫ awayι 𝒜 f f_deg hm = awayι 𝒜 x ...$$

Lean4

instance : IsOpenImmersion (Proj.awayι 𝒜 f f_deg hm) :=
  IsOpenImmersion.comp _ _

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