instIsOverMapStalkSpecializesCommRingCatPresheaf

English

As in the first specialization lemma, for x ⤳ y one has Spec.map of the stalk specialization map composed with fromSpecStalk y equals fromSpecStalk x.

Русский

Как и в первом лемме специализации, для x ⤳ y выполняется равенство Spec.map stalkSpecializes ∘ fromSpecStalk y = fromSpecStalk x.

LaTeX

$$Spec.map (X.presheaf.stalkSpecializes h) ≫ X.fromSpecStalk y = X.fromSpecStalk x$$

Lean4

instance {x y : X} (h : x ⤳ y) : (Spec.map (X.presheaf.stalkSpecializes h)).IsOver X where

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