K-morphisms into (Kⁿ, 𝒜_{Kⁿ}) from n global sections: compatibility

A K-morphism from an analytic K-space X into (Kⁿ, 𝒜_{Kⁿ}) is the same as n global sections of 𝒪_X (a local Kⁿ-coordination is such a morphism, [Hir64, Ch. 0, §1, p. 120]). The uniqueness is hom_ext_of_coord (Hironaka/AnalyticSpace/HomExt.lean: the pullbacks of the coordinate functions determine the morphism); the existence, AnalyticSpace.homOfSections, is assembled in Hironaka/AnalyticSpace/HomOfSections.lean from this file (compatibility), Hironaka/AnalyticSpace/HomOfSectionsAffine.lean (the affine case), Hironaka/AnalyticSpace/HomOfSectionsModel.lean (local models) and Hironaka/AnalyticSpace/GlueHomAffine.lean (gluing).

Compatibility from coordinates. For a K-morphism φ : X|W ⟶ Kⁿ and z ∈ W, the stalk map of φ at z followed by the isomorphism of the stalk of X|W with that of X is a local homomorphism σ_φ : 𝒜_{Kⁿ, φ(z)} → 𝒪_{X,z} sending constants to constants and the coordinate germs to the germs of the pullbacks φ^*(z_i). Two morphisms φ : X|W ⟶ Kⁿ, φ' : X|W' ⟶ Kⁿ whose coordinate pullbacks have the same germs at z ∈ W ∩ W' therefore have the same base point at z (the coordinates of φ(z) are the residues of φ^*(z_i) at z) and, when the stalk 𝒪_{X,z} is Noetherian (hypothesis hN; ringHom_ext_of_coord, Krull's intersection theorem), the same σ, hence the same germs of the pullbacks of every function of 𝒜_{Kⁿ}.

The stalk of an open subspace as the stalk of the space

@[reducible, inline]

noncomputable abbrev AnalyticSpace.resIso {K : Type} [RCLike K] (Z : KLocallyRingedSpace K) (W : TopologicalSpace.Opens ↑↑Z.toPresheafedSpace) {z : ↑↑Z.toPresheafedSpace} (hz : z ∈ W) : (Z.restrictOpen W).presheaf.stalk ⟨z, hz⟩ ≅ Z.presheaf.stalk z

