mem_domain_ofFromSpecStalk — Mathlib

English

If φ and h realize a morphism φ: Spec(X.presheaf.stalk x) → Y with φ ≫ sY = X.fromSpecStalk x ≫ sX, then the unique point x lies in the domain of the constructed fromFromSpecStalk.

Русский

Если φ и h реализуют морфизм φ: Spec(...) → Y с условием φ ≫ sY = X.fromSpecStalk x ≫ sX, то точка x принадлежит домену построенной fromFromSpecStalk.

LaTeX

$$$$ x \\in (\\text{ofFromSpecStalk } sX sY φ h).domain $$$$

Lean4

theorem mem_domain_ofFromSpecStalk [IrreducibleSpace X] [LocallyOfFiniteType sY] {x : X} [X.IsGermInjectiveAt x]
    (φ : Spec (X.presheaf.stalk x) ⟶ Y) (h : φ ≫ sY = X.fromSpecStalk x ≫ sX) :
    x ∈ (ofFromSpecStalk sX sY φ h).domain :=
  (spread_out_of_isGermInjective' sX sY φ h).choose_spec.choose

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