The model stalk map of a piece embedding and the local lifts

Kollár's Lemma 39 works in coordinates: the two embeddings i₁ : Y → 𝕜ⁿ, i₂ : Y → 𝕜ᵐ of one piece are compared through local analytic maps j₂ : 𝕜ⁿ ⇀ 𝕜ᵐ, j₁ : 𝕜ᵐ ⇀ 𝕜ⁿ with j₂ ∘ i₁ = i₂ and j₁ ∘ i₂ = i₁ near a point — the coordinate functions of one embedding, pulled back to Y, extend to analytic functions on the other ambient [Kol07, Lemma 39, proof]; a morphism of analytic spaces is described locally by its coordinate functions (Hironaka's local K-coordinations, [Hir64, Ch. 0, §1, p. 120]). This module provides that step:

• the coordinate map pieceCoord G : Sp(G) → 𝕜ⁿ of a one-piece ambient and its chart (pieceAmbientChart, the chart of Sp(G) at any point as a partial analytic isomorphism onto its target — the sources are the whole ambient);
• the model coordinate germs modelCoordGerm v k of 𝕜ⁿ at v and the model germs modelGerm f hf hv of functions analytic on an open O ∋ v, with their germs of functions;
• the model stalk map E.modelStalkMap y : 𝒪_{𝕜ⁿ, i(y)} →+* 𝒪_{X|V, y} of a piece embedding E at y — the stalk map of the K-morphism X|V → Sp(G) → Sp(𝕜ⁿ), which is pieceStalkMap after the coordinate germ map; it is local and carries constants to constants;
• the local lift (exists_modelLift): for two embeddings E, F of one piece and a point x there is an open O ∋ i_E(x) of 𝕜ⁿ and j : 𝕜ⁿ → 𝕜ᵐ analytic on O whose components, pulled back through E, are the coordinates of F at every y over O — from the local description of the sections of Sp(G)/𝓘 (exists_local_rep) applied to the coordinate functions of F pulled back to Sp(G)/𝓘 along E⁻¹ ∘ F, read through the chart;
• the residues (modelPoint_eq_of_coord_eq): such a lift takes i_E(y) to i_F(y) (a germ congruent to two constants modulo the maximal ideal has equal constants);
• the uniqueness (modelStalkMap_eq_of_lift): a lift with the coordinate identities gives ε_F = ε_E ∘ j^* on every germ (stalkMap_eq_of_coord, the stalks being Noetherian).

Not in the sources beyond Kollár's proof; bookkeeping on the local description of sections of a closed subspace (Hironaka/AnalyticSpace/Manifold/ClosedSub.lean) and the uniqueness of local homomorphisms determined by coordinates (Hironaka/AnalyticSpace/MonoidalUnique.lean).

The coordinate map and the chart of a one-piece ambient

def Hironaka.Manifold.pieceCoord {𝕜 : Type} [RCLike 𝕜] {n : ℕ} (G : TopologicalSpace.Opens (Fin n → 𝕜)) : (pieceAmbient 𝕜 G).carrier → Fin n → 𝕜

The coordinate map ⟨(), z⟩ ↦ z of the one-piece ambient Sp(G) = ⊔_{PUnit} G.

Equations

• Hironaka.Manifold.pieceCoord G w = ↑w.snd

theorem Hironaka.Manifold.pieceCoord_apply {𝕜 : Type} [RCLike 𝕜] {n : ℕ} (G : TopologicalSpace.Opens (Fin n → 𝕜)) (w : (pieceAmbient 𝕜 G).carrier) : pieceCoord G w = ↑w.snd

theorem Hironaka.Manifold.pieceCoord_mem {𝕜 : Type} [RCLike 𝕜] {n : ℕ} (G : TopologicalSpace.Opens (Fin n → 𝕜)) (w : (pieceAmbient 𝕜 G).carrier) : pieceCoord G w ∈ G

theorem Hironaka.Manifold.pieceCoord_injective {𝕜 : Type} [RCLike 𝕜] {n : ℕ} (G : TopologicalSpace.Opens (Fin n → 𝕜)) : Function.Injective (pieceCoord G)

