The ideal of a closed submanifold in a stalk

The restriction of germs 𝒪_{M,a} →+* 𝒪_{Y,a} (Hironaka/Manifold/Submanifold/Restrict.lean) is onto — an analytic function on Y near a extends to M along the complementary coordinates of an adapted chart (restrictStalk_surjective) — and its kernel, the ideal 𝓘_{Y,a} of germs vanishing on Y, is generated by the adapted coordinates x_{σ i} − x_{σ i}(a) (ker_restrictStalk): a germ vanishing on Y is, in the adapted chart, an analytic function vanishing on the coordinate subspace {z_σ = 0}, hence a combination ∑ z_{σ i} · G_i with analytic G_i (exists_sum_coord_mul_of_vanish_on_subspace of Hironaka/Analytic/Germ/CoordDiv.lean), read back on M through the chart. Consequently 𝒪_{M,a} / 𝓘_{Y,a} ≅ 𝒪_{Y,a} (IsRestrictStalk.exists_quotient_equiv'). This is Hironaka's "the ideal of D in 𝒪_{X,x} is generated by some of the z_i" of a regular system of parameters [Hir64, Definition 2, p. 141], and Bierstone–Milman's smooth subspace as a coordinate subspace [BM97, (3.8)(2)]; it is the description of the ideal sheaf of a centre used throughout the blow-up constructions (Hironaka/Manifold/BlowUp/Divisor.lean).

theorem Manifold.IsClosedSubmanifold.restrictStalk_surjective {𝕜 : Type} [RCLike 𝕜] {E : Type u_1} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {M : Type u} [TopologicalSpace M] [ChartedSpace E M] {n : ℕ} {ψ : E ≃L[𝕜] Fin n → 𝕜} {Y : Set M} {c : ℕ} (hY : IsClosedSubmanifold ψ Y c) (a : ↑Y) : Function.Surjective ⇑(hY.restrictStalk a)

The restriction of germs is onto: an analytic function on Y near a extends along the complementary coordinates of an adapted chart.

theorem Manifold.stalkToGerm_coord {𝕜 : Type} [RCLike 𝕜] {E : Type u_1} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {M : Type u} [TopologicalSpace M] [ChartedSpace E M] {n : ℕ} {ψ : E ≃L[𝕜] Fin n → 𝕜} {φ : OpenPartialHomeomorph M E} (hφ : φ ∈ IsManifold.maximalAtlas (modelWithCornersSelf 𝕜 E) ⊤ M) {a : M} (ha : a ∈ φ.source) (j : Fin n) : (stalkToGerm (modelWithCornersSelf 𝕜 E) ⊤ M a) (coord E ψ φ hφ ha j) = ↑(extendSection 𝕜 E (chartSection E ψ φ hφ j))

The germ of functions of a coordinate germ coord.

theorem Manifold.stalkToGerm_const {𝕜 : Type} [RCLike 𝕜] {E : Type u_1} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {M : Type u} [TopologicalSpace M] [ChartedSpace E M] (a : M) (r : 𝕜) : (stalkToGerm (modelWithCornersSelf 𝕜 E) ⊤ M a) ((const 𝕜 E M a) r) = ↑fun (x : M) => r

The germ of functions of a constant germ.

theorem Manifold.IsClosedSubmanifold.restrictStalk_coord_sub {𝕜 : Type} [RCLike 𝕜] {E : Type u_1} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {M : Type u} [TopologicalSpace M] [ChartedSpace E M] {n : ℕ} {ψ : E ≃L[𝕜] Fin n → 𝕜} {Y : Set M} {c : ℕ} (hY : IsClosedSubmanifold ψ Y c) (a : ↑Y) {φ : OpenPartialHomeomorph M E} {σ : Fin c ↪ Fin n} (h : IsAdaptedChart ψ Y φ σ) (ha : ↑a ∈ φ.source) (i : Fin c) : (hY.restrictStalk a) (coord E ψ φ ⋯ ha (σ i) - (const 𝕜 E M ↑a) ((eval 𝕜 E M ↑a) (coord E ψ φ ⋯ ha (σ i)))) = 0

The adapted coordinates x_{σ i} − x_{σ i}(a) restrict to zero on Y.

theorem Manifold.IsClosedSubmanifold.ker_restrictStalk {𝕜 : Type} [RCLike 𝕜] {E : Type u_1} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {M : Type u} [TopologicalSpace M] [ChartedSpace E M] {n : ℕ} {ψ : E ≃L[𝕜] Fin n → 𝕜} {Y : Set M} {c : ℕ} (hY : IsClosedSubmanifold ψ Y c) (a : ↑Y) {φ : OpenPartialHomeomorph M E} {σ : Fin c ↪ Fin n} (h : IsAdaptedChart ψ Y φ σ) (ha : ↑a ∈ φ.source) : RingHom.ker (hY.restrictStalk a) = Ideal.span (Set.range fun (i : Fin c) => coord E ψ φ ⋯ ha (σ i) - (const 𝕜 E M ↑a) ((eval 𝕜 E M ↑a) (coord E ψ φ ⋯ ha (σ i))))

The ideal of germs vanishing on Y is generated by the adapted coordinates x_{σ i} − x_{σ i}(a) [Hir64, Definition 2, p. 141].

For any map satisfying the specification

theorem Manifold.IsClosedSubmanifold.IsRestrictStalk.surjective' {𝕜 : Type} [RCLike 𝕜] {E : Type u_1} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {M : Type u} [TopologicalSpace M] [ChartedSpace E M] {n : ℕ} {ψ : E ≃L[𝕜] Fin n → 𝕜} {Y : Set M} {c : ℕ} (hY : IsClosedSubmanifold ψ Y c) {a : ↑Y} {r : ↑((structureSheaf 𝕜 E M).presheaf.stalk ↑a) →+* hY.stalk a} (hr : hY.IsRestrictStalk a r) : Function.Surjective ⇑r

The restriction of germs is onto.

theorem Manifold.IsClosedSubmanifold.IsRestrictStalk.ker_eq_span' {𝕜 : Type} [RCLike 𝕜] {E : Type u_1} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {M : Type u} [TopologicalSpace M] [ChartedSpace E M] {n : ℕ} {ψ : E ≃L[𝕜] Fin n → 𝕜} {Y : Set M} {c : ℕ} (hY : IsClosedSubmanifold ψ Y c) {a : ↑Y} {r : ↑((structureSheaf 𝕜 E M).presheaf.stalk ↑a) →+* hY.stalk a} (hr : hY.IsRestrictStalk a r) {φ : OpenPartialHomeomorph M E} {σ : Fin c ↪ Fin n} (h : IsAdaptedChart ψ Y φ σ) (ha : ↑a ∈ φ.source) : RingHom.ker r = Ideal.span (Set.range fun (i : Fin c) => coord E ψ φ ⋯ ha (σ i) - (const 𝕜 E M ↑a) ((eval 𝕜 E M ↑a) (coord E ψ φ ⋯ ha (σ i))))

The kernel of the restriction of germs is generated by the adapted coordinates.

theorem Manifold.IsClosedSubmanifold.IsRestrictStalk.exists_quotient_equiv' {𝕜 : Type} [RCLike 𝕜] {E : Type u_1} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {M : Type u} [TopologicalSpace M] [ChartedSpace E M] {n : ℕ} {ψ : E ≃L[𝕜] Fin n → 𝕜} {Y : Set M} {c : ℕ} (hY : IsClosedSubmanifold ψ Y c) {a : ↑Y} {r : ↑((structureSheaf 𝕜 E M).presheaf.stalk ↑a) →+* hY.stalk a} (hr : hY.IsRestrictStalk a r) : ∃ (e : ↑((structureSheaf 𝕜 E M).presheaf.stalk ↑a) ⧸ RingHom.ker r ≃+* hY.stalk a), ∀ (s : ↑((structureSheaf 𝕜 E M).presheaf.stalk ↑a)), e ((Ideal.Quotient.mk (RingHom.ker r)) s) = r s

𝒪_{M,a} / 𝓘_{Y,a} ≅ 𝒪_{Y,a}.