English
In any preorder context, equality of objects corresponds to equality of morphisms: eqToHom e equals homOfLE e.le.
Русский
В контексте предельного частичного порядка равенство объектов эквивалентно равенству морфизмов: eqToHom e = homOfLE e.le.
LaTeX
$$$\mathrm{eqToHom}(e) = \mathrm{homOfLE}(e.le)$$$
Lean4
/-- The stalk map of a restriction of a morphism is isomorphic to the stalk map of the original map.
-/
def morphismRestrictStalkMap {X Y : Scheme.{u}} (f : X ⟶ Y) (U : Y.Opens) (x) :
Arrow.mk ((f ∣_ U).stalkMap x) ≅ Arrow.mk (f.stalkMap x.1) :=
Arrow.isoMk' _ _
(U.stalkIso ((f ∣_ U).base x) ≪≫
(TopCat.Presheaf.stalkCongr _ <| Inseparable.of_eq <| morphismRestrict_base_coe f U x))
((f ⁻¹ᵁ U).stalkIso x) <|
by
apply TopCat.Presheaf.stalk_hom_ext
intro V hxV
change ↑(f ⁻¹ᵁ U) at x
simp [Scheme.stalkMap_germ_assoc, Scheme.Hom.appLE]
