fromSpecStalkOfMem_ι — Mathlib

English

For a fixed affine open U of X with x ∈ U, the map IsPreimmersion (X.fromSpecStalk hxU) holds, and in particular the canonical morphism is a preimmersion.

Русский

Для фиксированного аффинного открытого множества U с x ∈ U отображение является предиммерсионным.

LaTeX

$$IsPreimmersion (X.fromSpecStalk x)$$

Lean4

@[reassoc (attr := simp)]
theorem fromSpecStalkOfMem_ι {X : Scheme.{u}} (U : X.Opens) (x : X) (hxU : x ∈ U) :
    U.fromSpecStalkOfMem x hxU ≫ U.ι = X.fromSpecStalk x :=
  by
  simp only [Opens.fromSpecStalkOfMem, Spec.map_inv, Category.assoc, IsIso.inv_comp_eq]
  exact (Scheme.Spec_map_stalkMap_fromSpecStalk U.ι (x := ⟨x, hxU⟩)).symm

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