K-morphisms (Kᵐ, 𝒜)|W ⟶ (Kⁿ, 𝒜) from n analytic functions on W

The affine case of the existence of a morphism into Kⁿ with prescribed coordinate functions: n analytic functions a₁, …, aₙ on an open W ⊆ Kᵐ define the K-morphism (W, 𝒜_W) ⟶ (Kⁿ, 𝒜_{Kⁿ}), w ↦ (a₁(w), …, aₙ(w)) — the morphism ofManifoldHom of the analytic map W → Kⁿ, transported to the open subspace (Kᵐ, 𝒜)|W along ofManifold_restrictOpen_iso (Hironaka/AnalyticSpace/Manifold/Restrict.lean). Its coordinate pullbacks are the a_i (pullbackΓ_homOfSectionsAffine_coordSection): the germ of the pullback of z_i at w is computed through the stalk maps of the two factors (stalkMap_comp), the transport being controlled by ofManifold_restrictOpen_iso_hom_comp and the identification of the stalks of (Kᵐ, 𝒜)|W with those of 𝒜 (resIso). Routine.

def AnalyticSpace.KLocallyRingedSpace.affineMap {K : Type} [RCLike K] {m n : ℕ} (W : TopologicalSpace.Opens (Kn K m)) (a : Fin n → ↑((affine K m).presheaf.obj (Opposite.op W))) : ↥W → Kn K n

The analytic map W → Kⁿ with components a i.

Equations

• AnalyticSpace.KLocallyRingedSpace.affineMap W a w = { down := fun (i : Fin n) => ↑(a i) w }

theorem AnalyticSpace.KLocallyRingedSpace.contMDiff_affineMap {K : Type} [RCLike K] {m n : ℕ} (W : TopologicalSpace.Opens (Kn K m)) (a : Fin n → ↑((affine K m).presheaf.obj (Opposite.op W))) : ContMDiff (modelWithCornersSelf K (Kn K m)) (modelWithCornersSelf K (Kn K n)) ⊤ (affineMap W a)

@[reducible, inline]

noncomputable abbrev AnalyticSpace.KLocallyRingedSpace.affineRestrictIso {K : Type} [RCLike K] {m : ℕ} (W : TopologicalSpace.Opens (Kn K m)) : (affine K m).restrictOpen W ≅ ofManifold K (Kn K m) ↥W

The identification (Kᵐ, 𝒜)|W ≅ Sp(W) of the open subspace with the space of the manifold W.

Equations

• AnalyticSpace.KLocallyRingedSpace.affineRestrictIso W = AnalyticSpace.KLocallyRingedSpace.ofManifold_restrictOpen_iso W

noncomputable def AnalyticSpace.KLocallyRingedSpace.homOfSectionsAffine {K : Type} [RCLike K] {m n : ℕ} (W : TopologicalSpace.Opens (Kn K m)) (a : Fin n → ↑((affine K m).presheaf.obj (Opposite.op W))) : (affine K m).restrictOpen W ⟶ affine K n

The affine case: the K-morphism (Kᵐ, 𝒜)|W ⟶ (Kⁿ, 𝒜) with coordinate functions a₁, …, aₙ.

Equations

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

theorem AnalyticSpace.KLocallyRingedSpace.affineRestrictIso_hom_base {K : Type} [RCLike K] {m : ℕ} (W : TopologicalSpace.Opens (Kn K m)) (w : ↑↑((affine K m).restrictOpen W).toPresheafedSpace) : (CategoryTheory.ConcreteCategory.hom (↑(affineRestrictIso W).hom).base) w = w

The identification (Kᵐ, 𝒜)|W ≅ Sp(W) is the identity on points.

theorem AnalyticSpace.KLocallyRingedSpace.toFun_homOfSectionsAffine {K : Type} [RCLike K] {m n : ℕ} (W : TopologicalSpace.Opens (Kn K m)) (a : Fin n → ↑((affine K m).presheaf.obj (Opposite.op W))) (w : ↑↑((affine K m).restrictOpen W).toPresheafedSpace) : Hom.toFun (homOfSectionsAffine W a) w = affineMap W a w

@[reducible, inline]

noncomputable abbrev AnalyticSpace.KLocallyRingedSpace.affineMapHom {K : Type} [RCLike K] {m n : ℕ} (W : TopologicalSpace.Opens (Kn K m)) (a : Fin n → ↑((affine K m).presheaf.obj (Opposite.op W))) : ofManifold K (Kn K m) ↥W ⟶ affine K n

The analytic map W → Kⁿ as a K-morphism Sp(W) ⟶ (Kⁿ, 𝒜).

Equations

• AnalyticSpace.KLocallyRingedSpace.affineMapHom W a = AnalyticSpace.KLocallyRingedSpace.ofManifoldHom (AnalyticSpace.KLocallyRingedSpace.affineMap W a) ⋯

@[reducible, inline]

noncomputable abbrev AnalyticSpace.KLocallyRingedSpace.affineIncl {K : Type} [RCLike K] {m : ℕ} (W : TopologicalSpace.Opens (Kn K m)) : ofManifold K (Kn K m) ↥W ⟶ affine K m

The inclusion W → Kᵐ as a K-morphism Sp(W) ⟶ (Kᵐ, 𝒜).

Equations

• AnalyticSpace.KLocallyRingedSpace.affineIncl W = AnalyticSpace.KLocallyRingedSpace.ofManifoldHom Subtype.val ⋯

theorem AnalyticSpace.KLocallyRingedSpace.affineRestrictIso_hom_comp_affineIncl {K : Type} [RCLike K] {m : ℕ} (W : TopologicalSpace.Opens (Kn K m)) : CategoryTheory.CategoryStruct.comp (affineRestrictIso W).hom (affineIncl W) = (affine K m).ofRestrict W

theorem AnalyticSpace.KLocallyRingedSpace.resIso_germ_pullbackΓ_homOfSectionsAffine_coord {K : Type} [RCLike K] {m n : ℕ} (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 (resIso (affine K m) W ⋯).hom) ((CategoryTheory.ConcreteCategory.hom (((affine K m).restrictOpen W).presheaf.germ ⊤ w trivial)) ((Hom.pullbackΓ (homOfSectionsAffine W a)) (coordSection K n i))) = (CategoryTheory.ConcreteCategory.hom ((affine K m).presheaf.germ W ↑w ⋯)) (a i)

The germ at w of the pullback of a coordinate function along homOfSectionsAffine W a, seen in the stalk of 𝒜 at w, is the germ of a i.

theorem AnalyticSpace.KLocallyRingedSpace.pullbackΓ_homOfSectionsAffine_coordSection {K : Type} [RCLike K] {m n : ℕ} (W : TopologicalSpace.Opens (Kn K m)) (a : Fin n → ↑((affine K m).presheaf.obj (Opposite.op W))) (i : Fin n) : (Hom.pullbackΓ (homOfSectionsAffine W a)) (coordSection K n i) = (CategoryTheory.ConcreteCategory.hom ((affine K m).presheaf.map (CategoryTheory.homOfLE ⋯).op)) (a i)

The coordinate pullbacks of homOfSectionsAffine W a are the a i (restricted to the image of ⊤, which is W).