Morphisms into (Kⁿ, 𝒜_{Kⁿ}) are determined by their coordinate functions

A local Kⁿ-coordination is a K-morphism h : X|U → (Kⁿ, 𝒜_{Kⁿ}) [Hir64, Ch. 0, §1, p. 120], and such a morphism is determined by the n coordinate functions h^*z_i. This file proves that (hom_ext_of_coord) for any K-local-ringed space with Noetherian stalks, and establishes the Noetherianity of the stalks of analytic K-spaces on the way. Not stated in the sources; the argument:

1. Noetherian stalks. The stalk 𝒪_{X,x} of an analytic K-space is a Noetherian local ring: through the local-model isomorphism it is 𝒜_{G,z}/𝓘_z, a quotient of a stalk of 𝒜_{Kⁿ}, which is Noetherian by Rückert's basis theorem (isNoetherianRing_stalk of Hironaka/Manifold/Germ/StalkNoetherian.lean).
2. Base maps. For a K-morphism χ : X → (Kⁿ, 𝒜) the stalk map χ_x : 𝒜_{Kⁿ,χ(x)} → 𝒪_{X,x} is local and carries constants to constants, so χ_x(z_i - χ(x)_i) ∈ 𝔪_x, i.e. the germ of the pulled-back coordinate function χ^*z_i is congruent to the constant χ(x)_i modulo 𝔪_x. Two morphisms with the same χ^*z_i therefore have φ(x)_i - ψ(x)_i ∈ 𝔪_x as a constant; a nonzero constant is a unit, so φ(x) = ψ(x).
3. Stalk maps. Two local ring homomorphisms α, β : 𝒜_{Kⁿ,q} → R into a Noetherian local ring that agree on the constants and on the coordinate germs agree: by Hadamard's lemma (exists_eq_sum_coord_mul') every germ is, modulo 𝔪_q^N, a polynomial in the coordinate germs with constant coefficients, on which α and β agree; local homomorphisms map 𝔪_q^N into 𝔪_R^N; so α s - β s ∈ ⋂_N 𝔪_R^N = 0 by Krull's intersection theorem (Ideal.iInf_pow_eq_bot_of_isLocalRing) — ringHom_ext_of_coord.
4. Sheaf maps. With equal base maps, the components of the sheaf maps agree because a section of a sheaf is determined by its germs (TopCat.Presheaf.section_ext) and the germ of χ.c.app U s at x is χ_x of the germ of s (stalkMap_germ_apply) — hom_ext_of_coord.

This is the uniqueness half of the description of morphisms into Kⁿ by coordinate functions; it is used wherever such a morphism is specified by its coordinates, for instance for morphisms built from sections of the structure sheaf (Hironaka/AnalyticSpace/HomOfSectionsCompat.lean) and for the uniqueness of monoidal transformations (Hironaka/AnalyticSpace/MonoidalUnique.lean).

@[reducible, inline]

noncomputable abbrev AnalyticSpace.coordAt (K : Type) [RCLike K] (n : ℕ) (q : Kn K n) (i : Fin n) : ↑((Manifold.structureSheaf K (Kn K n) (Kn K n)).presheaf.stalk q)

The coordinate germs z_i of Kⁿ at q (in the identity chart).

Equations

• AnalyticSpace.coordAt K n q i = Manifold.coord (AnalyticSpace.Kn K n) ContinuousLinearEquiv.ulift (chartAt (AnalyticSpace.Kn K n) q) ⋯ ⋯ i

theorem AnalyticSpace.coordAt_eq_germ (K : Type) [RCLike K] (n : ℕ) (q : Kn K n) (i : Fin n) : coordAt K n q i = (CategoryTheory.ConcreteCategory.hom ((affine K n).presheaf.germ ⊤ q ⋯)) (coordSection K n i)

The coordinate germ coordAt q i is the germ at q of the coordinate section z_i.

theorem AnalyticSpace.eval_coordAt (K : Type) [RCLike K] (n : ℕ) (q : Kn K n) (i : Fin n) : (Manifold.eval K (Kn K n) (Kn K n) q) (coordAt K n q i) = q.down i

