English
Two scheme morphisms f,g:X→Y are equal if their base maps are equal and their action on all opens is equal when transported along the structure sheaf.
Русский
Два морфизма схем f,g:X→Y равны, если их базовые отображения совпадают и их действия на всех открытых множеств совпадают при переносе поSheaf.
LaTeX
$$Eq f g := (f.base = g.base) ∧ (∀ U, f.app U ≫ X.presheaf.map (eqToHom ⋯).op = g.app U)$$
Lean4
protected theorem ext {f g : X ⟶ Y} (h_base : f.base = g.base)
(h_app : ∀ U, f.app U ≫ X.presheaf.map (eqToHom congr((Opens.map $h_base.symm).obj U)).op = g.app U) : f = g :=
by
cases f; cases g; congr 1
exact LocallyRingedSpace.Hom.ext' <| SheafedSpace.ext _ _ h_base (TopCat.Presheaf.ext fun U ↦ by simpa using h_app U)
