Equality of morphisms of locally ringed spaces is local on the source

Two morphisms of locally ringed spaces that agree after restriction to every member of an open cover of the source are equal: their base maps agree pointwise, and their stalk maps agree because the stalk map of a composite is the composite of the stalk maps (stalkMap_comp) and the stalk map of the open immersion X | U → X is an isomorphism, so Mathlib's SheafedSpace.hom_stalk_ext applies. The K-morphism form follows since the K-condition is a proposition (Hom.ext). This is the uniqueness half of the gluing of morphisms along an open cover (Hironaka/AnalyticSpace/HomGlue.lean is the existence half), used for the uniqueness of the lift in Hironaka's universal mapping property (**) of a monoidal transformation [Hir64, Ch. 0, §2]: a lift is determined locally.

Stated for general locally ringed spaces and K-local-ringed spaces. Mathlib has LocallyRingedSpace.GlueData, IsOpenImmersion.lift and TopCat.Sheaf.existsUnique_gluing' but no locality lemma for morphisms out of a space covered by opens; SheafedSpace.hom_stalk_ext is the ingredient.

theorem AnalyticSpace.LocallyRingedSpace.hom_ext_of_cover {X Y : AlgebraicGeometry.LocallyRingedSpace} (f g : X ⟶ Y) {ι : Type u_1} (U : ι → TopologicalSpace.Opens ↑X.toTopCat) (hU : ∀ (x : ↑X.toTopCat), ∃ (i : ι), x ∈ U i) (h : ∀ (i : ι), CategoryTheory.CategoryStruct.comp (X.ofRestrict ⋯) f = CategoryTheory.CategoryStruct.comp (X.ofRestrict ⋯) g) : f = g

Equality of morphisms of locally ringed spaces is local on the source: if f and g agree after restriction to every member of an open cover, they are equal.

theorem AnalyticSpace.KLocallyRingedSpace.hom_ext_of_cover {K : Type} [RCLike K] {X Y : KLocallyRingedSpace K} (f g : X ⟶ Y) {ι : Type u_1} (U : ι → TopologicalSpace.Opens ↑↑X.toPresheafedSpace) (hU : ∀ (x : ↑↑X.toPresheafedSpace), ∃ (i : ι), x ∈ U i) (h : ∀ (i : ι), CategoryTheory.CategoryStruct.comp (X.ofRestrict (U i)) f = CategoryTheory.CategoryStruct.comp (X.ofRestrict (U i)) g) : f = g

Equality of K-morphisms is local on the source: K-morphisms that agree after restriction to every member of an open cover are equal (Hom.ext and the locally-ringed-space statement).