Morphisms out of a non-singular space are determined on a dense open subset

Two K-morphisms h₁ h₂ : A ⟶ Y of analytic K-spaces with A non-singular that agree after restriction to a dense open subspace A|_D are equal (AnalyticSpace.hom_ext_of_dense). This is the rigidity behind the uniqueness of the lift of a local analytic isomorphism to the resolutions ([Wlo09, Theorem 2.0.1 (3)]: the lift is "natural"; [Kol07, Theorem 45 (5)]): two lifts agree over the simple locus, where the resolution is an isomorphism, which is a dense open subset of the resolving manifold. Not stated in the sources; the argument:

• Sections (AnalyticSpace.eq_zero_of_pullbackΓ_ofRestrict_eq_zero_of_dense): a global section of a non-singular space Z whose restriction to a dense open D vanishes is zero. Near a point, Z is K-isomorphic to an open subspace (G, 𝒜_G) of Kⁿ (Hironaka's characterization of the simple points [Hir64, Ch. 0, §1, p. 121], isRegular_stalk_iff_exists_manifold_nhd), whose sections are analytic functions (Manifold.structureSheaf); the transported section is a continuous function vanishing on a dense subset of its domain, hence zero (Set.EqOn.of_subset_closure), so the germ of the section at the point vanishes, the stalk map of the chart being injective. Over ℝ the non-singularity cannot be weakened to reducedness: the reduced space x(x² + y²) = 0 near the origin of ℝ² has support the line x = 0, and the section x vanishes on the complement of the origin, where x² + y² is a unit, but not at the origin.
• Morphisms (AnalyticSpace.hom_ext_of_dense): the base maps agree, being continuous into a Hausdorff space and equal on a dense set (Continuous.ext_on). Equality of morphisms is local on the source (hom_ext_of_cover); near a point of A the target is a local model L ⊆ Kᵐ (exists_kIso_localModel), so both morphisms factor through Y|_U ≅ L ⟶ (Kᵐ, 𝒜), and a morphism into (Kᵐ, 𝒜) from a space with Noetherian stalks is determined by the pull-backs of the m coordinate functions (hom_ext_of_coord), global sections of the non-singular open subspace which agree on the dense open subset; the embedding of the model is a monomorphism (eq_of_comp_localModel_ι_eq).

theorem AnalyticSpace.isNonsingular_restrictOpen {K : Type} [RCLike K] {X : AnalyticSpace K} (hX : X.IsNonsingular) (U : TopologicalSpace.Opens ↑↑X.toPresheafedSpace) : (X.restrictOpen U).IsNonsingular

An open subspace of a non-singular analytic K-space is non-singular: the stalks are those of the space (isRegularLocalRing_stalk_restrictOpen_iff).

theorem AnalyticSpace.dense_preimage_toFun_ofRestrict {K : Type} [RCLike K] (X : KLocallyRingedSpace K) (U : TopologicalSpace.Opens ↑↑X.toPresheafedSpace) {D : Set ↑↑X.toPresheafedSpace} (hD : Dense D) : Dense (KLocallyRingedSpace.Hom.toFun (X.ofRestrict U) ⁻¹' D)

The preimage of a dense set under the open immersion X|_U ⟶ X is dense.

Sections of the model (G, 𝒜_G)

theorem AnalyticSpace.eq_zero_of_pullbackΓ_ofRestrict_eq_zero_of_dense_analyticSpaceOfOpen {K : Type} [RCLike K] {n : ℕ} (G : TopologicalSpace.Opens (Kn K n)) (O : TopologicalSpace.Opens ↑↑(analyticSpaceOfOpen K n G).toPresheafedSpace) (hO : Dense ↑O) (t : ↑(AlgebraicGeometry.LocallyRingedSpace.Γ.obj (Opposite.op (analyticSpaceOfOpen K n G).toLocallyRingedSpace))) (ht : (KLocallyRingedSpace.Hom.pullbackΓ ((analyticSpaceOfOpen K n G).ofRestrict O)) t = 0) : t = 0

A global section of (G, 𝒜_G) — an analytic function on G — whose restriction to a dense open subset O ⊆ G is zero is zero: it is a continuous function vanishing on a dense subset of its domain (Set.EqOn.of_subset_closure).

Sections of a non-singular space

theorem AnalyticSpace.eq_zero_of_pullbackΓ_ofRestrict_eq_zero_of_dense {K : Type} [RCLike K] {Z : AnalyticSpace K} (hZ : Z.IsNonsingular) (D : TopologicalSpace.Opens ↑↑Z.toPresheafedSpace) (hD : Dense ↑D) (s : ↑(AlgebraicGeometry.LocallyRingedSpace.Γ.obj (Opposite.op Z.toLocallyRingedSpace))) (hs : (KLocallyRingedSpace.Hom.pullbackΓ (Z.ofRestrict D)) s = 0) : s = 0

A global section of a non-singular analytic K-space Z whose restriction to a dense open D is zero is zero.

Morphisms

theorem AnalyticSpace.hom_ext_of_dense_affine {K : Type} [RCLike K] {Z : AnalyticSpace K} (hZ : Z.IsNonsingular) (D : TopologicalSpace.Opens ↑↑Z.toPresheafedSpace) (hD : Dense ↑D) {m : ℕ} (g₁ g₂ : Z.toKLocallyRingedSpace ⟶ affine K m) (h : CategoryTheory.CategoryStruct.comp (Z.ofRestrict D) g₁ = CategoryTheory.CategoryStruct.comp (Z.ofRestrict D) g₂) : g₁ = g₂

Two K-morphisms from a non-singular analytic K-space into (Kᵐ, 𝒜_{Kᵐ}) that agree on a dense open subspace are equal: the pull-backs of the coordinate functions agree on the dense open (eq_zero_of_pullbackΓ_ofRestrict_eq_zero_of_dense at their difference), and a morphism into (Kᵐ, 𝒜_{Kᵐ}) is determined by them (hom_ext_of_coord).

theorem AnalyticSpace.hom_ext_of_dense {K : Type} [RCLike K] {A Y : AnalyticSpace K} (hA : A.IsNonsingular) (D : TopologicalSpace.Opens ↑↑A.toPresheafedSpace) (hD : Dense ↑D) (h₁ h₂ : A ⟶ Y) (h : CategoryTheory.CategoryStruct.comp (A.ofRestrict D) h₁ = CategoryTheory.CategoryStruct.comp (A.ofRestrict D) h₂) : h₁ = h₂

Morphisms out of a non-singular space are determined on a dense open subset: two K-morphisms h₁ h₂ : A ⟶ Y of analytic K-spaces with A non-singular that agree after restriction to a dense open D ⊆ A are equal. The base maps agree by continuity; near each point the target is a local model L ⊆ Kᵐ and both morphisms, restricted to the preimage of the model neighbourhood (a non-singular open subspace in which D is dense), are determined by their composites with Y|_U ≅ L ⟶ (Kᵐ, 𝒜), which agree by hom_ext_of_dense_affine.