K-morphisms from a local model into (Kⁿ, 𝒜) from n sections

The local-model case of the existence of a morphism into Kⁿ with prescribed coordinate functions: a local analytic K-space L = V(f₁, …, f_k) ⊆ G ⊆ Kᵐ and n global sections σ_i of 𝒪_L. Near a point of L the σ_i are the classes of ambient analytic functions a_i on an open W ⊆ Kᵐ (the sections of the quotient sheaf are locally the class families of ambient sections); on such an open V ⊆ L the morphism is the closed-immersion restriction L|V ⟶ (Kᵐ, 𝒜)|W followed by the affine morphism of the a_i (modelPiece), and its coordinate pullbacks are the classes of the a_i (germ_pullbackΓ_modelPiece_coord), hence the σ_i; the pieces glue by glueHomAffine (localModel.homOfSections). Routine.

Functoriality of the pullback of global sections

theorem AnalyticSpace.KLocallyRingedSpace.Hom.pullbackΓ_comp {K : Type} [RCLike K] {X Y Z : KLocallyRingedSpace K} (f : X ⟶ Y) (g : Y ⟶ Z) (s : ↑(AlgebraicGeometry.LocallyRingedSpace.Γ.obj (Opposite.op Z.toLocallyRingedSpace))) : (pullbackΓ (CategoryTheory.CategoryStruct.comp f g)) s = (pullbackΓ f) ((pullbackΓ g) s)

theorem AnalyticSpace.KLocallyRingedSpace.Hom.pullbackΓ_id {K : Type} [RCLike K] {X : KLocallyRingedSpace K} (s : ↑(AlgebraicGeometry.LocallyRingedSpace.Γ.obj (Opposite.op X.toLocallyRingedSpace))) : (pullbackΓ (CategoryTheory.CategoryStruct.id X)) s = s

theorem AnalyticSpace.KLocallyRingedSpace.Iso.hom_pullbackΓ_inv_pullbackΓ {K : Type} [RCLike K] {X Y : KLocallyRingedSpace K} (e : X ≅ Y) (s : ↑(AlgebraicGeometry.LocallyRingedSpace.Γ.obj (Opposite.op X.toLocallyRingedSpace))) : (Hom.pullbackΓ e.hom) ((Hom.pullbackΓ e.inv) s) = s

The pullback along e.hom inverts the pullback along e.inv.

theorem AnalyticSpace.KLocallyRingedSpace.germ_pullbackΓ_ofRestrict {K : Type} [RCLike K] {X : KLocallyRingedSpace K} (U : TopologicalSpace.Opens ↑↑X.toPresheafedSpace) {x : ↑↑X.toPresheafedSpace} (hx : x ∈ U) (s : ↑(AlgebraicGeometry.LocallyRingedSpace.Γ.obj (Opposite.op X.toLocallyRingedSpace))) : (CategoryTheory.ConcreteCategory.hom (X.presheaf.germ (X.imgOpens U ⊤) x ⋯)) ((Hom.pullbackΓ (X.ofRestrict U)) s) = (CategoryTheory.ConcreteCategory.hom (X.presheaf.germ ⊤ x trivial)) s

The germ of a global section pulled back along an open immersion X|U ⟶ X.

The piece of a local model

noncomputable def AnalyticSpace.KLocallyRingedSpace.modelPiece {K : Type} [RCLike K] {n : ℕ} (m : ℕ) (G : TopologicalSpace.Opens (Kn K m)) {k : ℕ} (f : Fin k → AnalyticFun K m G) (V : TopologicalSpace.Opens ↑↑(localModel K m G f).toPresheafedSpace) (W : TopologicalSpace.Opens (Kn K m)) (hVW : ∀ v ∈ V, Hom.toFun (localModel.ι K m G f) v ∈ W) (a : Fin n → ↑((affine K m).presheaf.obj (Opposite.op W))) : (localModel K m G f).restrictOpen V ⟶ affine K n

The morphism L|V ⟶ (Kⁿ, 𝒜) of a local model L ⊆ G ⊆ Kᵐ given by ambient analytic functions a_i on an open W ⊆ Kᵐ with V ⊆ W: the restriction of the closed immersion L ⟶ (Kᵐ, 𝒜) to L|V ⟶ (Kᵐ, 𝒜)|W, followed by the affine morphism of the a_i.

Equations

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

