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

A K-morphism from an analytic K-space X into (Kⁿ, 𝒜_{Kⁿ}) is the same as n global sections of 𝒪_X: AnalyticSpace.homOfSections X t : X ⟶ (Kⁿ, 𝒜_{Kⁿ}) with (homOfSections X t).pullbackΓ (coordSection K n i) = t i, unique by hom_ext_of_coord (Hironaka/AnalyticSpace/HomExt.lean); the two together are AnalyticSpace.existsUnique_hom_pullbackΓ_coord, Hom(X, Kⁿ) ≃ Γ(X, 𝒪_X)ⁿ. This is the form in which local coordinations [Hir64, Ch. 0, §1, p. 120] and the extended coordinations of a complexification are produced. Also the chart form: a K-morphism into (Kⁿ, 𝒜_{Kⁿ}) with image in an open V factors uniquely through (Kⁿ, 𝒜_{Kⁿ})|V (Hom.liftRestrict, existsUnique_hom_restrictOpen_of_range).

Assembly. Around every point x a chart e : X|U ≅ L onto a local model; the sections σ_i := e.inv^*(t_i|U) of L define localModel.homOfSections σ : L ⟶ Kⁿ (Hironaka/AnalyticSpace/HomOfSectionsModel.lean), and e.hom ≫ localModel.homOfSections σ : X|U ⟶ Kⁿ has coordinate pullbacks t_i|U (functoriality of the pullback, e.hom ≫ e.inv = 𝟙). These pieces have the same germs of coordinate pullbacks at every point (the germ of t_i), hence agree on base points and on germs of all pullbacks (Hironaka/AnalyticSpace/HomOfSectionsCompat.lean), and glue by glueHomAffine (Hironaka/AnalyticSpace/GlueHomAffine.lean). Not in the sources as a stated result.

structure AnalyticSpace.ChartPiece {K : Type} [RCLike K] {n : ℕ} (X : AnalyticSpace K) (t : Fin n → ↑(X.presheaf.obj (Opposite.op ⊤))) (x : ↑↑X.toPresheafedSpace) : Type u

Chart data at a point: an open neighbourhood and a K-isomorphism onto a local model, with a K-morphism of the chart into (Kⁿ, 𝒜_{Kⁿ}) whose coordinate pullbacks are the restrictions of the t i.

• U : TopologicalSpace.Opens ↑↑X.toPresheafedSpace

  The chart's open neighbourhood.

• mem : x ∈ self.U
• φ : X.restrictOpen self.U ⟶ affine K n

  The morphism of the chart into Kⁿ.

• coord (i : Fin n) : (KLocallyRingedSpace.Hom.pullbackΓ self.φ) (coordSection K n i) = (KLocallyRingedSpace.Hom.pullbackΓ (X.ofRestrict self.U)) (t i)

theorem AnalyticSpace.nonempty_chartPiece {K : Type} [RCLike K] {n : ℕ} (X : AnalyticSpace K) (t : Fin n → ↑(X.presheaf.obj (Opposite.op ⊤))) (x : ↑↑X.toPresheafedSpace) : Nonempty (X.ChartPiece t x)

noncomputable def AnalyticSpace.chartPiece {K : Type} [RCLike K] {n : ℕ} (X : AnalyticSpace K) (t : Fin n → ↑(X.presheaf.obj (Opposite.op ⊤))) (x : ↑↑X.toPresheafedSpace) : X.ChartPiece t x

A choice of chart piece at every point.

Equations

• X.chartPiece t x = Classical.choice ⋯

theorem AnalyticSpace.germ_pullbackΓ_chartPiece_coord {K : Type} [RCLike K] {n : ℕ} (X : AnalyticSpace K) (t : Fin n → ↑(X.presheaf.obj (Opposite.op ⊤))) (x : ↑↑X.toPresheafedSpace) {z : ↑↑X.toPresheafedSpace} (hz : z ∈ (X.chartPiece t x).U) (i : Fin n) : (CategoryTheory.ConcreteCategory.hom (X.presheaf.germ (X.imgOpens (X.chartPiece t x).U ⊤) z ⋯)) ((KLocallyRingedSpace.Hom.pullbackΓ (X.chartPiece t x).φ) (coordSection K n i)) = (CategoryTheory.ConcreteCategory.hom (X.presheaf.germ ⊤ z trivial)) (t i)

The germ at z ∈ U x of the coordinate pullback of the piece at x is the germ of t i.

