fromSpecStalkOfMem_ofFromSpecStalk

English

Under the given φ and h, the specialization yields φ back from the constructed fromFromSpecStalk.

Русский

При заданных φ и h получаем, что специализация возвращает φ через построенную fromFromSpecStalk.

LaTeX

$$$$ (ofFromSpecStalk sX sY φ h).fromSpecStalkOfMem (mem_domain_ofFromSpecStalk sX sY φ h) = φ $$$$

Lean4

theorem fromSpecStalkOfMem_ofFromSpecStalk [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).fromSpecStalkOfMem (mem_domain_ofFromSpecStalk sX sY φ h) = φ :=
  (spread_out_of_isGermInjective' sX sY φ h).choose_spec.choose_spec.choose_spec.1.symm

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