theorem AnalyticSpace.KLocallyRingedSpace.stalkMap_homOfSectionsAffine_coordAt {K : Type} [RCLike K] {n : ℕ} (m : ℕ) (W : TopologicalSpace.Opens (Kn K m)) (a : Fin n → ↑((affine K m).presheaf.obj (Opposite.op W))) (w : ↑↑((affine K m).restrictOpen W).toPresheafedSpace) (i : Fin n) : (CategoryTheory.ConcreteCategory.hom (AlgebraicGeometry.LocallyRingedSpace.Hom.stalkMap (↑(homOfSectionsAffine W a)) w)) (coordAt K n ((CategoryTheory.ConcreteCategory.hom (↑(homOfSectionsAffine W a)).base) w) i) = (CategoryTheory.ConcreteCategory.hom (AlgebraicGeometry.LocallyRingedSpace.Hom.stalkMap (↑((affine K m).ofRestrict W)) w)) ((CategoryTheory.ConcreteCategory.hom ((affine K m).presheaf.germ W ↑w ⋯)) (a i))

The affine morphism of the a_i on the coordinate germ: the stalk map of the open immersion (Kᵐ, 𝒜)|W ⟶ (Kᵐ, 𝒜) on the germ of a i.

theorem AnalyticSpace.KLocallyRingedSpace.germ_pullbackΓ_modelPiece_coord {K : Type} [RCLike K] {n : ℕ} (m : ℕ) (G : TopologicalSpace.Opens (Kn K m)) {k : ℕ} (f : Fin k → AnalyticFun K m G) (V : TopologicalSpace.Opens ↑↑(localModel K m G f).toPresheafedSpace) (W : TopologicalSpace.Opens (Kn K m)) (hVW : ∀ v ∈ V, Hom.toFun (localModel.ι K m G f) v ∈ W) (a : Fin n → ↑((affine K m).presheaf.obj (Opposite.op W))) {v : ↑↑(localModel K m G f).toPresheafedSpace} (hv : v ∈ V) (i : Fin n) : (CategoryTheory.ConcreteCategory.hom ((localModel K m G f).presheaf.germ ((localModel K m G f).imgOpens V ⊤) v ⋯)) ((Hom.pullbackΓ (modelPiece m G f V W hVW a)) (coordSection K n i)) = (CategoryTheory.ConcreteCategory.hom ((localModel K m G f).presheaf.germ ((TopologicalSpace.Opens.map (↑(localModel.ι K m G f)).base).obj W) v ⋯)) ((CategoryTheory.ConcreteCategory.hom ((↑(localModel.ι K m G f)).c.app (Opposite.op W))) (a i))

The germ at v ∈ V of the coordinate pullback of the piece is the germ of the class of a i (the pullback of a i along the closed immersion L ⟶ (Kᵐ, 𝒜)).

Local lifts of a global section of a local model

theorem AnalyticSpace.KLocallyRingedSpace.ι_c_app_apply {K : Type} [RCLike K] (m : ℕ) (G : TopologicalSpace.Opens (Kn K m)) {k : ℕ} (f : Fin k → AnalyticFun K m G) (W : TopologicalSpace.Opens (Kn K m)) (a : ↑((affine K m).presheaf.obj (Opposite.op W))) (z : ↥((TopologicalSpace.Opens.map (↑(localModel.ι K m G f)).base).obj W)) : ↑((CategoryTheory.ConcreteCategory.hom ((↑(localModel.ι K m G f)).c.app (Opposite.op W))) a) z = (Ideal.Quotient.mk (QuotientSpace.stalkIdeal (analyticSpaceOfOpen K m G).toLocallyRingedSpace (modelIdeal K m G f) ↑↑z)) ((CategoryTheory.ConcreteCategory.hom (((affine K m).restrictOpen G).presheaf.germ ((TopologicalSpace.Opens.map (↑((affine K m).ofRestrict G)).base).obj W) ↑↑z ⋯)) ((CategoryTheory.ConcreteCategory.hom ((↑((affine K m).ofRestrict G)).c.app (Opposite.op W))) a))

The sheaf map of the closed immersion ι : L ⟶ (Kᵐ, 𝒜) on a section over W, at a point: the class of the germ of the restriction of the section to G.