The value at q of the coordinate germ z_i is q_i.

theorem AnalyticSpace.affine_germ_algebraMap (K : Type) [RCLike K] (n : ℕ) (q : Kn K n) (c : K) : (CategoryTheory.ConcreteCategory.hom ((affine K n).presheaf.germ ⊤ q ⋯)) ((affine K n).algebraMap c) = (Manifold.const K (Kn K n) (Kn K n) q) c

The constants of 𝒜_{Kⁿ,q} given by the K-structure of (Kⁿ, 𝒜_{Kⁿ}) are the constant germs const.

theorem AnalyticSpace.mem_maximalIdeal_coordAt_sub (K : Type) [RCLike K] (n : ℕ) (q : Kn K n) (i : Fin n) : coordAt K n q i - (Manifold.const K (Kn K n) (Kn K n) q) ((Manifold.eval K (Kn K n) (Kn K n) q) (coordAt K n q i)) ∈ IsLocalRing.maximalIdeal ↑((Manifold.structureSheaf K (Kn K n) (Kn K n)).presheaf.stalk q)

z_i − z_i(q) ∈ 𝔪_q.

theorem AnalyticSpace.ringHom_ext_of_coord {K : Type} [RCLike K] {n : ℕ} {R : Type u} [CommRing R] [IsLocalRing R] [IsNoetherianRing R] (q : Kn K n) (α β : ↑((Manifold.structureSheaf K (Kn K n) (Kn K n)).presheaf.stalk q) →+* R) [IsLocalHom α] [IsLocalHom β] (hc : ∀ (c : K), α ((Manifold.const K (Kn K n) (Kn K n) q) c) = β ((Manifold.const K (Kn K n) (Kn K n) q) c)) (hz : ∀ (i : Fin n), α (coordAt K n q i) = β (coordAt K n q i)) : α = β

Two local ring homomorphisms from 𝒜_{Kⁿ,q} into a Noetherian local ring that agree on the constants and on the coordinate germs agree: a convergent series is the 𝔪-adic limit of its truncations, and Krull's intersection theorem applies in the target.

Noetherian stalks

theorem AnalyticSpace.QuotientSpace.isNoetherianRing_stalk (X : AlgebraicGeometry.LocallyRingedSpace) (J : Manifold.IdealSheaf X.𝒪) [∀ (x : ↑X.toTopCat), IsNoetherianRing ↑(X.presheaf.stalk x)] (z : ↑(support X J)) : IsNoetherianRing ↑((quotientSpace X J).presheaf.stalk z)

The stalks of the quotient (S(𝒥), (𝒪_X/𝒥)|_{S(𝒥)}) are Noetherian when those of X are (through stalkEquiv).

theorem AnalyticSpace.isNoetherianRing_stalk_affine (K : Type) [RCLike K] (n : ℕ) (q : Kn K n) : IsNoetherianRing ↑((affine K n).presheaf.stalk q)

