Morphisms of non-singular analytic K-spaces are determined by their underlying maps #
hom_ext_toFun_of_isNonsingular: two K-morphisms f g : X ⟶ Y of analytic K-spaces with X
and Y non-singular (IsNonsingular: every stalk a regular local ring) and the same underlying
map are equal — compare the local Kⁿ-coordinations of [Hir64, Ch. 0, §1, p. 120], through
which a morphism is read off its coordinate functions; the manifold case is hom_ext_baseFun
(Hironaka/AnalyticSpace/Manifold/FullyFaithful.lean). Used for the uniqueness of the local
resolution over a piece (Hironaka/Resolution/Analytic/Kol07Thm45/LocalResolutionIndependent.lean;
the uniqueness in the proof of [Kol07, Theorem 36] and in [Wlo09, Theorem 6.0.6 (1)]): two
morphisms of local resolutions over the piece agree on a dense open, hence on points, hence as
morphisms.
Why non-singular, not reduced. Over ℝ the reduced singular space Y = V(x(x² + y²)) ⊂ ℝ² has
real points the line {x = 0}, and the section x vanishes on the dense open Y ∖ {0} yet is
nonzero in 𝒪_{Y,0}; "agreeing on a dense open" does not determine a morphism out of such a
source. On a non-singular space the sections are analytic functions on charts, determined by their
values, over ℝ as over ℂ.
Proof. Equality of K-morphisms is local on the source (hom_ext_of_cover). X is covered by
its dimension strata X_d = dimOpens X hX d (iUnion_dimSet_eq_univ,
Hironaka/AnalyticSpace/Manifold/Stratum.lean), each the space of an analytic manifold through the
comparison isomorphism stratumKIso : Sp(X_d) ≅ X | X_d
(Hironaka/AnalyticSpace/Manifold/StratumIso.lean) whose base map is the identity on points.
Composing with it, f and g become two morphisms F, G : Sp(X_d) ⟶ Y with the same base map.
Sp(X_d) is covered by the preimages P = F⁻¹(Y_{d'}) of the strata of Y; on P both F and
G factor through the open immersion Y | Y_{d'} → Y as their restrictions Hom.restrictTo
(restrictTo_comp_ofRestrict), and the restrictions, read between the manifold spaces
Sp(P) ≅ Sp(X_d) | P (ofManifold_restrictOpen_iso) and Sp(Y_{d'}) ≅ Y | Y_{d'} (stratumKIso),
are morphisms of manifold spaces with the same underlying map (Hom.toFun_restrictTo, the base
lemmas of the two isomorphisms), hence equal by hom_ext_baseFun; cancelling the isomorphisms
gives the equality of the restrictions, and the two open-cover arguments give f = g. Routine.
The base map of the inverse of the stratum isomorphism Sp(X_d) ≅ X | X_d is the identity on
points (its hom is stratumHom, whose base map is the identity, stratumHom_base_apply).
The inverse of the stratum isomorphism is the identity on points, for the underlying map
Hom.toFun.
The manifold-source case: two K-morphisms from the space Sp(M) of an analytic manifold into
a non-singular analytic K-space with the same underlying map are equal — locality on the source
over the preimages of the dimension strata of the target, Hom.restrictTo into a stratum, the
isomorphisms Sp(M) | P ≅ Sp(P) and Sp(Y_{d'}) ≅ Y | Y_{d'}, and hom_ext_baseFun between
manifold spaces.
Two morphisms of non-singular analytic K-spaces with the same underlying map are equal
(compare the local Kⁿ-coordinations of [Hir64, Ch. 0, §1, p. 120]): locality on the source
(hom_ext_of_cover) over the dimension strata of X, the comparison isomorphism
stratumKIso : Sp(X_d) ≅ X | X_d to a manifold space, and the manifold-source case.