From (91.1)–(91.4) at the completion to (1′)–(4′) on a neighbourhood

In the proof of Theorem 92 ([Kol07, 95]) 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)". For an étale neighbourhood pair ψ, ψ' : W ⇉ X of p whose automorphism φ = θ⁻¹ = (ψ̂^*)⁻¹ ∘ ψ̂'^* of Ô_{X,p} satisfies the conditions (91.1)–(91.4) of [Kol07, Definition 91], this file produces an open V ∋ q of W with (1′) ψ⁻¹(H) = ψ'⁻¹(H'), (2′) ψ^*I = ψ'^*I, (3′) ψ⁻¹(Eⁱ) = ψ'⁻¹(Eⁱ) and (4′) ψ = ψ' on V(MC(ψ^*I)): the hypotheses of formallyEquivalentAt_of_etaleNbhdPair for the restricted pair, and the summand conditions of the disjoint union in Hironaka/Resolution/Algebraic/MaximalContact/EtaleEquivSigma.lean.

• (1′)–(3′): φ(Ĵ') = Ĵ transports along ψ̂^* (map_completionMap_stalkHom, ψ̂^* ∘ φ = ψ̂'^*) to (ψ^*J)^_q = (ψ'^*J')^_q, and Kollár's appeal to [Kol07, Definition 55] (exists_comap_eq_of_map_adicCompletion_eq) spreads the equality of completions to an open neighbourhood; the finitely many opens (one for H, one for I, one per component of E) are intersected.
• (4′): h − φ(h) ∈ \widehat{MC(I)} gives ψ̂^*(x) − ψ̂'^*(x) ∈ (ψ^*MC(I))^_q, and exists_agreeOn_of_forall_completionMap_sub_mem (the equalizer argument) gives an open on which ψ, ψ' agree on V(ψ^*MC(I)); MC(ψ^*I) = ψ^*MC(I) is [Kol07, Lemma 74 (4)] (MC_comap_of_etale).
• Restriction to a smaller open: equalities of pulled-back ideal sheaves restrict along V ⊆ V₁ by comap_comp; AgreeOn restricts because V(M|_V) = V(M|_{V₁}) ×_{V₁} V (AgreeOn.restrict_of_le, the pullback square AlgebraicGeometry.isPullback_subschemeι_comap).

theorem AlgebraicGeometry.Scheme.IdealSheafData.comap_ι_eq_of_le {W : Scheme} {J J' : W.IdealSheafData} {V V₁ : W.Opens} (hle : V ≤ V₁) (h : J.comap V₁.ι = J'.comap V₁.ι) : J.comap V.ι = J'.comap V.ι

An equality of ideal sheaves on an open V₁ restricts to every open V ⊆ V₁.

theorem AlgebraicGeometry.Scheme.IdealSheafData.AgreeOn.restrict_of_le {W X : Scheme} (ψ ψ' : W ⟶ X) (M : W.IdealSheafData) {V V₁ : W.Opens} (hle : V ≤ V₁) (h : AgreeOn (CategoryTheory.CategoryStruct.comp V₁.ι ψ) (CategoryTheory.CategoryStruct.comp V₁.ι ψ') (M.comap V₁.ι)) : AgreeOn (CategoryTheory.CategoryStruct.comp V.ι ψ) (CategoryTheory.CategoryStruct.comp V.ι ψ') (M.comap V.ι)

Agreement of ψ, ψ' on V(M) over an open V₁ restricts to every open V ⊆ V₁: V(M|_V) is the pullback of V(M|_{V₁}) along V ⟶ V₁ (AlgebraicGeometry.isPullback_subschemeι_comap).

theorem AlgebraicGeometry.Scheme.IdealSheafData.exists_opens_conditions_of_formalAutomorphism {k : Type u} [Field k] {X : Scheme} (f : X ⟶ Spec ↧k) [Smooth f] (I : X.IdealSheafData) (m : ℕ) (E : X.DivisorFamily) (H H' : X.IdealSheafData) {p : ↥X} (Q : EtaleNbhdPair X p) (ha : Function.Bijective ⇑(IsLocalRing.completionMap Q.stalkHom)) (ha' : Function.Bijective ⇑(IsLocalRing.completionMap Q.stalkHom')) (h1 : Ideal.map (Q.formalAutomorphism ha ha').symm (H'.completionIdeal p) = H.completionIdeal p) (h2 : Ideal.map (Q.formalAutomorphism ha ha').symm (I.completionIdeal p) = I.completionIdeal p) (h3 : ∀ (i : E.ι), Ideal.map (Q.formalAutomorphism ha ha').symm ((E.component i).completionIdeal p) = (E.component i).completionIdeal p) (h4 : ∀ (h : AdicCompletion (IsLocalRing.maximalIdeal ↑(X.presheaf.stalk p)) ↑(X.presheaf.stalk p)), h - (Q.formalAutomorphism ha ha').symm h ∈ (MC f I m).completionIdeal p) : ∃ (V : Q.W.Opens), Q.q ∈ V ∧ H.comap (CategoryTheory.CategoryStruct.comp V.ι Q.ψ) = H'.comap (CategoryTheory.CategoryStruct.comp V.ι Q.ψ') ∧ I.comap (CategoryTheory.CategoryStruct.comp V.ι Q.ψ) = I.comap (CategoryTheory.CategoryStruct.comp V.ι Q.ψ') ∧ (∀ (i : E.ι), (E.component i).comap (CategoryTheory.CategoryStruct.comp V.ι Q.ψ) = (E.component i).comap (CategoryTheory.CategoryStruct.comp V.ι Q.ψ')) ∧ AgreeOn (CategoryTheory.CategoryStruct.comp V.ι Q.ψ) (CategoryTheory.CategoryStruct.comp V.ι Q.ψ') (MC (CategoryTheory.CategoryStruct.comp (CategoryTheory.CategoryStruct.comp V.ι Q.ψ) f) (I.comap (CategoryTheory.CategoryStruct.comp V.ι Q.ψ)) m)

Kollár's "(91.1′–4′) also hold in an open neighborhood U(p) ∋ (p, p) by (55)" ([Kol07, 95]): for an étale neighbourhood pair Q of p whose automorphism φ = θ⁻¹ satisfies (91.1)–(91.4) at p, there is an open V ∋ q in W on which (1′) ψ⁻¹(H) = ψ'⁻¹(H'), (2′) ψ^*I = ψ'^*I, (3′) ψ⁻¹(Eⁱ) = ψ'⁻¹(Eⁱ) for every i, and (4′) ψ and ψ' agree on V(MC(ψ^*I)). (1′)–(3′) by spreading out equalities of completions after the transports map_completionMap_stalkHom('), intersecting the finitely many opens; (4′) by exists_agreeOn_of_forall_completionMap_sub_mem with [Kol07, Lemma 74 (4)].