From agreement on a completed stalk to agreement on a neighbourhood

In the proof of Theorem 92 ([Kol07, 95]) Kollár passes from the completion to a neighbourhood: the conditions (91.1)–(91.4) hold after completion at (p, p), so "(91.1′–4′) also hold in an open neighborhood U(p) ∋ (p, p) by (55)". Conditions (1′)–(3′) are equalities of ideal sheaves, spread out by exists_comap_eq_of_map_adicCompletion_eq. Condition (4′) is the equality of two morphisms ψ, ψ' on the closed subscheme V(M), M = MC(ψ^*I); this file spreads it out from the completion at q. The argument (not in the sources; Kollár's appeal to [Kol07, Definition 55] applied to the equalizer):

1. faithful flatness of the completion descends ψ̂^*(x) − ψ̂'^*(x) ∈ M̂_q to ψ^*(s) − ψ'^*(s) ∈ M_q, so the two composites g, g' : V(M) ⇉ X have the same stalk map at the point z over q (the stalk map of V(M) → W at z has kernel M_q);
2. two morphisms with the same stalk map at z agree after composing with Spec 𝒪_{V(M),z} → V(M) (fromSpecStalk_comp_eq_of_stalkMap_eq, Mathlib's SpecMap_stalkMap_fromSpecStalk), so Spec 𝒪_{V(M),z} lifts to their equalizer E;
3. the equalizer of two morphisms of schemes is an immersion (Mathlib), i.e. a closed subscheme of an open coborder(E) ⊆ V(M); the lift makes z a point of E at which the stalk map of the immersion is bijective, so the kernel of the closed part E → coborder(E) has zero stalk at z and vanishes on an open neighbourhood (V(M) is locally Noetherian); over that open the closed immersion is an isomorphism (isIso_iff_ker_eq_bot), giving an open immersion j into V(M) through z with j ≫ g = j ≫ g' (exists_openImmersion_comp_eq_of_lift);
4. the open subset range j of the closed V(M) is the trace of an open V ⊆ W; the subscheme V(M|_V) = V(M) ×_W V factors through j, hence ψ = ψ' on it (AgreeOn).

If q ∉ V(M), the complement of V(M) is the neighbourhood and V(M|_V) = ∅.

No hypothesis on the k-structures of ψ, ψ' is needed: the argument never chooses generators.

theorem AlgebraicGeometry.Scheme.IdealSheafData.agreeOn_top {X U : Scheme} (ψ ψ' : U ⟶ X) : AgreeOn ψ ψ' ⊤

Every pair of morphisms agrees on the empty subscheme V(⊤).

theorem AlgebraicGeometry.Scheme.IdealSheafData.fromSpecStalk_comp_eq_of_stalkMap_eq {X T : Scheme} (g g' : T ⟶ X) (t : ↥T) {p : ↥X} (h : g t = p) (h' : g' t = p) (hst : ∀ (s : ↑(X.presheaf.stalk p)), (CommRingCat.Hom.hom (Hom.stalkMap g t)) ((CategoryTheory.ConcreteCategory.hom (X.presheaf.stalkCongr ⋯).hom) s) = (CommRingCat.Hom.hom (Hom.stalkMap g' t)) ((CategoryTheory.ConcreteCategory.hom (X.presheaf.stalkCongr ⋯).hom) s)) : CategoryTheory.CategoryStruct.comp (T.fromSpecStalk t) g = CategoryTheory.CategoryStruct.comp (T.fromSpecStalk t) g'

Two morphisms g, g' : T ⟶ X with the same image point and the same stalk map at t agree after composing with the canonical Spec 𝒪_{T,t} ⟶ T (Mathlib's SpecMap_stalkMap_fromSpecStalk, with the stalks transported along the two image-point equalities).

theorem AlgebraicGeometry.Scheme.IdealSheafData.exists_openImmersion_comp_eq_of_lift {X Z : Scheme} [IsLocallyNoetherian Z] {E : Scheme} (e : E ⟶ Z) [IsImmersion e] (g g' : Z ⟶ X) (hcond : CategoryTheory.CategoryStruct.comp e g = CategoryTheory.CategoryStruct.comp e g') (z : ↥Z) (l : Spec (Z.presheaf.stalk z) ⟶ E) (hl : CategoryTheory.CategoryStruct.comp l e = Z.fromSpecStalk z) : ∃ (T : Scheme) (j : T ⟶ Z), IsOpenImmersion j ∧ z ∈ Set.range ⇑j ∧ CategoryTheory.CategoryStruct.comp j g = CategoryTheory.CategoryStruct.comp j g'

The core of the spreading-out argument, on an arbitrary locally Noetherian scheme Z: an immersion e : E ⟶ Z equalizing g, g' : Z ⟶ X, together with a lift of Spec 𝒪_{Z,z} ⟶ Z through e, yields an open immersion j into Z whose image contains z and on which g = g'. Route: the closed part E → coborder(E) of the immersion has a kernel with zero stalk at z (the lift makes the stalk map of e at the point over z injective), hence vanishing on an open neighbourhood (Krull's intersection theorem, exists_comap_eq_of_stalkIdeal_eq), over which the closed immersion is an isomorphism (IsClosedImmersion.isIso_iff_ker_eq_bot).

theorem AlgebraicGeometry.Scheme.IdealSheafData.exists_agreeOn_of_forall_completionMap_sub_mem {k : Type u} [Field k] {X : Scheme} (f : X ⟶ Spec ↧k) [LocallyOfFiniteType f] {p : ↥X} (Q : EtaleNbhdPair X p) (M : Q.W.IdealSheafData) (h : ∀ (x : AdicCompletion (IsLocalRing.maximalIdeal ↑(X.presheaf.stalk p)) ↑(X.presheaf.stalk p)), (IsLocalRing.completionMap Q.stalkHom) x - (IsLocalRing.completionMap Q.stalkHom') x ∈ M.completionIdeal Q.q) : ∃ (V : Q.W.Opens), Q.q ∈ V ∧ AgreeOn (CategoryTheory.CategoryStruct.comp V.ι Q.ψ) (CategoryTheory.CategoryStruct.comp V.ι Q.ψ') (M.comap V.ι)

Kollár's "(91.1′–4′) also hold in an open neighborhood U(p) ∋ (p, p) by (55)" ([Kol07, 95]), for the condition (4′): for an étale neighbourhood pair Q of p and an ideal sheaf M on W, if ψ̂^*(x) − ψ̂'^*(x) ∈ M̂_q for every x ∈ Ô_{X,p}, then there is an open V ∋ q on which ψ and ψ' agree on the closed subscheme V(M|_V) (AgreeOn). Faithful flatness descends the hypothesis to the stalk; the two composites V(M) ⇉ X then agree on the stalk at the point over q, so q lies in their equalizer with an isomorphic stalk there, and the equalizer contains an open neighbourhood of q in V(M) because W is locally Noetherian (exists_openImmersion_comp_eq_of_lift).