The stalks 𝒜_{Kⁿ,q} are Noetherian (Rückert's basis theorem).

theorem AnalyticSpace.isNoetherianRing_stalk_analyticSpaceOfOpen (K : Type) [RCLike K] (n : ℕ) (G : TopologicalSpace.Opens (Kn K n)) (x : ↑↑(analyticSpaceOfOpen K n G).toPresheafedSpace) : IsNoetherianRing ↑((analyticSpaceOfOpen K n G).presheaf.stalk x)

The stalks of (G, 𝒜_G) are Noetherian (restrictStalkIso).

theorem AnalyticSpace.isNoetherianRing_stalk_localModel (K : Type) [RCLike K] (n : ℕ) (G : TopologicalSpace.Opens (Kn K n)) {k : ℕ} (f : Fin k → AnalyticFun K n G) (z : ↑↑(localModel K n G f).toPresheafedSpace) : IsNoetherianRing ↑((localModel K n G f).presheaf.stalk z)

The stalks of a local model (S(𝓘), (𝒜_G/𝓘)|_{S(𝓘)}) are Noetherian.

theorem AnalyticSpace.KLocallyRingedSpace.isNoetherianRing_stalk_restrictOpen {K : Type} [RCLike K] (X : KLocallyRingedSpace K) (U : TopologicalSpace.Opens ↑↑X.toPresheafedSpace) (x : ↑↑(X.restrictOpen U).toPresheafedSpace) (h : IsNoetherianRing ↑(X.presheaf.stalk ↑x)) : IsNoetherianRing ↑((X.restrictOpen U).presheaf.stalk x)

Noetherianity of a stalk passes from X to the open subspace X|U.

theorem AnalyticSpace.KLocallyRingedSpace.isNoetherianRing_stalk_of_restrictOpen {K : Type} [RCLike K] (X : KLocallyRingedSpace K) (U : TopologicalSpace.Opens ↑↑X.toPresheafedSpace) (x : ↑↑(X.restrictOpen U).toPresheafedSpace) (h : IsNoetherianRing ↑((X.restrictOpen U).presheaf.stalk x)) : IsNoetherianRing ↑(X.presheaf.stalk ↑x)

Noetherianity of a stalk passes from the open subspace X|U to X.

theorem AnalyticSpace.KLocallyRingedSpace.isNoetherianRing_stalk_of_kIso {K : Type} [RCLike K] {A B : KLocallyRingedSpace K} (e : A.KIso B) (a : ↑↑A.toPresheafedSpace) (h : IsNoetherianRing ↑(B.presheaf.stalk ((CategoryTheory.ConcreteCategory.hom (↑e.hom).base) a))) : IsNoetherianRing ↑(A.presheaf.stalk a)

Noetherianity of stalks transports along a K-isomorphism (its stalk maps are isomorphisms).

theorem AnalyticSpace.isNoetherianRing_stalk {K : Type} [RCLike K] (X : AnalyticSpace K) (x : ↑↑X.toPresheafedSpace) : IsNoetherianRing ↑(X.presheaf.stalk x)

The stalks of an analytic K-space are Noetherian: every point has a neighbourhood isomorphic to an open of a local model, whose stalks are quotients of stalks of 𝒜_{Kⁿ}.

A K-morphism into (Kⁿ, 𝒜_{Kⁿ}) is determined by its coordinate functions

noncomputable def AnalyticSpace.KLocallyRingedSpace.constAt {K : Type} [RCLike K] (X : KLocallyRingedSpace K) (x : ↑↑X.toPresheafedSpace) : K →+* ↑(X.presheaf.stalk x)

The constants of the stalk 𝒪_{X,x}: the germs of the global constants, K →+* 𝒪_{X,x}.

Equations

• X.constAt x = (CommRingCat.Hom.hom (X.presheaf.germ ⊤ x ⋯)).comp X.algebraMap

theorem AnalyticSpace.KLocallyRingedSpace.isUnit_constAt {K : Type} [RCLike K] (X : KLocallyRingedSpace K) (x : ↑↑X.toPresheafedSpace) {c : K} (hc : c ≠ 0) : IsUnit ((X.constAt x) c)

A nonzero constant is a unit of every stalk.

theorem AnalyticSpace.stalkMap_coordAt {K : Type} [RCLike K] {n : ℕ} (X : KLocallyRingedSpace K) (χ : X ⟶ affine K n) (x : ↑↑X.toPresheafedSpace) (i : Fin n) : (CategoryTheory.ConcreteCategory.hom (AlgebraicGeometry.LocallyRingedSpace.Hom.stalkMap (↑χ) x)) (coordAt K n ((CategoryTheory.ConcreteCategory.hom (↑χ).base) x) i) = (CategoryTheory.ConcreteCategory.hom (X.presheaf.germ ⊤ x ⋯)) ((KLocallyRingedSpace.Hom.pullbackΓ χ) (coordSection K n i))

The stalk map at x of a K-morphism χ : X → Kⁿ carries the coordinate germ z_i at χ(x) to the germ at x of the pullback χ^*z_i.

theorem AnalyticSpace.stalkMap_const {K : Type} [RCLike K] {n : ℕ} (X : KLocallyRingedSpace K) (χ : X ⟶ affine K n) (x : ↑↑X.toPresheafedSpace) (c : K) : (CategoryTheory.ConcreteCategory.hom (AlgebraicGeometry.LocallyRingedSpace.Hom.stalkMap (↑χ) x)) ((Manifold.const K (Kn K n) (Kn K n) ((CategoryTheory.ConcreteCategory.hom (↑χ).base) x)) c) = (X.constAt x) c

The stalk map of a K-morphism χ : X → Kⁿ carries the constants to the constants.

theorem AnalyticSpace.KLocallyRingedSpace.base_apply_eq_of_pullbackΓ_coord {K : Type} [RCLike K] {n : ℕ} (X : KLocallyRingedSpace K) (φ ψ : X ⟶ affine K n) (h : ∀ (i : Fin n), (Hom.pullbackΓ φ) (coordSection K n i) = (Hom.pullbackΓ ψ) (coordSection K n i)) (x : ↑↑X.toPresheafedSpace) : (CategoryTheory.ConcreteCategory.hom (↑φ).base) x = (CategoryTheory.ConcreteCategory.hom (↑ψ).base) x

Two K-morphisms X → Kⁿ with the same pullbacks of the coordinate functions have the same underlying map: the constant φ(x)_i − ψ(x)_i lies in 𝔪_x, and a nonzero constant is a unit (isUnit_constAt).

theorem AnalyticSpace.base_apply_eq_of_pullbackΓ_coord {K : Type} [RCLike K] {n : ℕ} (X : AnalyticSpace K) (φ ψ : X.toKLocallyRingedSpace ⟶ affine K n) (h : ∀ (i : Fin n), (KLocallyRingedSpace.Hom.pullbackΓ φ) (coordSection K n i) = (KLocallyRingedSpace.Hom.pullbackΓ ψ) (coordSection K n i)) (x : ↑↑X.toPresheafedSpace) : (CategoryTheory.ConcreteCategory.hom (↑φ).base) x = (CategoryTheory.ConcreteCategory.hom (↑ψ).base) x

Two K-morphisms from an analytic K-space to Kⁿ with the same pullbacks of the coordinate functions have the same underlying map (the special case of KLocallyRingedSpace.base_apply_eq_of_pullbackΓ_coord).

theorem AnalyticSpace.KLocallyRingedSpace.hom_ext_of_coord {K : Type} [RCLike K] {n : ℕ} (X : KLocallyRingedSpace K) (hN : ∀ (x : ↑↑X.toPresheafedSpace), IsNoetherianRing ↑(X.presheaf.stalk x)) (φ ψ : X ⟶ affine K n) (h : ∀ (i : Fin n), (Hom.pullbackΓ φ) (coordSection K n i) = (Hom.pullbackΓ ψ) (coordSection K n i)) : φ = ψ

A K-morphism from a K-local-ringed space with Noetherian stalks into (Kⁿ, 𝒜_{Kⁿ}) is determined by the pullbacks of the coordinate functions (a local Kⁿ-coordination [Hir64, Ch. 0, §1, p. 120] is such a morphism; the uniqueness itself is not stated in the sources). The proof uses the analytic-space structure only through the Noetherianity of the stalks, hence the general form.

theorem AnalyticSpace.hom_ext_of_coord {K : Type} [RCLike K] {n : ℕ} (X : AnalyticSpace K) (φ ψ : X.toKLocallyRingedSpace ⟶ affine K n) (h : ∀ (i : Fin n), (KLocallyRingedSpace.Hom.pullbackΓ φ) (coordSection K n i) = (KLocallyRingedSpace.Hom.pullbackΓ ψ) (coordSection K n i)) : φ = ψ

A K-morphism from an analytic K-space into (Kⁿ, 𝒜_{Kⁿ}) is determined by the pullbacks of the coordinate functions: the special case of KLocallyRingedSpace.hom_ext_of_coord, the stalks of an analytic space being Noetherian.