Lifting a morphism to Kⁿ into a manifold through a chart

A K-morphism χ : X → (Kⁿ, 𝒜) from a K-local-ringed space whose values lie in G = ψ(Φ.target), the domain of a chart Φ of a manifold M', lifts to a K-morphism chartLift : X → Sp(M') with image in Φ.source, namely X ≅ X|⊤ → (Kⁿ, 𝒜)|G ≅ Sp(G) → Sp(M') (restrictOpenTopIso, Hom.restrictTo, ofManifold_restrictOpen_iso, and Sp of the inverse chart chartFromOpens of Hironaka/AnalyticSpace/Manifold/Chart.lean). Its base point is Φ⁻¹ (ψ⁻¹ (χ x)) (chartLift_base) and it pulls the coordinate germs u_j of Φ back to the pulled-back coordinates χ^* z_j (stalkMap_chartLift_coord); with the morphisms from sections of Hironaka/AnalyticSpace/HomOfSections.lean this produces the local lifts through the charted blow-up. The open subspace (G, 𝒜_G) is Hironaka's [Hir64, Ch. 0, §1, p. 119]; that a morphism into (Kⁿ, 𝒜) is determined by its coordinate functions is the library's (hom_ext_of_coord, Hironaka/AnalyticSpace/HomExt.lean; compare the local Kⁿ-coordinations of [Hir64, Ch. 0, §1, p. 120]). The lemmas are general (any K-local-ringed space X, any chart of any analytic manifold); also used by Hironaka/Manifold/Sequence/Restrict/.

theorem AnalyticSpace.KLocallyRingedSpace.stalkMap_comp_apply {K : Type} [RCLike K] {X Y W : KLocallyRingedSpace K} (f : X ⟶ Y) (g : Y ⟶ W) (x : ↑↑X.toPresheafedSpace) (s : ↑(W.presheaf.stalk ((CategoryTheory.ConcreteCategory.hom (↑g).base) ((CategoryTheory.ConcreteCategory.hom (↑f).base) x)))) : (CommRingCat.Hom.hom (AlgebraicGeometry.LocallyRingedSpace.Hom.stalkMap (↑(CategoryTheory.CategoryStruct.comp f g)) x)) s = (CommRingCat.Hom.hom (AlgebraicGeometry.LocallyRingedSpace.Hom.stalkMap (↑f) x)) ((CommRingCat.Hom.hom (AlgebraicGeometry.LocallyRingedSpace.Hom.stalkMap (↑g) ((CategoryTheory.ConcreteCategory.hom (↑f).base) x))) s)

The stalk map of a composite of K-morphisms, elementwise.

theorem AnalyticSpace.KLocallyRingedSpace.restrictOpenTopIso_hom {K : Type} [RCLike K] (X : KLocallyRingedSpace K) : X.restrictOpenTopIso.hom = X.ofRestrict ⊤

The isomorphism X | ⊤ ≅ X (restrictOpenTopIso) is, as a morphism, the open immersion X | ⊤ ⟶ X.

theorem AnalyticSpace.KLocallyRingedSpace.restrictOpenTopIso_inv_comp_ofRestrict {K : Type} [RCLike K] (X : KLocallyRingedSpace K) : CategoryTheory.CategoryStruct.comp X.restrictOpenTopIso.inv (X.ofRestrict ⊤) = CategoryTheory.CategoryStruct.id X

X ⟶ X | ⊤ ⟶ X is the identity.

theorem AnalyticSpace.KLocallyRingedSpace.stalkMap_apply_coordAt_congr {K : Type} [RCLike K] {n : ℕ} {Y : KLocallyRingedSpace K} {F₁ F₂ : Y ⟶ affine K n} (h : F₁ = F₂) (y : ↑↑Y.toPresheafedSpace) (j : Fin n) : (CommRingCat.Hom.hom (AlgebraicGeometry.LocallyRingedSpace.Hom.stalkMap (↑F₁) y)) (coordAt K n ((CategoryTheory.ConcreteCategory.hom (↑F₁).base) y) j) = (CommRingCat.Hom.hom (AlgebraicGeometry.LocallyRingedSpace.Hom.stalkMap (↑F₂) y)) (coordAt K n ((CategoryTheory.ConcreteCategory.hom (↑F₂).base) y) j)

Transport of a pulled-back coordinate germ of Kⁿ along an equality of morphisms.

theorem AnalyticSpace.KLocallyRingedSpace.contMDiff_val_chartFromOpens {K : Type} [RCLike K] {E : Type u_1} [NormedAddCommGroup E] [NormedSpace K E] {n : ℕ} (ψ : E ≃L[K] Fin n → K) {M' : Type u} [TopologicalSpace M'] [ChartedSpace E M'] {Φ : OpenPartialHomeomorph M' E} (hΦ : Φ ∈ IsManifold.maximalAtlas (modelWithCornersSelf K E) ⊤ M') : ContMDiff (modelWithCornersSelf K (Kn K n)) (modelWithCornersSelf K E) ⊤ fun (y : ↥(chartOpens ψ Φ)) => ↑(chartFromOpens ψ Φ y)

The inverse chart G → M', y ↦ Φ⁻¹ (ψ⁻¹ y), is analytic (chartFromOpens).

noncomputable def AnalyticSpace.KLocallyRingedSpace.chartFromOpensHom {K : Type} [RCLike K] {E : Type u_1} [NormedAddCommGroup E] [NormedSpace K E] {n : ℕ} (ψ : E ≃L[K] Fin n → K) {M' : Type u} [TopologicalSpace M'] [ChartedSpace E M'] {Φ : OpenPartialHomeomorph M' E} (hΦ : Φ ∈ IsManifold.maximalAtlas (modelWithCornersSelf K E) ⊤ M') : ofManifold K (Kn K n) ↥(chartOpens ψ Φ) ⟶ ofManifold K E M'

Sp(G) → Sp(M'), y ↦ Φ⁻¹ (ψ⁻¹ y).

Equations

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

noncomputable def AnalyticSpace.KLocallyRingedSpace.chartOpensHom {K : Type} [RCLike K] {E : Type u_1} [NormedAddCommGroup E] [NormedSpace K E] {n : ℕ} (ψ : E ≃L[K] Fin n → K) {M' : Type u} [TopologicalSpace M'] [ChartedSpace E M'] {Φ : OpenPartialHomeomorph M' E} (hΦ : Φ ∈ IsManifold.maximalAtlas (modelWithCornersSelf K E) ⊤ M') : (affine K n).restrictOpen (chartOpens ψ Φ) ⟶ ofManifold K E M'

(Kⁿ, 𝒜)|G ⟶ Sp(M').

Equations

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

theorem AnalyticSpace.KLocallyRingedSpace.germMap_chartFromOpens_coord {K : Type} [RCLike K] {E : Type u_1} [NormedAddCommGroup E] [NormedSpace K E] {n : ℕ} (ψ : E ≃L[K] Fin n → K) {M' : Type u} [TopologicalSpace M'] [ChartedSpace E M'] {Φ : OpenPartialHomeomorph M' E} (hΦ : Φ ∈ IsManifold.maximalAtlas (modelWithCornersSelf K E) ⊤ M') (c : ↥(chartOpens ψ Φ)) (hc : ↑(chartFromOpens ψ Φ c) ∈ Φ.source) (j : Fin n) : (Manifold.germMap (fun (y : ↥(chartOpens ψ Φ)) => ↑(chartFromOpens ψ Φ y)) ⋯ c) (Manifold.coord E ψ Φ hΦ hc j) = (Manifold.germMap Subtype.val ⋯ c) (coordAt K n (↑c) j)

The inverse chart Sp(G) → Sp(M') pulls the coordinate germ u_j of Φ back to the coordinate germ z_j of Kⁿ, both read on G ⊆ Kⁿ.

noncomputable def AnalyticSpace.KLocallyRingedSpace.chartLift {K : Type} [RCLike K] {E : Type u_1} [NormedAddCommGroup E] [NormedSpace K E] {n : ℕ} (ψ : E ≃L[K] Fin n → K) {M' : Type u} [TopologicalSpace M'] [ChartedSpace E M'] {Φ : OpenPartialHomeomorph M' E} (hΦ : Φ ∈ IsManifold.maximalAtlas (modelWithCornersSelf K E) ⊤ M') {X : KLocallyRingedSpace K} (χ : X ⟶ affine K n) (hval : ∀ (x : ↑↑X.toPresheafedSpace), Hom.toFun χ x ∈ chartOpens ψ Φ) : X ⟶ ofManifold K E M'

The lift into Sp(M') through the chart Φ of a K-morphism χ : X → Kⁿ with values in ψ(Φ.target).

Equations

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

theorem AnalyticSpace.KLocallyRingedSpace.chartLift_base {K : Type} [RCLike K] {E : Type u_1} [NormedAddCommGroup E] [NormedSpace K E] {n : ℕ} (ψ : E ≃L[K] Fin n → K) {M' : Type u} [TopologicalSpace M'] [ChartedSpace E M'] {Φ : OpenPartialHomeomorph M' E} (hΦ : Φ ∈ IsManifold.maximalAtlas (modelWithCornersSelf K E) ⊤ M') {X : KLocallyRingedSpace K} (χ : X ⟶ affine K n) (hval : ∀ (x : ↑↑X.toPresheafedSpace), Hom.toFun χ x ∈ chartOpens ψ Φ) (x : ↑↑X.toPresheafedSpace) : (CategoryTheory.ConcreteCategory.hom (↑(chartLift ψ hΦ χ hval)).base) x = ↑Φ.symm (ψ.symm ((CategoryTheory.ConcreteCategory.hom (↑χ).base) x).down)

The base point of the chart lift: Φ⁻¹ (ψ⁻¹ (χ x)).

theorem AnalyticSpace.KLocallyRingedSpace.chartLift_base_mem {K : Type} [RCLike K] {E : Type u_1} [NormedAddCommGroup E] [NormedSpace K E] {n : ℕ} (ψ : E ≃L[K] Fin n → K) {M' : Type u} [TopologicalSpace M'] [ChartedSpace E M'] {Φ : OpenPartialHomeomorph M' E} (hΦ : Φ ∈ IsManifold.maximalAtlas (modelWithCornersSelf K E) ⊤ M') {X : KLocallyRingedSpace K} (χ : X ⟶ affine K n) (hval : ∀ (x : ↑↑X.toPresheafedSpace), Hom.toFun χ x ∈ chartOpens ψ Φ) (x : ↑↑X.toPresheafedSpace) : (CategoryTheory.ConcreteCategory.hom (↑(chartLift ψ hΦ χ hval)).base) x ∈ Φ.source

The chart lift lands in the chart's source.

theorem AnalyticSpace.KLocallyRingedSpace.stalkMap_chartLift_coord {K : Type} [RCLike K] {E : Type u_1} [NormedAddCommGroup E] [NormedSpace K E] {n : ℕ} (ψ : E ≃L[K] Fin n → K) {M' : Type u} [TopologicalSpace M'] [ChartedSpace E M'] {Φ : OpenPartialHomeomorph M' E} (hΦ : Φ ∈ IsManifold.maximalAtlas (modelWithCornersSelf K E) ⊤ M') {X : KLocallyRingedSpace K} (χ : X ⟶ affine K n) (hval : ∀ (x : ↑↑X.toPresheafedSpace), Hom.toFun χ x ∈ chartOpens ψ Φ) (x : ↑↑X.toPresheafedSpace) (j : Fin n) : (CommRingCat.Hom.hom (AlgebraicGeometry.LocallyRingedSpace.Hom.stalkMap (↑(chartLift ψ hΦ χ hval)) x)) (Manifold.coord E ψ Φ hΦ ⋯ j) = (CommRingCat.Hom.hom (AlgebraicGeometry.LocallyRingedSpace.Hom.stalkMap (↑χ) x)) (coordAt K n ((CategoryTheory.ConcreteCategory.hom (↑χ).base) x) j)

The chart lift pulls the coordinate germs u_j of Φ back to the pulled-back coordinate germs χ^* z_j — the stalk-level description of the lift, through the four factors X ≅ X|⊤ → (Kⁿ,𝒜)|G ≅ Sp(G) → Sp(M').