The stalk of Z|W at z ∈ W, identified with the stalk of Z at z (Mathlib's restrictStalkIso).

Equations

• AnalyticSpace.resIso Z W hz = Z.restrictStalkIso ⋯ ⟨z, hz⟩

theorem AnalyticSpace.resIso_hom_germ {K : Type} [RCLike K] (Z : KLocallyRingedSpace K) (W : TopologicalSpace.Opens ↑↑Z.toPresheafedSpace) {z : ↑↑Z.toPresheafedSpace} (hz : z ∈ W) (T : TopologicalSpace.Opens ↑↑(Z.restrictOpen W).toPresheafedSpace) (hT : ⟨z, hz⟩ ∈ T) (s : ↑(Z.presheaf.obj (Opposite.op (Z.imgOpens W T)))) : (CategoryTheory.ConcreteCategory.hom (resIso Z W hz).hom) ((CategoryTheory.ConcreteCategory.hom ((Z.restrictOpen W).presheaf.germ T ⟨z, hz⟩ hT)) s) = (CategoryTheory.ConcreteCategory.hom (Z.presheaf.germ (Z.imgOpens W T) z ⋯)) s

The identification on germs: a section of 𝒪_{Z|W} over T is a section of 𝒪_Z over the image of T.

theorem AnalyticSpace.resIso_hom_constAt {K : Type} [RCLike K] (Z : KLocallyRingedSpace K) (W : TopologicalSpace.Opens ↑↑Z.toPresheafedSpace) {z : ↑↑Z.toPresheafedSpace} (hz : z ∈ W) (c : K) : (CategoryTheory.ConcreteCategory.hom (resIso Z W hz).hom) (((Z.restrictOpen W).constAt ⟨z, hz⟩) c) = (Z.constAt z) c

The identification sends the constant germs of Z|W to those of Z.

theorem AnalyticSpace.resIso_inv_eq_stalkMap_ofRestrict {K : Type} [RCLike K] (Z : KLocallyRingedSpace K) (W : TopologicalSpace.Opens ↑↑Z.toPresheafedSpace) (w : ↑↑(Z.restrictOpen W).toPresheafedSpace) : (resIso Z W ⋯).inv = AlgebraicGeometry.LocallyRingedSpace.Hom.stalkMap (↑(Z.ofRestrict W)) w

The inverse of the identification is the stalk map of the open immersion Z|W ⟶ Z (Mathlib's restrictStalkIso_inv_eq_ofRestrict).

theorem AnalyticSpace.map_mem_maximalIdeal_of_isLocalHom {R : Type u_1} {S : Type u_2} [CommRing R] [CommRing S] [IsLocalRing R] [IsLocalRing S] (φ : R →+* S) [IsLocalHom φ] {x : R} (hx : x ∈ IsLocalRing.maximalIdeal R) : φ x ∈ IsLocalRing.maximalIdeal S

A local homomorphism sends the maximal ideal into the maximal ideal.

The stalk map of a morphism into affine space, as a map into the stalk of X

noncomputable def AnalyticSpace.sigmaStalk {K : Type} [RCLike K] {n : ℕ} (Z : KLocallyRingedSpace K) {W : TopologicalSpace.Opens ↑↑Z.toPresheafedSpace} (φ : Z.restrictOpen W ⟶ affine K n) {z : ↑↑Z.toPresheafedSpace} (hz : z ∈ W) : ↑((affine K n).presheaf.stalk ((CategoryTheory.ConcreteCategory.hom (↑φ).base) ⟨z, hz⟩)) →+* ↑(Z.presheaf.stalk z)

The stalk map of φ : Z|W ⟶ Kⁿ at z, followed by the identification of the stalk of Z|W with that of Z: 𝒜_{Kⁿ, φ(z)} → 𝒪_{Z,z}.

Equations

• AnalyticSpace.sigmaStalk Z φ hz = (CommRingCat.Hom.hom (AnalyticSpace.resIso Z W hz).hom).comp (CommRingCat.Hom.hom (AlgebraicGeometry.LocallyRingedSpace.Hom.stalkMap ↑φ ⟨z, hz⟩))

theorem AnalyticSpace.sigmaStalk_apply {K : Type} [RCLike K] {n : ℕ} (Z : KLocallyRingedSpace K) {W : TopologicalSpace.Opens ↑↑Z.toPresheafedSpace} (φ : Z.restrictOpen W ⟶ affine K n) {z : ↑↑Z.toPresheafedSpace} (hz : z ∈ W) (a : ↑((affine K n).presheaf.stalk ((CategoryTheory.ConcreteCategory.hom (↑φ).base) ⟨z, hz⟩))) : (sigmaStalk Z φ hz) a = (CategoryTheory.ConcreteCategory.hom (resIso Z W hz).hom) ((CategoryTheory.ConcreteCategory.hom (AlgebraicGeometry.LocallyRingedSpace.Hom.stalkMap ↑φ ⟨z, hz⟩)) a)

instance AnalyticSpace.isLocalHom_sigmaStalk {K : Type} [RCLike K] {n : ℕ} (Z : KLocallyRingedSpace K) {W : TopologicalSpace.Opens ↑↑Z.toPresheafedSpace} (φ : Z.restrictOpen W ⟶ affine K n) {z : ↑↑Z.toPresheafedSpace} (hz : z ∈ W) : IsLocalHom (sigmaStalk Z φ hz)

theorem AnalyticSpace.sigmaStalk_const {K : Type} [RCLike K] {n : ℕ} (Z : KLocallyRingedSpace K) {W : TopologicalSpace.Opens ↑↑Z.toPresheafedSpace} (φ : Z.restrictOpen W ⟶ affine K n) {z : ↑↑Z.toPresheafedSpace} (hz : z ∈ W) (c : K) : (sigmaStalk Z φ hz) ((Manifold.const K (Kn K n) (Kn K n) ((CategoryTheory.ConcreteCategory.hom (↑φ).base) ⟨z, hz⟩)) c) = (Z.constAt z) c

theorem AnalyticSpace.sigmaStalk_coordAt {K : Type} [RCLike K] {n : ℕ} (Z : KLocallyRingedSpace K) {W : TopologicalSpace.Opens ↑↑Z.toPresheafedSpace} (φ : Z.restrictOpen W ⟶ affine K n) {z : ↑↑Z.toPresheafedSpace} (hz : z ∈ W) (i : Fin n) : (sigmaStalk Z φ hz) (coordAt K n ((CategoryTheory.ConcreteCategory.hom (↑φ).base) ⟨z, hz⟩) i) = (CategoryTheory.ConcreteCategory.hom (Z.presheaf.germ (Z.imgOpens W ⊤) z ⋯)) ((KLocallyRingedSpace.Hom.pullbackΓ φ) (coordSection K n i))

theorem AnalyticSpace.sigmaStalk_germ {K : Type} [RCLike K] {n : ℕ} (Z : KLocallyRingedSpace K) {W : TopologicalSpace.Opens ↑↑Z.toPresheafedSpace} (φ : Z.restrictOpen W ⟶ affine K n) {z : ↑↑Z.toPresheafedSpace} (hz : z ∈ W) (V : TopologicalSpace.Opens (Kn K n)) (hV : (CategoryTheory.ConcreteCategory.hom (↑φ).base) ⟨z, hz⟩ ∈ V) (F : ↑((affine K n).presheaf.obj (Opposite.op V))) : (sigmaStalk Z φ hz) ((CategoryTheory.ConcreteCategory.hom ((affine K n).presheaf.germ V ((CategoryTheory.ConcreteCategory.hom (↑φ).base) ⟨z, hz⟩) hV)) F) = (CategoryTheory.ConcreteCategory.hom (Z.presheaf.germ (Z.imgOpens W ((TopologicalSpace.Opens.map (↑φ).base).obj V)) z ⋯)) ((CategoryTheory.ConcreteCategory.hom ((↑φ).c.app (Opposite.op V))) F)

The stalk map on a germ of F ∈ 𝒜(V): the germ at z of the pullback φ^*F.

theorem AnalyticSpace.germ_pullbackΓ_coord_sub_constAt_mem {K : Type} [RCLike K] {n : ℕ} (Z : KLocallyRingedSpace K) {W : TopologicalSpace.Opens ↑↑Z.toPresheafedSpace} (φ : Z.restrictOpen W ⟶ affine K n) {z : ↑↑Z.toPresheafedSpace} (hz : z ∈ W) (i : Fin n) : (CategoryTheory.ConcreteCategory.hom (Z.presheaf.germ (Z.imgOpens W ⊤) z ⋯)) ((KLocallyRingedSpace.Hom.pullbackΓ φ) (coordSection K n i)) - (Z.constAt z) (((CategoryTheory.ConcreteCategory.hom (↑φ).base) ⟨z, hz⟩).down i) ∈ IsLocalRing.maximalIdeal ↑(Z.presheaf.stalk z)

The coordinates of φ(z) are the residues of the pullbacks of the coordinates at z.

Transport of germs along an equality of points

theorem AnalyticSpace.germ_eqToHom {K : Type} [RCLike K] (n : ℕ) {p q : Kn K n} (hpq : p = q) (V : TopologicalSpace.Opens (Kn K n)) (hp : p ∈ V) (F : ↑((affine K n).presheaf.obj (Opposite.op V))) : (CommRingCat.Hom.hom (CategoryTheory.eqToHom ⋯)) ((CategoryTheory.ConcreteCategory.hom ((affine K n).presheaf.germ V p hp)) F) = (CategoryTheory.ConcreteCategory.hom ((affine K n).presheaf.germ V q ⋯)) F

theorem AnalyticSpace.const_eqToHom {K : Type} [RCLike K] (n : ℕ) {p q : Kn K n} (hpq : p = q) (c : K) : (CommRingCat.Hom.hom (CategoryTheory.eqToHom ⋯)) ((Manifold.const K (Kn K n) (Kn K n) p) c) = (Manifold.const K (Kn K n) (Kn K n) q) c

theorem AnalyticSpace.coordAt_eqToHom {K : Type} [RCLike K] (n : ℕ) {p q : Kn K n} (hpq : p = q) (i : Fin n) : (CommRingCat.Hom.hom (CategoryTheory.eqToHom ⋯)) (coordAt K n p i) = coordAt K n q i

Two morphisms with the same coordinate pullbacks agree on base points and germs

theorem AnalyticSpace.base_eq_of_germ_pullbackΓ_coord {K : Type} [RCLike K] {n : ℕ} (Z : KLocallyRingedSpace K) {W W' : TopologicalSpace.Opens ↑↑Z.toPresheafedSpace} (φ : Z.restrictOpen W ⟶ affine K n) (φ' : Z.restrictOpen W' ⟶ affine K n) {z : ↑↑Z.toPresheafedSpace} (hz : z ∈ W) (hz' : z ∈ W') (hcoord : ∀ (i : Fin n), (CategoryTheory.ConcreteCategory.hom (Z.presheaf.germ (Z.imgOpens W ⊤) z ⋯)) ((KLocallyRingedSpace.Hom.pullbackΓ φ) (coordSection K n i)) = (CategoryTheory.ConcreteCategory.hom (Z.presheaf.germ (Z.imgOpens W' ⊤) z ⋯)) ((KLocallyRingedSpace.Hom.pullbackΓ φ') (coordSection K n i))) : (CategoryTheory.ConcreteCategory.hom (↑φ).base) ⟨z, hz⟩ = (CategoryTheory.ConcreteCategory.hom (↑φ').base) ⟨z, hz'⟩