theorem AnalyticSpace.KLocallyRingedSpace.exists_lift_near {K : Type} [RCLike K] (m : ℕ) (G : TopologicalSpace.Opens (Kn K m)) {k : ℕ} (f : Fin k → AnalyticFun K m G) (σ : ↑((localModel K m G f).presheaf.obj (Opposite.op ⊤))) (y : ↑↑(localModel K m G f).toPresheafedSpace) : ∃ (V : TopologicalSpace.Opens ↑↑(localModel K m G f).toPresheafedSpace) (_ : y ∈ V) (W : TopologicalSpace.Opens (Kn K m)) (hVW : ∀ v ∈ V, Hom.toFun (localModel.ι K m G f) v ∈ W) (a : ↑((affine K m).presheaf.obj (Opposite.op W))), ∀ (v : ↑↑(localModel K m G f).toPresheafedSpace) (hv : v ∈ V), (CategoryTheory.ConcreteCategory.hom ((localModel K m G f).presheaf.germ ((TopologicalSpace.Opens.map (↑(localModel.ι K m G f)).base).obj W) v ⋯)) ((CategoryTheory.ConcreteCategory.hom ((↑(localModel.ι K m G f)).c.app (Opposite.op W))) a) = (CategoryTheory.ConcreteCategory.hom ((localModel K m G f).presheaf.germ ⊤ v trivial)) σ

A global section σ of a local model is, near every point y, the class family of an ambient analytic function a on an open W ⊆ Kᵐ: the germ of ι^*a at every point of an open V ∋ y is the germ of σ.

The morphism of a local model from n global sections

structure AnalyticSpace.KLocallyRingedSpace.LiftData {K : Type} [RCLike K] {n : ℕ} (m : ℕ) (G : TopologicalSpace.Opens (Kn K m)) {k : ℕ} (f : Fin k → AnalyticFun K m G) (σ : Fin n → ↑((localModel K m G f).presheaf.obj (Opposite.op ⊤))) (y : ↑↑(localModel K m G f).toPresheafedSpace) : Type u

Lift data at a point y for n global sections simultaneously.

• V : TopologicalSpace.Opens ↑↑(localModel K m G f).toPresheafedSpace

  The open neighbourhood of y on which the lifts exist.

• mem : y ∈ self.V
• W : TopologicalSpace.Opens (Kn K m)

  The ambient open of Kᵐ.

• hVW (v : ↑↑(localModel K m G f).toPresheafedSpace) : v ∈ self.V → Hom.toFun (localModel.ι K m G f) v ∈ self.W
• a : Fin n → ↑((affine K m).presheaf.obj (Opposite.op self.W))

  The ambient lifts.

• spec (i : Fin n) (v : ↑↑(localModel K m G f).toPresheafedSpace) (hv : v ∈ self.V) : (CategoryTheory.ConcreteCategory.hom ((localModel K m G f).presheaf.germ ((TopologicalSpace.Opens.map (↑(localModel.ι K m G f)).base).obj self.W) v ⋯)) ((CategoryTheory.ConcreteCategory.hom ((↑(localModel.ι K m G f)).c.app (Opposite.op self.W))) (self.a i)) = (CategoryTheory.ConcreteCategory.hom ((localModel K m G f).presheaf.germ ⊤ v trivial)) (σ i)

theorem AnalyticSpace.KLocallyRingedSpace.nonempty_liftData {K : Type} [RCLike K] {n : ℕ} (m : ℕ) (G : TopologicalSpace.Opens (Kn K m)) {k : ℕ} (f : Fin k → AnalyticFun K m G) (σ : Fin n → ↑((localModel K m G f).presheaf.obj (Opposite.op ⊤))) (y : ↑↑(localModel K m G f).toPresheafedSpace) : Nonempty (LiftData m G f σ y)

noncomputable def AnalyticSpace.KLocallyRingedSpace.liftData {K : Type} [RCLike K] {n : ℕ} (m : ℕ) (G : TopologicalSpace.Opens (Kn K m)) {k : ℕ} (f : Fin k → AnalyticFun K m G) (σ : Fin n → ↑((localModel K m G f).presheaf.obj (Opposite.op ⊤))) (y : ↑↑(localModel K m G f).toPresheafedSpace) : LiftData m G f σ y

A choice of lift data at every point.

Equations

• AnalyticSpace.KLocallyRingedSpace.liftData m G f σ y = Classical.choice ⋯

@[reducible, inline]

noncomputable abbrev AnalyticSpace.KLocallyRingedSpace.liftPiece {K : Type} [RCLike K] {n : ℕ} (m : ℕ) (G : TopologicalSpace.Opens (Kn K m)) {k : ℕ} (f : Fin k → AnalyticFun K m G) (σ : Fin n → ↑((localModel K m G f).presheaf.obj (Opposite.op ⊤))) (y : ↑↑(localModel K m G f).toPresheafedSpace) : (localModel K m G f).restrictOpen (liftData m G f σ y).V ⟶ affine K n

The piece at y.

Equations

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

