Agreement on a closed analytic subspace: set-level consequences

AgreeOnSubspace ψ ψ' J (Hironaka/Resolution/Analytic/LocalIsoEquiv.lean), the analytic form of condition (4′) of Kollár's étale equivalence [Kol07, Definition 91], says ψ^*h − ψ'^*h ∈ J_u for every local section h near ψ u and ψ' u. Its set-level content: on the closed analytic subspace V(J) = {u | J_u ≠ 𝒪_{U,u}} the two maps coincide (AgreeOnSubspace.apply_eq_of_mem_support) — if ψ u ≠ ψ' u, a locally constant analytic section on the union of two disjoint neighbourhoods, 1 near ψ u and 0 near ψ' u, has ψ^*h − ψ'^*h = 1 ∈ J_u. This is the step "ψ_i|_{W_i} = ψ'_i|_{W_i}, thus Z_i = ψ_i(Z^U_i) = ψ'_i(Z^U_i) = Z'_i" of Kollár's proof of the uniqueness of blow-up sequences [Kol07, Theorem 97, proof]. Also the symmetry of the relation and its monotonicity in J.

theorem Hironaka.Manifold.AgreeOnSubspace.symm {𝕜 : Type} [RCLike 𝕜] {E : Type v} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {U M : AnalyticManifold 𝕜 E} {ψ ψ' : AnalyticMap U M} {J : U.IdealSheaf} (h : AgreeOnSubspace ψ ψ' J) : AgreeOnSubspace ψ' ψ J

theorem Hironaka.Manifold.AgreeOnSubspace.mono {𝕜 : Type} [RCLike 𝕜] {E : Type v} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {U M : AnalyticManifold 𝕜 E} {ψ ψ' : AnalyticMap U M} {J J' : U.IdealSheaf} (h : AgreeOnSubspace ψ ψ' J) (hJ : J ≤ J') : AgreeOnSubspace ψ ψ' J'

theorem Hironaka.Manifold.germMap_germ_eq_const_of_eventuallyEq {𝕜 : Type} [RCLike 𝕜] {E : Type v} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {U M : AnalyticManifold 𝕜 E} {ψ : AnalyticMap U M} {W : TopologicalSpace.Opens M.carrier} {u : U.carrier} (hu : ψ u ∈ W) (f : ↑((Manifold.structureSheaf 𝕜 E M.carrier).presheaf.obj (Opposite.op W))) {c : 𝕜} (hf : ∀ᶠ (x : M.carrier) in nhds (ψ u), Manifold.extendSection 𝕜 E f x = c) : (Manifold.germMap ⇑ψ ⋯ u) ((CategoryTheory.ConcreteCategory.hom ((Manifold.structureSheaf 𝕜 E M.carrier).presheaf.germ W (ψ u) hu)) f) = (Manifold.const 𝕜 E U.carrier u) c

The germ at u of a section that is constant near ψ u pulls back to the constant germ.

theorem Hironaka.Manifold.AgreeOnSubspace.apply_eq_of_mem_support {𝕜 : Type} [RCLike 𝕜] {E : Type v} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {U M : AnalyticManifold 𝕜 E} {ψ ψ' : AnalyticMap U M} {J : U.IdealSheaf} (h : AgreeOnSubspace ψ ψ' J) {u : U.carrier} (hu : u ∈ Manifold.IdealSheaf.support J) : ψ u = ψ' u

Kollár's "ψ_i|_{W_i} = ψ'_i|_{W_i}" [Kol07, Theorem 97, proof]: two maps agreeing on the closed analytic subspace V(J) coincide at every point of V(J).