theorem Hironaka.Manifold.contMDiff_pieceCoord {𝕜 : Type} [RCLike 𝕜] {n : ℕ} (G : TopologicalSpace.Opens (Fin n → 𝕜)) : ContMDiff (modelWithCornersSelf 𝕜 (Fin n → 𝕜)) (modelWithCornersSelf 𝕜 (Fin n → 𝕜)) ⊤ (pieceCoord G)

theorem Hironaka.Manifold.chartAt_pieceAmbient_apply_eq_pieceCoord {𝕜 : Type} [RCLike 𝕜] {n : ℕ} (G : TopologicalSpace.Opens (Fin n → 𝕜)) (x y : (pieceAmbient 𝕜 G).carrier) : ↑(chartAt (Fin n → 𝕜) x) y = pieceCoord G y

The chart of the one-piece ambient at any point is the coordinate map (the lifted chart of the open G ⊆ 𝕜ⁿ; PadIdeal.lean's chartAt_pieceAmbient_apply for an arbitrary open).

theorem Hironaka.Manifold.mem_chart_source_pieceAmbient {𝕜 : Type} [RCLike 𝕜] {n : ℕ} (G : TopologicalSpace.Opens (Fin n → 𝕜)) (x y : (pieceAmbient 𝕜 G).carrier) : y ∈ (chartAt (Fin n → 𝕜) x).source

The source of the chart of the one-piece ambient at any point is the whole ambient.

noncomputable def Hironaka.Manifold.pieceAmbientChart {𝕜 : Type} [RCLike 𝕜] {n : ℕ} (G : TopologicalSpace.Opens (Fin n → 𝕜)) (x : (pieceAmbient 𝕜 G).carrier) : PartialDiffeomorph (modelWithCornersSelf 𝕜 (Fin n → 𝕜)) (modelWithCornersSelf 𝕜 (Fin n → 𝕜)) (pieceAmbient 𝕜 G).carrier (Fin n → 𝕜) ⊤

The chart of the one-piece ambient at x, as a partial analytic isomorphism Sp(G) ⇀ 𝕜ⁿ (source the whole ambient, target the chart's target).

Equations

• Hironaka.Manifold.pieceAmbientChart G x = { toPartialEquiv := (chartAt (Fin n → 𝕜) x).toPartialEquiv, open_source := ⋯, open_target := ⋯, contMDiffOn_toFun := ⋯, contMDiffOn_invFun := ⋯ }

theorem Hironaka.Manifold.pieceAmbientChart_apply {𝕜 : Type} [RCLike 𝕜] {n : ℕ} (G : TopologicalSpace.Opens (Fin n → 𝕜)) (x y : (pieceAmbient 𝕜 G).carrier) : ↑(pieceAmbientChart G x).toPartialEquiv y = pieceCoord G y

theorem Hironaka.Manifold.mem_pieceAmbientChart_source {𝕜 : Type} [RCLike 𝕜] {n : ℕ} (G : TopologicalSpace.Opens (Fin n → 𝕜)) (x y : (pieceAmbient 𝕜 G).carrier) : y ∈ (pieceAmbientChart G x).source

theorem Hironaka.Manifold.pieceCoord_mem_pieceAmbientChart_target {𝕜 : Type} [RCLike 𝕜] {n : ℕ} (G : TopologicalSpace.Opens (Fin n → 𝕜)) (x y : (pieceAmbient 𝕜 G).carrier) : pieceCoord G y ∈ (pieceAmbientChart G x).target

theorem Hironaka.Manifold.pieceAmbientChart_symm_pieceCoord {𝕜 : Type} [RCLike 𝕜] {n : ℕ} (G : TopologicalSpace.Opens (Fin n → 𝕜)) (x y : (pieceAmbient 𝕜 G).carrier) : ↑(pieceAmbientChart G x).symm.toPartialEquiv (pieceCoord G y) = y

theorem Hironaka.Manifold.pieceCoord_pieceAmbientChart_symm {𝕜 : Type} [RCLike 𝕜] {n : ℕ} (G : TopologicalSpace.Opens (Fin n → 𝕜)) (x : (pieceAmbient 𝕜 G).carrier) {v : Fin n → 𝕜} (hv : v ∈ (pieceAmbientChart G x).target) : pieceCoord G (↑(pieceAmbientChart G x).symm.toPartialEquiv v) = v

The stalks of a one-piece ambient are the stalks of the model space

theorem Hironaka.Manifold.pieceCoord_eq_chartAt {𝕜 : Type} [RCLike 𝕜] {n : ℕ} (G : TopologicalSpace.Opens (Fin n → 𝕜)) (x : (pieceAmbient 𝕜 G).carrier) : pieceCoord G = ↑(chartAt (Fin n → 𝕜) x)

theorem Hironaka.Manifold.map_nhds_pieceCoord {𝕜 : Type} [RCLike 𝕜] {n : ℕ} (G : TopologicalSpace.Opens (Fin n → 𝕜)) (w : (pieceAmbient 𝕜 G).carrier) : Filter.map (pieceCoord G) (nhds w) = nhds (pieceCoord G w)

theorem Hironaka.Manifold.germMap_pieceCoord_injective {𝕜 : Type} [RCLike 𝕜] {n : ℕ} (G : TopologicalSpace.Opens (Fin n → 𝕜)) (q : (pieceAmbient 𝕜 G).carrier) : Function.Injective ⇑(Manifold.germMap (pieceCoord G) ⋯ q)

The germ map of the coordinate map is injective (the argument for a local analytic isomorphism, GermIso.lean, for the coordinate map of a one-piece ambient).

theorem Hironaka.Manifold.germMap_pieceCoord_surjective {𝕜 : Type} [RCLike 𝕜] {n : ℕ} (G : TopologicalSpace.Opens (Fin n → 𝕜)) (q : (pieceAmbient 𝕜 G).carrier) : Function.Surjective ⇑(Manifold.germMap (pieceCoord G) ⋯ q)

The germ map of the coordinate map is surjective: a representative near q composed with the inverse chart represents a germ at the coordinates of q.

noncomputable def Hironaka.Manifold.modelStalkEquiv {𝕜 : Type} [RCLike 𝕜] {n : ℕ} (G : TopologicalSpace.Opens (Fin n → 𝕜)) (q : (pieceAmbient 𝕜 G).carrier) : ↑((Manifold.structureSheaf 𝕜 (Fin n → 𝕜) (Fin n → 𝕜)).presheaf.stalk (pieceCoord G q)) ≃+* ↑((Manifold.structureSheaf 𝕜 (Fin n → 𝕜) (pieceAmbient 𝕜 G).carrier).presheaf.stalk q)

The stalk of a one-piece ambient at q is the stalk of the model space at its coordinates: the germ map of the coordinate map, as a ring isomorphism 𝒪_{𝕜ⁿ, z} ≃+* 𝒪_{Sp(G), ⟨(), z⟩}.

Equations

• Hironaka.Manifold.modelStalkEquiv G q = RingEquiv.ofBijective (Manifold.germMap (Hironaka.Manifold.pieceCoord G) ⋯ q) ⋯

theorem Hironaka.Manifold.modelStalkEquiv_apply {𝕜 : Type} [RCLike 𝕜] {n : ℕ} (G : TopologicalSpace.Opens (Fin n → 𝕜)) (q : (pieceAmbient 𝕜 G).carrier) (s : ↑((Manifold.structureSheaf 𝕜 (Fin n → 𝕜) (Fin n → 𝕜)).presheaf.stalk (pieceCoord G q))) : (modelStalkEquiv G q) s = (Manifold.germMap (pieceCoord G) ⋯ q) s

The coordinate germs and the germs of functions of the model space

theorem Hironaka.Manifold.germMapOn_const' {𝕜 : Type} [RCLike 𝕜] {E : Type u_1} {E' : Type u_2} [NormedAddCommGroup E] [NormedSpace 𝕜 E] [NormedAddCommGroup E'] [NormedSpace 𝕜 E'] {M : Type u} [TopologicalSpace M] [ChartedSpace E M] {N : Type v} [TopologicalSpace N] [ChartedSpace E' N] (φ : N → M) {V : TopologicalSpace.Opens N} (hφ : ContMDiffOn (modelWithCornersSelf 𝕜 E') (modelWithCornersSelf 𝕜 E) ⊤ φ ↑V) {b : N} (hb : b ∈ V) {c : M} (hc : φ b = c) (a : 𝕜) : (Manifold.germMapOn φ hφ hb hc) ((Manifold.const 𝕜 E M c) a) = (Manifold.const 𝕜 E' N b) a

The germ map of a partial analytic map carries the constants to the constants (germMap_const for maps between manifolds of different models and universes).

noncomputable def Hironaka.Manifold.modelCoordGerm {𝕜 : Type} [RCLike 𝕜] {n : ℕ} (v : Fin n → 𝕜) (k : Fin n) : ↑((Manifold.structureSheaf 𝕜 (Fin n → 𝕜) (Fin n → 𝕜)).presheaf.stalk v)

The coordinate germ u_k of the model space 𝕜ⁿ at v (coord for the identity chart).

Equations

• Hironaka.Manifold.modelCoordGerm v k = Manifold.coord (Fin n → 𝕜) (ContinuousLinearEquiv.refl 𝕜 (Fin n → 𝕜)) (chartAt (Fin n → 𝕜) v) ⋯ ⋯ k

theorem Hironaka.Manifold.stalkToGerm_modelCoordGerm {𝕜 : Type} [RCLike 𝕜] {n : ℕ} (v : Fin n → 𝕜) (k : Fin n) : (Manifold.stalkToGerm (modelWithCornersSelf 𝕜 (Fin n → 𝕜)) ⊤ (Fin n → 𝕜) v) (modelCoordGerm v k) = ↑fun (w : Fin n → 𝕜) => w k

theorem Hironaka.Manifold.coord_pieceAmbient_eq {𝕜 : Type} [RCLike 𝕜] {n : ℕ} {G : TopologicalSpace.Opens (Fin n → 𝕜)} (q : (pieceAmbient 𝕜 G).carrier) (k : Fin n) : Manifold.coord (Fin n → 𝕜) (ContinuousLinearEquiv.refl 𝕜 (Fin n → 𝕜)) (chartAt (Fin n → 𝕜) q) ⋯ ⋯ k = (Manifold.germMap (pieceCoord G) ⋯ q) (modelCoordGerm (pieceCoord G q) k)

The coordinate germ of a chart of a one-piece ambient is the model coordinate germ, transported along the coordinate map.

noncomputable def Hironaka.Manifold.pieceCoordSection {𝕜 : Type} [RCLike 𝕜] {n : ℕ} (G : TopologicalSpace.Opens (Fin n → 𝕜)) (k : Fin n) : ↑((Manifold.structureSheaf 𝕜 (Fin n → 𝕜) (pieceAmbient 𝕜 G).carrier).presheaf.obj (Opposite.op ⊤))

The k-th coordinate function of a one-piece ambient as a global section.

Equations

• Hironaka.Manifold.pieceCoordSection G k = Manifold.sectionOfContMDiffOn (fun (w : (Hironaka.Manifold.pieceAmbient 𝕜 G).carrier) => Hironaka.Manifold.pieceCoord G w k) ⊤ ⋯

theorem Hironaka.Manifold.germ_pieceCoordSection {𝕜 : Type} [RCLike 𝕜] {n : ℕ} {G : TopologicalSpace.Opens (Fin n → 𝕜)} (q : (pieceAmbient 𝕜 G).carrier) (k : Fin n) : (CategoryTheory.ConcreteCategory.hom ((Manifold.structureSheaf 𝕜 (Fin n → 𝕜) (pieceAmbient 𝕜 G).carrier).presheaf.germ ⊤ q ⋯)) (pieceCoordSection G k) = (Manifold.germMap (pieceCoord G) ⋯ q) (modelCoordGerm (pieceCoord G q) k)

noncomputable def Hironaka.Manifold.modelGerm {𝕜 : Type} [RCLike 𝕜] {n : ℕ} {O : TopologicalSpace.Opens (Fin n → 𝕜)} (f : (Fin n → 𝕜) → 𝕜) (hf : ContDiffOn 𝕜 ⊤ f ↑O) {v : Fin n → 𝕜} (hv : v ∈ O) : ↑((Manifold.structureSheaf 𝕜 (Fin n → 𝕜) (Fin n → 𝕜)).presheaf.stalk v)

The germ at v ∈ O of a function analytic on the open O ⊆ 𝕜ⁿ.

Equations

• Hironaka.Manifold.modelGerm f hf hv = (CategoryTheory.ConcreteCategory.hom ((Manifold.structureSheaf 𝕜 (Fin n → 𝕜) (Fin n → 𝕜)).presheaf.germ O v hv)) (Manifold.sectionOfContMDiffOn f O ⋯)

theorem Hironaka.Manifold.stalkToGerm_modelGerm {𝕜 : Type} [RCLike 𝕜] {n : ℕ} {O : TopologicalSpace.Opens (Fin n → 𝕜)} (f : (Fin n → 𝕜) → 𝕜) (hf : ContDiffOn 𝕜 ⊤ f ↑O) {v : Fin n → 𝕜} (hv : v ∈ O) : (Manifold.stalkToGerm (modelWithCornersSelf 𝕜 (Fin n → 𝕜)) ⊤ (Fin n → 𝕜) v) (modelGerm f hf hv) = ↑f

theorem Hironaka.Manifold.eval_modelGerm {𝕜 : Type} [RCLike 𝕜] {n : ℕ} {O : TopologicalSpace.Opens (Fin n → 𝕜)} (f : (Fin n → 𝕜) → 𝕜) (hf : ContDiffOn 𝕜 ⊤ f ↑O) {v : Fin n → 𝕜} (hv : v ∈ O) : (Manifold.eval 𝕜 (Fin n → 𝕜) (Fin n → 𝕜) v) (modelGerm f hf hv) = f v

theorem Hironaka.Manifold.eval_modelCoordGerm {𝕜 : Type} [RCLike 𝕜] {n : ℕ} (v : Fin n → 𝕜) (k : Fin n) : (Manifold.eval 𝕜 (Fin n → 𝕜) (Fin n → 𝕜) v) (modelCoordGerm v k) = v k

theorem Hironaka.Manifold.modelGerm_sub_const_mem {𝕜 : Type} [RCLike 𝕜] {n : ℕ} {O : TopologicalSpace.Opens (Fin n → 𝕜)} (f : (Fin n → 𝕜) → 𝕜) (hf : ContDiffOn 𝕜 ⊤ f ↑O) {v : Fin n → 𝕜} (hv : v ∈ O) : modelGerm f hf hv - (Manifold.const 𝕜 (Fin n → 𝕜) (Fin n → 𝕜) v) (f v) ∈ IsLocalRing.maximalIdeal ↑((Manifold.structureSheaf 𝕜 (Fin n → 𝕜) (Fin n → 𝕜)).presheaf.stalk v)

The model germ of f at v is congruent to the constant f v modulo the maximal ideal.

theorem Hironaka.Manifold.modelCoordGerm_sub_const_mem {𝕜 : Type} [RCLike 𝕜] {n : ℕ} (v : Fin n → 𝕜) (k : Fin n) : modelCoordGerm v k - (Manifold.const 𝕜 (Fin n → 𝕜) (Fin n → 𝕜) v) (v k) ∈ IsLocalRing.maximalIdeal ↑((Manifold.structureSheaf 𝕜 (Fin n → 𝕜) (Fin n → 𝕜)).presheaf.stalk v)

theorem Hironaka.Manifold.germMapOn_modelCoordGerm {𝕜 : Type} [RCLike 𝕜] {n m : ℕ} {j : (Fin n → 𝕜) → Fin m → 𝕜} {O : TopologicalSpace.Opens (Fin n → 𝕜)} (hj : ContDiffOn 𝕜 ⊤ j ↑O) {v : Fin n → 𝕜} (hv : v ∈ O) {w : Fin m → 𝕜} (hjv : j v = w) (k : Fin m) : (Manifold.germMapOn j ⋯ hv hjv) (modelCoordGerm w k) = modelGerm (fun (v : Fin n → 𝕜) => j v k) ⋯ hv

The germ map of a partial analytic map j carries the coordinate germ u_k to the germ of the component j_k.

theorem Hironaka.Manifold.modelStalkEquiv_const {𝕜 : Type} [RCLike 𝕜] {n : ℕ} {G : TopologicalSpace.Opens (Fin n → 𝕜)} (q : (pieceAmbient 𝕜 G).carrier) (c : 𝕜) : (modelStalkEquiv G q) ((Manifold.const 𝕜 (Fin n → 𝕜) (Fin n → 𝕜) (pieceCoord G q)) c) = (Manifold.const 𝕜 (Fin n → 𝕜) (pieceAmbient 𝕜 G).carrier q) c

The stalk isomorphism of a one-piece ambient carries the constants to the constants.

theorem Hironaka.Manifold.modelStalkEquiv_symm_const {𝕜 : Type} [RCLike 𝕜] {n : ℕ} {G : TopologicalSpace.Opens (Fin n → 𝕜)} (q : (pieceAmbient 𝕜 G).carrier) (c : 𝕜) : (modelStalkEquiv G q).symm ((Manifold.const 𝕜 (Fin n → 𝕜) (pieceAmbient 𝕜 G).carrier q) c) = (Manifold.const 𝕜 (Fin n → 𝕜) (Fin n → 𝕜) (pieceCoord G q)) c

The model stalk map of a piece embedding

@[reducible, inline]

noncomputable abbrev Hironaka.Manifold.PieceEmbedding.modelPoint {𝕜 : Type} [RCLike 𝕜] {n : ℕ} {X : AnalyticSpace 𝕜} {V : Set ↑↑X.toPresheafedSpace} (E : PieceEmbedding 𝕜 n X V) (y : ↑↑(X.restrictSet V).toPresheafedSpace) : Fin n → 𝕜

The coordinates i(y) ∈ 𝕜ⁿ of the ambient point of y.

Equations

• E.modelPoint y = Hironaka.Manifold.pieceCoord E.G (E.ambientPoint y)

theorem Hironaka.Manifold.PieceEmbedding.modelPoint_mem {𝕜 : Type} [RCLike 𝕜] {n : ℕ} {X : AnalyticSpace 𝕜} {V : Set ↑↑X.toPresheafedSpace} (E : PieceEmbedding 𝕜 n X V) (y : ↑↑(X.restrictSet V).toPresheafedSpace) : E.modelPoint y ∈ E.G

instance Hironaka.Manifold.PieceEmbedding.isLocalHom_pieceStalkMap {𝕜 : Type} [RCLike 𝕜] {n : ℕ} {X : AnalyticSpace 𝕜} {V : Set ↑↑X.toPresheafedSpace} (E : PieceEmbedding 𝕜 n X V) (y : ↑↑(X.restrictSet V).toPresheafedSpace) : IsLocalHom (E.pieceStalkMap y)

theorem Hironaka.Manifold.PieceEmbedding.pieceStalkMap_const {𝕜 : Type} [RCLike 𝕜] {n : ℕ} {X : AnalyticSpace 𝕜} {V : Set ↑↑X.toPresheafedSpace} (E : PieceEmbedding 𝕜 n X V) (y : ↑↑(X.restrictSet V).toPresheafedSpace) (c : 𝕜) : (E.pieceStalkMap y) ((Manifold.const 𝕜 (Fin n → 𝕜) (pieceAmbient 𝕜 E.G).carrier (E.ambientPoint y)) c) = ((X.restrictSet V).constAt y) c

The stalk map of a piece embedding carries the constants to the constants.

noncomputable def Hironaka.Manifold.PieceEmbedding.modelStalkMap {𝕜 : Type} [RCLike 𝕜] {n : ℕ} {X : AnalyticSpace 𝕜} {V : Set ↑↑X.toPresheafedSpace} (E : PieceEmbedding 𝕜 n X V) (y : ↑↑(X.restrictSet V).toPresheafedSpace) : ↑((Manifold.structureSheaf 𝕜 (Fin n → 𝕜) (Fin n → 𝕜)).presheaf.stalk (E.modelPoint y)) →+* ↑((X.restrictSet V).presheaf.stalk y)

The model stalk map ε_y : 𝒪_{𝕜ⁿ, i(y)} →+* 𝒪_{X|V, y} of a piece embedding at y: the stalk map of the piece after the coordinate germ map (the description of a morphism by its coordinate functions, Hironaka's local K-coordinations [Hir64, Ch. 0, §1, p. 120]).

Equations

• E.modelStalkMap y = (E.pieceStalkMap y).comp (Manifold.germMap (Hironaka.Manifold.pieceCoord E.G) ⋯ (E.ambientPoint y))

theorem Hironaka.Manifold.PieceEmbedding.modelStalkMap_apply {𝕜 : Type} [RCLike 𝕜] {n : ℕ} {X : AnalyticSpace 𝕜} {V : Set ↑↑X.toPresheafedSpace} (E : PieceEmbedding 𝕜 n X V) (y : ↑↑(X.restrictSet V).toPresheafedSpace) (s : ↑((Manifold.structureSheaf 𝕜 (Fin n → 𝕜) (Fin n → 𝕜)).presheaf.stalk (E.modelPoint y))) : (E.modelStalkMap y) s = (E.pieceStalkMap y) ((Manifold.germMap (pieceCoord E.G) ⋯ (E.ambientPoint y)) s)

theorem Hironaka.Manifold.PieceEmbedding.modelStalkMap_modelStalkEquiv {𝕜 : Type} [RCLike 𝕜] {n : ℕ} {X : AnalyticSpace 𝕜} {V : Set ↑↑X.toPresheafedSpace} (E : PieceEmbedding 𝕜 n X V) (y : ↑↑(X.restrictSet V).toPresheafedSpace) (s : ↑((Manifold.structureSheaf 𝕜 (Fin n → 𝕜) (Fin n → 𝕜)).presheaf.stalk (E.modelPoint y))) : (E.pieceStalkMap y) ((modelStalkEquiv E.G (E.ambientPoint y)) s) = (E.modelStalkMap y) s

theorem Hironaka.Manifold.PieceEmbedding.modelStalkMap_modelStalkEquiv_symm {𝕜 : Type} [RCLike 𝕜] {n : ℕ} {X : AnalyticSpace 𝕜} {V : Set ↑↑X.toPresheafedSpace} (E : PieceEmbedding 𝕜 n X V) (y : ↑↑(X.restrictSet V).toPresheafedSpace) (s : ↑((Manifold.structureSheaf 𝕜 (Fin n → 𝕜) (pieceAmbient 𝕜 E.G).carrier).presheaf.stalk (E.ambientPoint y))) : (E.modelStalkMap y) ((modelStalkEquiv E.G (E.ambientPoint y)).symm s) = (E.pieceStalkMap y) s

instance Hironaka.Manifold.PieceEmbedding.isLocalHom_modelStalkMap {𝕜 : Type} [RCLike 𝕜] {n : ℕ} {X : AnalyticSpace 𝕜} {V : Set ↑↑X.toPresheafedSpace} (E : PieceEmbedding 𝕜 n X V) (y : ↑↑(X.restrictSet V).toPresheafedSpace) : IsLocalHom (E.modelStalkMap y)

theorem Hironaka.Manifold.PieceEmbedding.modelStalkMap_const {𝕜 : Type} [RCLike 𝕜] {n : ℕ} {X : AnalyticSpace 𝕜} {V : Set ↑↑X.toPresheafedSpace} (E : PieceEmbedding 𝕜 n X V) (y : ↑↑(X.restrictSet V).toPresheafedSpace) (c : 𝕜) : (E.modelStalkMap y) ((Manifold.const 𝕜 (Fin n → 𝕜) (Fin n → 𝕜) (E.modelPoint y)) c) = ((X.restrictSet V).constAt y) c

The model stalk map carries the constants to the constants.

The local lifts

theorem Hironaka.Manifold.PieceEmbedding.sub_constAt_mem_of_isLocalHom {𝕜 : Type} [RCLike 𝕜] {E' : Type u_1} [NormedAddCommGroup E'] [NormedSpace 𝕜 E'] {M : Type v} [TopologicalSpace M] [ChartedSpace E' M] {a : M} {Z : AnalyticSpace.KLocallyRingedSpace 𝕜} {z : ↑↑Z.toPresheafedSpace} (θ : ↑((Manifold.structureSheaf 𝕜 E' M).presheaf.stalk a) →+* ↑(Z.presheaf.stalk z)) [IsLocalHom θ] (hθ : ∀ (c : 𝕜), θ ((Manifold.const 𝕜 E' M a) c) = (Z.constAt z) c) {s : ↑((Manifold.structureSheaf 𝕜 E' M).presheaf.stalk a)} {c : 𝕜} (hs : s - (Manifold.const 𝕜 E' M a) c ∈ IsLocalRing.maximalIdeal ↑((Manifold.structureSheaf 𝕜 E' M).presheaf.stalk a)) : θ s - (Z.constAt z) c ∈ IsLocalRing.maximalIdeal ↑(Z.presheaf.stalk z)

A local homomorphism carrying the constants to the constants carries a germ congruent to the constant c to a germ congruent to the constant c (the maximal ideal goes into the maximal ideal).

theorem Hironaka.Manifold.PieceEmbedding.modelPoint_eq_of_coord_eq {𝕜 : Type} [RCLike 𝕜] {n : ℕ} {X : AnalyticSpace 𝕜} {V : Set ↑↑X.toPresheafedSpace} (E : PieceEmbedding 𝕜 n X V) {m : ℕ} (F : PieceEmbedding 𝕜 m X V) (y : ↑↑(X.restrictSet V).toPresheafedSpace) {O : TopologicalSpace.Opens (Fin n → 𝕜)} {f : (Fin n → 𝕜) → 𝕜} (hf : ContDiffOn 𝕜 ⊤ f ↑O) (hy : E.modelPoint y ∈ O) (k : Fin m) (h : (F.modelStalkMap y) (modelCoordGerm (F.modelPoint y) k) = (E.modelStalkMap y) (modelGerm f hf hy)) : F.modelPoint y k = f (E.modelPoint y)

Residues of a lift: if the k-th coordinate of F at y is the germ of f pulled back through E, then i_F(y)_k = f (i_E(y)) (a germ congruent to two constants modulo the maximal ideal has equal constants).

theorem Hironaka.Manifold.PieceEmbedding.modelStalkMap_eq_of_lift {𝕜 : Type} [RCLike 𝕜] {n : ℕ} {X : AnalyticSpace 𝕜} {V : Set ↑↑X.toPresheafedSpace} (E : PieceEmbedding 𝕜 n X V) {m : ℕ} (F : PieceEmbedding 𝕜 m X V) (y : ↑↑(X.restrictSet V).toPresheafedSpace) {O : TopologicalSpace.Opens (Fin n → 𝕜)} {j : (Fin n → 𝕜) → Fin m → 𝕜} (hj : ContDiffOn 𝕜 ⊤ j ↑O) (hy : E.modelPoint y ∈ O) (hjy : j (E.modelPoint y) = F.modelPoint y) (hcoord : ∀ (k : Fin m), (F.modelStalkMap y) (modelCoordGerm (F.modelPoint y) k) = (E.modelStalkMap y) (modelGerm (fun (v : Fin n → 𝕜) => j v k) ⋯ hy)) (s : ↑((Manifold.structureSheaf 𝕜 (Fin m → 𝕜) (Fin m → 𝕜)).presheaf.stalk (F.modelPoint y))) : (F.modelStalkMap y) s = (E.modelStalkMap y) ((Manifold.germMapOn j ⋯ hy hjy) s)

The stalk maps of a lift agree everywhere (ringHom_ext_of_coord', the stalks of X|V being Noetherian): if the coordinates of F at y are the components of j pulled back through E, and j carries i_E(y) to i_F(y), then ε_F y = ε_E y ∘ j^* on every germ.

theorem Hironaka.Manifold.PieceEmbedding.exists_modelLift {𝕜 : Type} [RCLike 𝕜] {n : ℕ} {X : AnalyticSpace 𝕜} {V : Set ↑↑X.toPresheafedSpace} (E : PieceEmbedding 𝕜 n X V) {m : ℕ} (F : PieceEmbedding 𝕜 m X V) (x : ↑↑(X.restrictSet V).toPresheafedSpace) : ∃ (O : TopologicalSpace.Opens (Fin n → 𝕜)) (_ : E.modelPoint x ∈ O) (j : (Fin n → 𝕜) → Fin m → 𝕜) (hj : ContDiffOn 𝕜 ⊤ j ↑O), ∀ (y : ↑↑(X.restrictSet V).toPresheafedSpace) (hy : E.modelPoint y ∈ O) (k : Fin m), (F.modelStalkMap y) (modelCoordGerm (F.modelPoint y) k) = (E.modelStalkMap y) (modelGerm (fun (v : Fin n → 𝕜) => j v k) ⋯ hy)

The local lift (the extension j of one embedding's coordinates to the other ambient in [Kol07, Lemma 39, proof]): for two embeddings E : X|V ↪ 𝕜ⁿ, F : X|V ↪ 𝕜ᵐ of one piece and a point x, there is an open O ∋ i_E(x) of 𝕜ⁿ and a map j : 𝕜ⁿ → 𝕜ᵐ analytic on O whose components, pulled back through E, are the coordinates of F at every y over O — the local description of the sections of Sp(G)/𝓘 (exists_local_rep) applied to the coordinate functions of Sp(G') pulled back along E⁻¹ ∘ F, and read in the chart of Sp(G).