theorem AnalyticSpace.KLocallyRingedSpace.germ_pullbackΓ_liftPiece_coord {K : Type} [RCLike K] {n : ℕ} (m : ℕ) (G : TopologicalSpace.Opens (Kn K m)) {k : ℕ} (f : Fin k → AnalyticFun K m G) (σ : Fin n → ↑((localModel K m G f).presheaf.obj (Opposite.op ⊤))) (y : ↑↑(localModel K m G f).toPresheafedSpace) {z : ↑↑(localModel K m G f).toPresheafedSpace} (hz : z ∈ (liftData m G f σ y).V) (i : Fin n) : (CategoryTheory.ConcreteCategory.hom ((localModel K m G f).presheaf.germ ((localModel K m G f).imgOpens (liftData m G f σ y).V ⊤) z ⋯)) ((Hom.pullbackΓ (liftPiece m G f σ y)) (coordSection K n i)) = (CategoryTheory.ConcreteCategory.hom ((localModel K m G f).presheaf.germ ⊤ z trivial)) (σ i)

The germ of the coordinate pullback of the piece at y is the germ of σ i.

theorem AnalyticSpace.KLocallyRingedSpace.hcoord_liftPiece {K : Type} [RCLike K] {n : ℕ} (m : ℕ) (G : TopologicalSpace.Opens (Kn K m)) {k : ℕ} (f : Fin k → AnalyticFun K m G) (σ : Fin n → ↑((localModel K m G f).presheaf.obj (Opposite.op ⊤))) (y y' : ↑↑(localModel K m G f).toPresheafedSpace) {z : ↑↑(localModel K m G f).toPresheafedSpace} (hz : z ∈ (liftData m G f σ y).V) (hz' : z ∈ (liftData m G f σ y').V) (i : Fin n) : (CategoryTheory.ConcreteCategory.hom ((localModel K m G f).presheaf.germ ((localModel K m G f).imgOpens (liftData m G f σ y).V ⊤) z ⋯)) ((Hom.pullbackΓ (liftPiece m G f σ y)) (coordSection K n i)) = (CategoryTheory.ConcreteCategory.hom ((localModel K m G f).presheaf.germ ((localModel K m G f).imgOpens (liftData m G f σ y').V ⊤) z ⋯)) ((Hom.pullbackΓ (liftPiece m G f σ y')) (coordSection K n i))

theorem AnalyticSpace.KLocallyRingedSpace.germ_pullbackΓ_liftPiece_coord' {K : Type} [RCLike K] {n : ℕ} (m : ℕ) (G : TopologicalSpace.Opens (Kn K m)) {k : ℕ} (f : Fin k → AnalyticFun K m G) (σ : Fin n → ↑((localModel K m G f).presheaf.obj (Opposite.op ⊤))) (y : ↑↑(localModel K m G f).toPresheafedSpace) {z : ↑↑(localModel K m G f).toPresheafedSpace} (hz : z ∈ (liftData m G f σ y).V) (i : Fin n) : (CategoryTheory.ConcreteCategory.hom ((localModel K m G f).presheaf.germ ((localModel K m G f).imgOpens (liftData m G f σ y).V ((TopologicalSpace.Opens.map (↑(liftPiece m G f σ y)).base).obj ⊤)) z ⋯)) ((Hom.pullbackΓ (liftPiece m G f σ y)) (coordSection K n i)) = (CategoryTheory.ConcreteCategory.hom ((localModel K m G f).presheaf.germ ⊤ z trivial)) (σ i)

The germ of the coordinate pullback of the piece at y, over the open in the form of glueHomAffine's locV.

theorem AnalyticSpace.KLocallyRingedSpace.base_liftPiece_eq {K : Type} [RCLike K] {n : ℕ} (m : ℕ) (G : TopologicalSpace.Opens (Kn K m)) {k : ℕ} (f : Fin k → AnalyticFun K m G) (σ : Fin n → ↑((localModel K m G f).presheaf.obj (Opposite.op ⊤))) (y y' : ↑↑(localModel K m G f).toPresheafedSpace) {z : ↑↑(localModel K m G f).toPresheafedSpace} (hz : z ∈ (liftData m G f σ y).V) (hz' : z ∈ (liftData m G f σ y').V) : (CategoryTheory.ConcreteCategory.hom (↑(liftPiece m G f σ y)).base) ⟨z, hz⟩ = (CategoryTheory.ConcreteCategory.hom (↑(liftPiece m G f σ y')).base) ⟨z, hz'⟩

theorem AnalyticSpace.KLocallyRingedSpace.germ_c_app_liftPiece_eq {K : Type} [RCLike K] {n : ℕ} (m : ℕ) (G : TopologicalSpace.Opens (Kn K m)) {k : ℕ} (f : Fin k → AnalyticFun K m G) (σ : Fin n → ↑((localModel K m G f).presheaf.obj (Opposite.op ⊤))) (y y' : ↑↑(localModel K m G f).toPresheafedSpace) (V : TopologicalSpace.Opens (Kn K n)) (F : ↑((affine K n).presheaf.obj (Opposite.op V))) (z : ↑↑(localModel K m G f).toPresheafedSpace) (hzi : z ∈ (localModel K m G f).locV (fun (y : ↑↑(localModel K m G f).toPresheafedSpace) => (liftData m G f σ y).V) (liftPiece m G f σ) y V) (hzj : z ∈ (localModel K m G f).locV (fun (y : ↑↑(localModel K m G f).toPresheafedSpace) => (liftData m G f σ y).V) (liftPiece m G f σ) y' V) : (CategoryTheory.ConcreteCategory.hom ((localModel K m G f).presheaf.germ ((localModel K m G f).locV (fun (y : ↑↑(localModel K m G f).toPresheafedSpace) => (liftData m G f σ y).V) (liftPiece m G f σ) y V) z hzi)) ((localModel K m G f).locSec (fun (y : ↑↑(localModel K m G f).toPresheafedSpace) => (liftData m G f σ y).V) (liftPiece m G f σ) y V F) = (CategoryTheory.ConcreteCategory.hom ((localModel K m G f).presheaf.germ ((localModel K m G f).locV (fun (y : ↑↑(localModel K m G f).toPresheafedSpace) => (liftData m G f σ y).V) (liftPiece m G f σ) y' V) z hzj)) ((localModel K m G f).locSec (fun (y : ↑↑(localModel K m G f).toPresheafedSpace) => (liftData m G f σ y).V) (liftPiece m G f σ) y' V F)

theorem AnalyticSpace.KLocallyRingedSpace.liftCover {K : Type} [RCLike K] {n : ℕ} (m : ℕ) (G : TopologicalSpace.Opens (Kn K m)) {k : ℕ} (f : Fin k → AnalyticFun K m G) (σ : Fin n → ↑((localModel K m G f).presheaf.obj (Opposite.op ⊤))) (z : ↑↑(localModel K m G f).toPresheafedSpace) : ∃ (y : ↑↑(localModel K m G f).toPresheafedSpace), z ∈ (fun (y : ↑↑(localModel K m G f).toPresheafedSpace) => (liftData m G f σ y).V) y

The cover of L by the lifting opens.

theorem AnalyticSpace.KLocallyRingedSpace.liftPiece_hbase {K : Type} [RCLike K] {n : ℕ} (m : ℕ) (G : TopologicalSpace.Opens (Kn K m)) {k : ℕ} (f : Fin k → AnalyticFun K m G) (σ : Fin n → ↑((localModel K m G f).presheaf.obj (Opposite.op ⊤))) (y y' z : ↑↑(localModel K m G f).toPresheafedSpace) (hz : z ∈ (fun (y : ↑↑(localModel K m G f).toPresheafedSpace) => (liftData m G f σ y).V) y) (hz' : z ∈ (fun (y : ↑↑(localModel K m G f).toPresheafedSpace) => (liftData m G f σ y).V) y') : (CategoryTheory.ConcreteCategory.hom (↑(liftPiece m G f σ y)).base) ⟨z, hz⟩ = (CategoryTheory.ConcreteCategory.hom (↑(liftPiece m G f σ y')).base) ⟨z, hz'⟩

noncomputable def AnalyticSpace.KLocallyRingedSpace.localModel.homOfSections {K : Type} [RCLike K] {n : ℕ} (m : ℕ) (G : TopologicalSpace.Opens (Kn K m)) {k : ℕ} (f : Fin k → AnalyticFun K m G) (σ : Fin n → ↑((localModel K m G f).presheaf.obj (Opposite.op ⊤))) : localModel K m G f ⟶ affine K n

The local-model case: the K-morphism L ⟶ (Kⁿ, 𝒜) with coordinate pullbacks σ₁, …, σₙ, glued from the pieces.

Equations

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

theorem AnalyticSpace.KLocallyRingedSpace.localModel.pullbackΓ_homOfSections_coordSection {K : Type} [RCLike K] {n : ℕ} (m : ℕ) (G : TopologicalSpace.Opens (Kn K m)) {k : ℕ} (f : Fin k → AnalyticFun K m G) (σ : Fin n → ↑((localModel K m G f).presheaf.obj (Opposite.op ⊤))) (i : Fin n) : (Hom.pullbackΓ (homOfSections m G f σ)) (coordSection K n i) = σ i

The coordinate pullbacks of localModel.homOfSections σ are the σ i.