The restriction of germs to a closed submanifold

The inclusion Y → M of a closed submanifold is analytic for the induced charts (contMDiff_val: in an induced chart it is φ⁻¹ ∘ ψ⁻¹ ∘ embedCompl), so the restriction of an analytic function on M to Y is analytic, and the germs of sections of 𝒪_M at a ∈ Y restrict to germs of sections of 𝒪_Y: through the embeddings of the stalks into the rings of germs of functions (stalkToGerm), the restriction 𝒪_{M,a} →+* 𝒪_{Y,a} is the composition with the inclusion (germRestrict) read back in 𝒪_{Y,a} (restrictStalk). It satisfies the specification IsRestrictStalk of Hironaka/Manifold/Submanifold.lean (isRestrictStalk_restrictStalk) and is the unique map doing so (IsRestrictStalk.eq). The local ring 𝒪_{Y,a} of Hironaka's non-singular subspace D is thereby a quotient of 𝒪_{M,a} [Hir64, Definition 2, p. 141]; its kernel is computed in Hironaka/Manifold/Submanifold/Ideal.lean.

theorem Manifold.IsClosedSubmanifold.contMDiff_val {𝕜 : 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) : ContMDiff (modelWithCornersSelf 𝕜 (Fin (n - c) → 𝕜)) (modelWithCornersSelf 𝕜 E) ⊤ Subtype.val

The inclusion of a closed submanifold is analytic for the induced charts.

def Manifold.germRestrict {𝕜 : Type} [RCLike 𝕜] {M : Type u} [TopologicalSpace M] (Y : Set M) (a : ↑Y) : (nhds ↑a).Germ 𝕜 →+* (nhds a).Germ 𝕜

The restriction of germs of functions along the inclusion Y → M.

Equations

• Manifold.germRestrict Y a = Manifold.germCompRingHom Subtype.val ⋯

theorem Manifold.germRestrict_coe {𝕜 : Type} [RCLike 𝕜] {M : Type u} [TopologicalSpace M] (Y : Set M) (a : ↑Y) (f : M → 𝕜) : (germRestrict Y a) ↑f = ↑(f ∘ Subtype.val)

germRestrict sends the germ of f at a to the germ of f ∘ Subtype.val (unfolding lemma).

theorem Manifold.IsClosedSubmanifold.germRestrict_mem_range {𝕜 : 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) (s : ↑((structureSheaf 𝕜 E M).presheaf.stalk ↑a)) : (germRestrict Y a) ((stalkToGerm (modelWithCornersSelf 𝕜 E) ⊤ M ↑a) s) ∈ Set.range ⇑(stalkToGerm (modelWithCornersSelf 𝕜 (Fin (n - c) → 𝕜)) ⊤ (↑Y) a)

The restriction to Y of the germ of a section of 𝒪_M is the germ of a section of 𝒪_Y.

noncomputable def Manifold.IsClosedSubmanifold.stalkEquivRange {𝕜 : 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) : hY.stalk a ≃+* ↥(stalkToGerm (modelWithCornersSelf 𝕜 (Fin (n - c) → 𝕜)) ⊤ (↑Y) a).range

𝒪_{Y,a} is isomorphic to the ring of germs of analytic functions on Y at a, the range of stalkToGerm.

Equations

• hY.stalkEquivRange a = RingEquiv.ofBijective (Manifold.stalkToGerm (modelWithCornersSelf 𝕜 (Fin (n - c) → 𝕜)) ⊤ (↑Y) a).rangeRestrict ⋯

noncomputable def Manifold.IsClosedSubmanifold.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) : ↑((structureSheaf 𝕜 E M).presheaf.stalk ↑a) →+* hY.stalk a

The restriction of germs 𝒪_{M,a} →+* 𝒪_{Y,a}.

Equations

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

theorem Manifold.IsClosedSubmanifold.stalkToGerm_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) (s : ↑((structureSheaf 𝕜 E M).presheaf.stalk ↑a)) : (stalkToGerm (modelWithCornersSelf 𝕜 (Fin (n - c) → 𝕜)) ⊤ (↑Y) a) ((hY.restrictStalk a) s) = (germRestrict Y a) ((stalkToGerm (modelWithCornersSelf 𝕜 E) ⊤ M ↑a) s)

The restriction of germs read through stalkToGerm: the germ on Y of restrictStalk s is the restriction (germRestrict) of the germ of s.

theorem Manifold.IsClosedSubmanifold.isRestrictStalk_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) : hY.IsRestrictStalk a (hY.restrictStalk a)

restrictStalk satisfies the specification IsRestrictStalk.

theorem Manifold.IsClosedSubmanifold.IsRestrictStalk.eq {𝕜 : 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 r' : ↑((structureSheaf 𝕜 E M).presheaf.stalk ↑a) →+* hY.stalk a} (hr : hY.IsRestrictStalk a r) (hr' : hY.IsRestrictStalk a r') : r = r'

The restriction of germs is determined by its specification.