The local isomorphism criterion for analytic K-spaces #
A K-morphism φ : X ⟶ Y of analytic K-spaces whose stalk map φ^*_x : 𝒪_{Y,φ x} → 𝒪_{X,x} is
bijective restricts to a K-isomorphism X|U ≅ Y|V of open neighbourhoods of x and φ x
(AnalyticSpace.exists_isIso_restrictTo_of_bijective_stalkMap). Hironaka's analytic K-spaces are
locally the closed subspaces V(f) ⊆ G ⊆ Kⁿ of opens of Kⁿ cut out by finitely many analytic
functions, with the structure sheaf 𝒜_G/(f) [Hir64, Ch. 0, §1, pp. 119–120]; the local rings
determine the spaces near a point — the content of the equivalence between germs of analytic
spaces and analytic algebras [GR84, Ch. 1], of which this is the weakest form, the one Hironaka
uses tacitly when a local Kⁿ-coordination is recognised on the local rings
[Hir64, Ch. 0, §1, p. 120]. Not proved in the sources; the argument:
Construction of the local inverse. Take a chart eX : X|U₁ ≅ V(f') ⊆ G' ⊆ Kⁿ at x, with chart
map κ = eX.hom ≫ ι : X|U₁ ⟶ (Kⁿ, 𝒜). The n coordinate germs of κ at x have preimages under
the bijection φ^*_x, realised as sections t_j of Y near φ x; the t_j are the
coordinates of a unique K-morphism χ₀ : Y|W → (Kⁿ, 𝒜) (AnalyticSpace.homOfSections,
Hironaka/AnalyticSpace/HomOfSections.lean). Its base point at φ x is κ(x) ∈ G' (the coordinate
germs of κ at x and of χ₀ at φ x correspond under the local homomorphism φ^*_x, so the
values agree, stalkMap_sigmaStalk_eq_of_coord), and the pullbacks of the equations f'_i along
χ₀ have zero germs at φ x (they are the (φ^*_x)⁻¹-images of the pullbacks along κ, which
vanish on the model, stalkMap_localModel_ι_germ_eq_zero); shrinking W to W₂, χ₀ lands in
G' and kills the f'_i, so it factors through the model by the functoriality of quotients along
the zero ideal sheaf (quotientMap, quotientBotIso), and χ = (…) ≫ eX.inv : Y|W₂ ⟶ X|U₁ has
the coordinate identity φ^*_x(germ (χ ≫ κ)^* z_j) = germ κ^* z_j
(exists_hom_coord_of_bijective_stalkMap).
The two inverse identities. Germ identities between finitely many sections spread to a
neighbourhood (exists_opens_forall_germ_eq, exists_opens_forall_stalkMap_germ_eq). A
K-morphism into (Kⁿ, 𝒜) is determined by its coordinate pullbacks (hom_ext_of_coord) and the
chart map is a monomorphism (Hom.ext_of_comp_localModel_ι), so equality of morphisms into a
chart of A reduces to germ identities of coordinates
(restrictTo_comp_eq_of_stalkMap_germ_pullbackΓ_coord, with the bookkeeping lemma
germ_pullbackΓ_restrictTo: the germ of a pullback along a restriction g|U is the stalk map of
g on the germ). This gives φ|S ≫ χ = incl on an open S ∋ x; then the coordinates of
χ ≫ φ|U₁ ≫ κY and of κY (κY the chart map of Y at φ x) have the same germs at φ x
(apply the injective φ^*_x and use the first identity), spread to an open T ∋ φ x, and give
incl ≫ χ ≫ φ|U₁ = incl on Y|T.
Assembly (exists_isIso_restrictTo_of_inverse). With U = S ∩ φ⁻¹T and
V = {b ∈ T | χ b ∈ U}, the base map of φ|U : X|U ⟶ Y|V is a homeomorphism with inverse χ,
and the stalk maps are bijective: surjective by the first identity (φ|S^* ∘ χ^* = id), injective
by the second (χ^* ∘ φ|U₁^* = id); the criterion isIso_of_isIso_base_of_stalkMap_bijective
(Hironaka/AnalyticSpace/IsoCriterion.lean) concludes. Mathlib's stalkMap_comp,
stalkMap_germ_apply, germ_eq and section_ext carry the stalk computations. Used by
Hironaka/AnalyticSpace/IsoOverOpen.lean and Hironaka/Manifold/Sequence/Restrict/.
The closed immersion (S(𝒥), 𝒪_X/𝒥) ⟶ X of a quotient is a monomorphism of K-spaces: two
K-morphisms into the quotient with the same composite into X are equal (the base map of the
immersion is injective, its stalk maps are surjective, and a morphism of locally ringed spaces
into a sheaf-valued target is determined by its base map and its stalk maps).
Two K-morphisms into Y|U with the same composite into Y are equal; the composite of two
open immersions with a closed immersion of a quotient is a monomorphism: the chart map
X|U ≅ V(f) ⟶ (G, 𝒜_G) ⟶ (Kⁿ, 𝒜) of a local coordination is a monomorphism of K-spaces.
The functoriality of quotients commutes with the canonical morphisms.
The equations of a local model pull back to zero along its closed embedding into (Kⁿ, 𝒜): the
germ of f i at the image of a point of the model is killed by the stalk map.
The equations of a local model pull back to zero along e ≫ ι for a K-isomorphism e onto
the model.
Equal morphisms have equal stalk maps on germs (the point of the germ transported along the
equality; a Prop-level congruence avoiding the dependent rewrite).
The germ at a ∈ U of the pullback of a global section u of B|U' along the restriction
g|U : A|U ⟶ B|U' of g : A ⟶ B is the image under the stalk map g^*_a of the germ of u at
g a (both read in the stalks of A and B).
Two finite families of sections with the same germs at x have the same germs on a
neighbourhood of x.
A finite family of identities f^*_x (germ u_i) = germ v_i between germs at x holds at every
point of a neighbourhood of x.
A one-sided inverse identity from coordinates: if the stalk maps of g : Z ⟶ Z' carry the
coordinate germs of α ≫ κ (κ = e.hom ≫ ι the chart map of A) at g z to those of β ≫ κ at
z for every z ∈ S, then g|S ≫ α = (S ⊆ U') ≫ β as morphisms Z|S ⟶ A — the chart map is a
monomorphism (Hom.ext_of_comp_localModel_ι) and a morphism into Kⁿ is determined by its
coordinate pullbacks (hom_ext_of_coord), which are determined by their germs.
The germ of the pullback of a section of A|U' along the inclusion A|U ⟶ A|U', U ≤ U'.
Equal morphisms have stalk maps that are injective together.
Equal morphisms have stalk maps that are surjective together.
Injectivity of the stalk map of a composite passes to the second factor.
Surjectivity of the stalk map of a composite passes to the first factor.
The stalk maps of the inclusion A|U ⟶ A|U' of open subspaces are bijective.
Surjectivity of a stalk map of g|U : A|U ⟶ B|U' gives that of the stalk map of g.
Injectivity of a stalk map of g|U : A|U ⟶ B|U' gives that of the stalk map of g.
The assembly of the local isomorphism criterion: a K-morphism φ : X ⟶ Y with a two-sided
local inverse χ : Y|W₂ ⟶ X|U₁ — φ|S ≫ χ is the inclusion X|S ⟶ X|U₁ and χ ≫ φ|U₁
restricted to Y|T is the inclusion Y|T ⟶ Y|V₁ — restricts to a K-isomorphism X|U ≅ Y|V at
any x ∈ S with φ x ∈ T: U = S ∩ φ⁻¹T, V = {b ∈ T | χ b ∈ U}; the base map is a
homeomorphism with inverse χ, and the stalk maps are bijective (surjective from the first
identity, injective from the second), so isIso_of_isIso_base_of_stalkMap_bijective applies.
The chart at x may be taken inside any open neighbourhood O of x (a chart of the open
subspace X|O at x, carried back by restrictOpen_restrictOpen_iso; exists_kIso_localModel
refined).
The germ-level content of the local isomorphism criterion. For a K-morphism φ : X → Y, a
point x, a K-morphism κ : X|U₁ → Kⁿ and a K-morphism ψ : Y|W → Kⁿ whose coordinate
pullbacks at φ x are carried by the stalk map φ^*_x to the coordinate pullbacks of κ at x:
then ψ(φ x) = κ(x), and φ^*_x ∘ σ_ψ = σ_κ on the stalk 𝒜_{Kⁿ,ψ(φ x)} (sigmaStalk: the stalk
maps followed by the identification of the stalks of the open subspaces with those of the spaces)
— two local K-algebra maps out of 𝒜_{Kⁿ,q} agreeing on the constants and the coordinates agree
(ringHom_ext_of_coord).
The construction of the local inverse: for φ : X → Y with a bijective stalk map at x, a
chart e : X|U₁ ≅ V(f') ⊆ G' ⊆ Kⁿ of X at x and an open V₁ ∋ φ x, there is an open
W₂ ∋ φ x inside V₁ and a K-morphism χ : Y|W₂ ⟶ X|U₁ such that φ^*_x carries the
coordinate germs of χ ≫ κ (κ = e.hom ≫ ι the chart map) at φ x to those of κ at x. The
coordinates of χ ≫ κ are sections t j of Y near φ x whose germs are the preimages under
φ^*_x of the coordinate germs of κ; the morphism Y|W₂ → Kⁿ with those coordinates is
homOfSections; it lands in G' near φ x; its pullbacks of the equations f' of the model
vanish near φ x (their germs at φ x are (φ^*_x)⁻¹ of the germs of the pullbacks along κ,
which are zero, stalkMap_localModel_ι_germ_eq_zero), so it factors through the model by the
functoriality of quotients along the zero ideal sheaf (quotientMap, quotientBotIso), and χ
is the composite with e.inv.
The local isomorphism criterion ([Hir64, Ch. 0, §1, pp. 119–120], tacit; [GR84, Ch. 1]): a
K-morphism φ : X ⟶ Y of analytic K-spaces whose stalk map at x is bijective restricts to a
K-isomorphism of open neighbourhoods X|U ≅ Y|V. Charts eY of Y at φ x and eX of X at
x inside φ⁻¹V₁; the construction exists_hom_coord_of_bijective_stalkMap gives
χ : Y|W₂ ⟶ X|U₁ with the coordinate identity at φ x, which spreads to an open S ∋ x
(exists_opens_forall_stalkMap_germ_eq) and yields φ|S ≫ χ = incl by the uniqueness of
morphisms into Kⁿ with given coordinates (restrictTo_comp_eq_of_stalkMap_germ_pullbackΓ_coord);
the coordinates of χ ≫ φ|U₁ ≫ κY and of κY have the same germs at φ x (by the first identity
and injectivity of φ^*_x), spread to an open T ∋ φ x, and give incl ≫ χ ≫ φ|U₁ = incl on
Y|T; exists_isIso_restrictTo_of_inverse concludes through
isIso_of_isIso_base_of_stalkMap_bijective.