Same coordinate pullbacks at z ⇒ same base point at z.

theorem AnalyticSpace.germ_c_app_eq_of_germ_pullbackΓ_coord {K : Type} [RCLike K] {n : ℕ} (Z : KLocallyRingedSpace K) {W W' : TopologicalSpace.Opens ↑↑Z.toPresheafedSpace} (φ : Z.restrictOpen W ⟶ affine K n) (φ' : Z.restrictOpen W' ⟶ affine K n) {z : ↑↑Z.toPresheafedSpace} (hz : z ∈ W) (hz' : z ∈ W') (hcoord : ∀ (i : Fin n), (CategoryTheory.ConcreteCategory.hom (Z.presheaf.germ (Z.imgOpens W ⊤) z ⋯)) ((KLocallyRingedSpace.Hom.pullbackΓ φ) (coordSection K n i)) = (CategoryTheory.ConcreteCategory.hom (Z.presheaf.germ (Z.imgOpens W' ⊤) z ⋯)) ((KLocallyRingedSpace.Hom.pullbackΓ φ') (coordSection K n i))) (hN : IsNoetherianRing ↑(Z.presheaf.stalk z)) (V : TopologicalSpace.Opens (Kn K n)) (hV : (CategoryTheory.ConcreteCategory.hom (↑φ).base) ⟨z, hz⟩ ∈ V) (hV' : (CategoryTheory.ConcreteCategory.hom (↑φ').base) ⟨z, hz'⟩ ∈ V) (F : ↑((affine K n).presheaf.obj (Opposite.op V))) : (CategoryTheory.ConcreteCategory.hom (Z.presheaf.germ (Z.imgOpens W ((TopologicalSpace.Opens.map (↑φ).base).obj V)) z ⋯)) ((CategoryTheory.ConcreteCategory.hom ((↑φ).c.app (Opposite.op V))) F) = (CategoryTheory.ConcreteCategory.hom (Z.presheaf.germ (Z.imgOpens W' ((TopologicalSpace.Opens.map (↑φ').base).obj V)) z ⋯)) ((CategoryTheory.ConcreteCategory.hom ((↑φ').c.app (Opposite.op V))) F)

Same coordinate pullbacks at z ⇒ same germs at z of the pullbacks of every F ∈ 𝒜(V) (ringHom_ext_of_coord on the stalk maps).