Stalk homomorphisms agreeing modulo an ideal on the coordinates agree on all germs

Kollár's proof of the uniqueness of blow-up sequences checks the agreement of the two lifts f', g' on V(M_{i+1}) on the pulled-back coordinates y_j of a chart of the blow-up [Kol07, Theorem 97, proof]. This module is the passage from the coordinates to every germ, for two local ring homomorphisms F, G : 𝒪_{M,a} → 𝒪_{N,b} preserving the constants (the two pull-backs f'^*, g'^*) and an ideal K ⊆ 𝒪_{N,b}: if F x_i − G x_i ∈ K for the coordinate germs x_i of a chart at a, then F s − G s ∈ K for every germ s (sub_mem_of_forall_coord_sub_mem).

The proof is Hadamard's lemma iterated against Krull's intersection theorem: writing s = s(a) + ∑ (x_i − x_i(a)) g_i (exists_eq_sum_coord_mul'), F s − G s = ∑ (F x_i − G x_i) F g_i + ∑ G(x_i − x_i(a)) (F g_i − G g_i); the first sum lies in K, the second in 𝔪_b · (K + 𝔪_b^N) once F g_i − G g_i ∈ K + 𝔪_b^N (induction on N), so F s − G s ∈ K + 𝔪_b^{N+1} for every N, and ⋂_N (K + 𝔪_b^N) = K in the Noetherian local ring 𝒪_{N,b} (isNoetherianRing_stalk; Krull's intersection theorem [Kol07, Definition 55] in the form IsLocalRing.mem_of_forall_mem_sup_pow).

theorem Hironaka.Manifold.sub_mem_of_forall_coord_sub_mem {𝕜 : Type} [RCLike 𝕜] (E : Type u_1) [NormedAddCommGroup E] [NormedSpace 𝕜 E] {M : Type u} [TopologicalSpace M] [ChartedSpace E M] {n : ℕ} (ψ : E ≃L[𝕜] Fin n → 𝕜) (φ : OpenPartialHomeomorph M E) {a : M} (ha : a ∈ φ.source) (hφ : φ ∈ IsManifold.maximalAtlas (modelWithCornersSelf 𝕜 E) ⊤ M) {N : Type u} [TopologicalSpace N] [ChartedSpace E N] [IsManifold (modelWithCornersSelf 𝕜 E) ⊤ N] [FiniteDimensional 𝕜 E] {b : N} (F G : ↑((Manifold.structureSheaf 𝕜 E M).presheaf.stalk a) →+* ↑((Manifold.structureSheaf 𝕜 E N).presheaf.stalk b)) [IsLocalHom G] (hF : ∀ (c : 𝕜), F ((Manifold.const 𝕜 E M a) c) = (Manifold.const 𝕜 E N b) c) (hG : ∀ (c : 𝕜), G ((Manifold.const 𝕜 E M a) c) = (Manifold.const 𝕜 E N b) c) (K : Ideal ↑((Manifold.structureSheaf 𝕜 E N).presheaf.stalk b)) (hK : ∀ (i : Fin n), F (Manifold.coord E ψ φ hφ ha i) - G (Manifold.coord E ψ φ hφ ha i) ∈ K) (s : ↑((Manifold.structureSheaf 𝕜 E M).presheaf.stalk a)) : F s - G s ∈ K

Two ring homomorphisms of stalks F, G : 𝒪_{M,a} → 𝒪_{N,b} preserving the constants, G local, which agree modulo an ideal K on the coordinate germs of a chart at a, agree modulo K on every germ (the passage from the coordinates to all germs in [Kol07, Theorem 97, proof]): Hadamard's lemma iterated against Krull's intersection theorem in the Noetherian local ring 𝒪_{N,b}.