English
The right-hand side of resLE maps respects refinement of open sets: refining U to U' yields a transitive refinement of the restriction map.
Русский
Правый член restrict map сохраняет смену открытых множеств: уточнение U до U' порождает переходное уточнение отображения ограничения.
LaTeX
$$$\mathrm{map\_resLE}(i) : X.homOfLE(i) \circ f.resLE U V e = f.resLE U' V (i.trans e)$$$
Lean4
/-- The stalk map of `f.resLE U V` at `x : V` is the stalk map of `f` at `x`. -/
def resLEStalkMap (x : V) : Arrow.mk ((f.resLE U V e).stalkMap x) ≅ Arrow.mk (f.stalkMap x) :=
Arrow.isoMk (U.stalkIso _ ≪≫ (Y.presheaf.stalkCongr <| Inseparable.of_eq <| by simp)) (V.stalkIso x) <|
by
dsimp
rw [Category.assoc, ← Iso.eq_inv_comp, ← Category.assoc, ← Iso.comp_inv_eq, Opens.stalkIso_inv, Opens.stalkIso_inv,
← stalkMap_comp, stalkMap_congr_hom _ _ (resLE_comp_ι f e), stalkMap_comp]
simp
