English
If φ and h realize a morphism φ: Spec(X.presheaf.stalk x) → Y with φ ≫ sY = X.fromSpecStalk x ≫ sX, then the constructed fromFromSpecStalk morphism satisfies certain equalities with its domain and target restrictions.
Русский
Если φ и h реализуют морфизм φ: Spec(... stalk ...) → Y с условием φ ≫ sY = X.fromSpecStalk x ≫ sX, то построенный morphism fromFromSpecStalk удовлетворяет определенным равенствам на домене и ограничениях.
LaTeX
$$$$ (ofFromSpecStalk sX sY φ h).hom \\;\\text{ и }\\; (ofFromSpecStalk sX sY φ h).domain.ι \\text{ удовлетворяют } (hom) \\gg sY = (domain.ι) \\gg sX $$$$
Lean4
theorem ofFromSpecStalk_comp [IrreducibleSpace X] [LocallyOfFiniteType sY] {x : X} [X.IsGermInjectiveAt x]
(φ : Spec (X.presheaf.stalk x) ⟶ Y) (h : φ ≫ sY = X.fromSpecStalk x ≫ sX) :
(ofFromSpecStalk sX sY φ h).hom ≫ sY = (ofFromSpecStalk sX sY φ h).domain.ι ≫ sX :=
(spread_out_of_isGermInjective' sX sY φ h).choose_spec.choose_spec.choose_spec.2