theorem AnalyticSpace.hcoord_chartPiece {K : Type} [RCLike K] {n : ℕ} (X : AnalyticSpace K) (t : Fin n → ↑(X.presheaf.obj (Opposite.op ⊤))) (x x' : ↑↑X.toPresheafedSpace) {z : ↑↑X.toPresheafedSpace} (hz : z ∈ (X.chartPiece t x).U) (hz' : z ∈ (X.chartPiece t x').U) (i : Fin n) : (CategoryTheory.ConcreteCategory.hom (X.presheaf.germ (X.imgOpens (X.chartPiece t x).U ⊤) z ⋯)) ((KLocallyRingedSpace.Hom.pullbackΓ (X.chartPiece t x).φ) (coordSection K n i)) = (CategoryTheory.ConcreteCategory.hom (X.presheaf.germ (X.imgOpens (X.chartPiece t x').U ⊤) z ⋯)) ((KLocallyRingedSpace.Hom.pullbackΓ (X.chartPiece t x').φ) (coordSection K n i))

theorem AnalyticSpace.chartPiece_hbase {K : Type} [RCLike K] {n : ℕ} (X : AnalyticSpace K) (t : Fin n → ↑(X.presheaf.obj (Opposite.op ⊤))) (x x' z : ↑↑X.toPresheafedSpace) (hz : z ∈ (fun (x : ↑↑X.toPresheafedSpace) => (X.chartPiece t x).U) x) (hz' : z ∈ (fun (x : ↑↑X.toPresheafedSpace) => (X.chartPiece t x).U) x') : (CategoryTheory.ConcreteCategory.hom (↑(X.chartPiece t x).φ).base) ⟨z, hz⟩ = (CategoryTheory.ConcreteCategory.hom (↑(X.chartPiece t x').φ).base) ⟨z, hz'⟩

theorem AnalyticSpace.chartPiece_hgerm {K : Type} [RCLike K] {n : ℕ} (X : AnalyticSpace K) (t : Fin n → ↑(X.presheaf.obj (Opposite.op ⊤))) (x x' : ↑↑X.toPresheafedSpace) (V : TopologicalSpace.Opens (Kn K n)) (F : ↑((affine K n).presheaf.obj (Opposite.op V))) (z : ↑↑X.toPresheafedSpace) (hzi : z ∈ X.locV (fun (x : ↑↑X.toPresheafedSpace) => (X.chartPiece t x).U) (fun (x : ↑↑X.toPresheafedSpace) => (X.chartPiece t x).φ) x V) (hzj : z ∈ X.locV (fun (x : ↑↑X.toPresheafedSpace) => (X.chartPiece t x).U) (fun (x : ↑↑X.toPresheafedSpace) => (X.chartPiece t x).φ) x' V) : (CategoryTheory.ConcreteCategory.hom (X.presheaf.germ (X.locV (fun (x : ↑↑X.toPresheafedSpace) => (X.chartPiece t x).U) (fun (x : ↑↑X.toPresheafedSpace) => (X.chartPiece t x).φ) x V) z hzi)) (X.locSec (fun (x : ↑↑X.toPresheafedSpace) => (X.chartPiece t x).U) (fun (x : ↑↑X.toPresheafedSpace) => (X.chartPiece t x).φ) x V F) = (CategoryTheory.ConcreteCategory.hom (X.presheaf.germ (X.locV (fun (x : ↑↑X.toPresheafedSpace) => (X.chartPiece t x).U) (fun (x : ↑↑X.toPresheafedSpace) => (X.chartPiece t x).φ) x' V) z hzj)) (X.locSec (fun (x : ↑↑X.toPresheafedSpace) => (X.chartPiece t x).U) (fun (x : ↑↑X.toPresheafedSpace) => (X.chartPiece t x).φ) x' V F)

noncomputable def AnalyticSpace.homOfSections {K : Type} [RCLike K] {n : ℕ} (X : AnalyticSpace K) (t : Fin n → ↑(X.presheaf.obj (Opposite.op ⊤))) : X.toKLocallyRingedSpace ⟶ affine K n

The K-morphism X ⟶ (Kⁿ, 𝒜_{Kⁿ}) with coordinate functions t₁, …, tₙ, for an analytic K-space X.

Equations

• X.homOfSections t = X.glueHomAffine (fun (x : ↑↑X.toPresheafedSpace) => (X.chartPiece t x).U) ⋯ (fun (x : ↑↑X.toPresheafedSpace) => (X.chartPiece t x).φ) ⋯ ⋯

theorem AnalyticSpace.pullbackΓ_homOfSections_coordSection {K : Type} [RCLike K] {n : ℕ} (X : AnalyticSpace K) (t : Fin n → ↑(X.presheaf.obj (Opposite.op ⊤))) (i : Fin n) : (KLocallyRingedSpace.Hom.pullbackΓ (X.homOfSections t)) (coordSection K n i) = t i

The coordinate pullbacks of homOfSections X t are the t i.

theorem AnalyticSpace.existsUnique_hom_pullbackΓ_coord {K : Type} [RCLike K] {n : ℕ} (X : AnalyticSpace K) (t : Fin n → ↑(X.presheaf.obj (Opposite.op ⊤))) : ∃! φ : X.toKLocallyRingedSpace ⟶ affine K n, ∀ (i : Fin n), (KLocallyRingedSpace.Hom.pullbackΓ φ) (coordSection K n i) = t i

Hom(X, Kⁿ) ≃ Γ(X, 𝒪_X)ⁿ: there is exactly one K-morphism X ⟶ (Kⁿ, 𝒜_{Kⁿ}) with prescribed coordinate pullbacks.

theorem AnalyticSpace.homOfSections_pullbackΓ_coord {K : Type} [RCLike K] {n : ℕ} (X : AnalyticSpace K) (φ : X.toKLocallyRingedSpace ⟶ affine K n) : (X.homOfSections fun (i : Fin n) => (KLocallyRingedSpace.Hom.pullbackΓ φ) (coordSection K n i)) = φ

The morphism with the coordinate pullbacks of φ is φ (uniqueness).

noncomputable def AnalyticSpace.KLocallyRingedSpace.Hom.liftRestrict {K : Type} [RCLike K] {X Y : KLocallyRingedSpace K} (g : X ⟶ Y) (U : TopologicalSpace.Opens ↑↑Y.toPresheafedSpace) (h : ∀ (x : ↑↑X.toPresheafedSpace), toFun g x ∈ U) : X ⟶ Y.restrictOpen U

The lift of a K-morphism g : X ⟶ Y with g(X) ⊆ U through the open immersion Y|U ⟶ Y (Mathlib's universal property of open immersions of locally ringed spaces; the K-condition is inherited from g). Hironaka's (G, 𝒜_G) is (Kⁿ, 𝒜_{Kⁿ})|G [Hir64, Ch. 0, §1], so a morphism into Kⁿ landing in G is a morphism into (G, 𝒜_G).

Equations

• One or more equations did not get rendered due to their size.

theorem AnalyticSpace.KLocallyRingedSpace.Hom.liftRestrict_comp_ofRestrict {K : Type} [RCLike K] {X Y : KLocallyRingedSpace K} (g : X ⟶ Y) (U : TopologicalSpace.Opens ↑↑Y.toPresheafedSpace) (h : ∀ (x : ↑↑X.toPresheafedSpace), toFun g x ∈ U) : CategoryTheory.CategoryStruct.comp (liftRestrict g U h) (Y.ofRestrict U) = g

theorem AnalyticSpace.KLocallyRingedSpace.Hom.ext_of_comp_ofRestrict {K : Type} [RCLike K] {X Y : KLocallyRingedSpace K} {U : TopologicalSpace.Opens ↑↑Y.toPresheafedSpace} {φ ψ : X ⟶ Y.restrictOpen U} (h : CategoryTheory.CategoryStruct.comp φ (Y.ofRestrict U) = CategoryTheory.CategoryStruct.comp ψ (Y.ofRestrict U)) : φ = ψ

Open immersions are monomorphisms: two K-morphisms into Y|U with the same composite into Y are equal.

theorem AnalyticSpace.KLocallyRingedSpace.existsUnique_hom_restrictOpen_of_range {K : Type} [RCLike K] {n : ℕ} (X : KLocallyRingedSpace K) (V : TopologicalSpace.Opens (Kn K n)) (φ₀ : X ⟶ affine K n) (h : ∀ (x : ↑↑X.toPresheafedSpace), Hom.toFun φ₀ x ∈ V) : ∃! φ : X ⟶ (affine K n).restrictOpen V, CategoryTheory.CategoryStruct.comp φ ((affine K n).ofRestrict V) = φ₀

A K-morphism X ⟶ (Kⁿ, 𝒜_{Kⁿ}) whose image lies in the open V factors uniquely through (Kⁿ, 𝒜_{Kⁿ})|V.