Restriction of germs to a closed submanifold: the tools

Three facts used in the analytic form of Kollár's Lemma 62 (birationalTransform_pullback_restrictMap in LemmaSixtyTwo.lean), the compatibility of the marked transform with restriction to a hypersurface containing the centre [Kol07, Lemma 62]:

• the germ map of the inclusion S ↪ M of a bundled closed submanifold (inclusionMap, germMap) is the restriction of germs restrictStalk (germMap_inclusionMap_eq_restrictStalk), surjective with kernel the ideal of S;
• the ideal sheaf of Y ⊆ S as a closed submanifold of the bundled S is the restriction of the ideal sheaf I_Y (idealSheaf_preimageVal_eq_pullback): a germ on S vanishes on Y near a point iff some (equivalently any) extension to M vanishes on Y there — Y is contained in S;
• the colon by a power of an element commutes with a ring map into a domain, on ideals divisible by that power (Ideal.map_colon_singleton_pow_eq) — the algebra behind Kollár's remark that it does not matter whether one first sets x_1 = 0 and computes the transform or first computes the transform and then sets y_1 = 0 [Kol07, Lemma 62, proof]; and a coordinate of a chart lies outside the ideal spanned by the other (centred) coordinates (coord_notMem_span_coord_sub_const), which is why the exceptional coordinate does not vanish identically on the strict transform in a good chart.

Not in the sources; routine.

theorem Ideal.map_colon_singleton_pow_eq {R : Type u_1} {R' : Type u_2} [CommRing R] [CommRing R'] [IsDomain R'] (f : R →+* R') {A : Ideal R} {u : R} {m : ℕ} (hA : A ≤ span {u ^ m}) (hu : f u ≠ 0) : Submodule.colon (map f A) {f u ^ m} = map f (Submodule.colon A {u ^ m})

The colon by f u ^ m of the image of an ideal A ⊆ (u ^ m) under a ring map f into a domain, with f u ≠ 0, is the image of the colon (A : u ^ m): A = (u ^ m) · (A : u ^ m) (span_pow_mul_colon_of_le) and (f u) ^ m cancels in the domain (colon_span_pow_mul_self).

theorem Manifold.coord_notMem_span_coord_sub_const {𝕜 : Type} [RCLike 𝕜] {E : Type u_1} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {n : ℕ} {M : Type u} [TopologicalSpace M] [ChartedSpace E M] (ψ : E ≃L[𝕜] Fin n → 𝕜) {Φ : OpenPartialHomeomorph M E} (hΦ : Φ ∈ IsManifold.maximalAtlas (modelWithCornersSelf 𝕜 E) ⊤ M) {a : M} (ha : a ∈ Φ.source) {ι : Type u_2} [Finite ι] (v : ι → Fin n) {k : Fin n} (hv : ∀ (j : ι), v j ≠ k) : coord E ψ Φ hΦ ha k ∉ Ideal.span (Set.range fun (j : ι) => coord E ψ Φ hΦ ha (v j) - (const 𝕜 E M a) ((eval 𝕜 E M a) (coord E ψ Φ hΦ ha (v j))))

A coordinate germ of a chart lies outside the ideal spanned by centred coordinate germs of other indices: applying the partial derivative ∂_k to a relation x_k = ∑ c_j (x_{v j} − x_{v j}(a)) gives 1 ∈ (x_{v j} − x_{v j}(a))_j ⊆ 𝔪_a.

theorem Manifold.IsClosedSubmanifold.germMap_inclusionMap_eq_restrictStalk {𝕜 : Type} [RCLike 𝕜] {E : Type u_1} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {n : ℕ} {ψ : E ≃L[𝕜] Fin n → 𝕜} {M : Type u} [TopologicalSpace M] [ChartedSpace E M] [T2Space M] [SecondCountableTopology M] {S : Set M} {s : ℕ} (hS : IsClosedSubmanifold ψ S s) (p : hS.toAnalyticManifold.carrier) (t : ↑((structureSheaf 𝕜 E M).presheaf.stalk (hS.inclusionMap p))) : (germMap ⇑hS.inclusionMap ⋯ p) t = (hS.restrictStalk p) t

The germ map of the inclusion of a bundled closed submanifold is the restriction of germs restrictStalk.

theorem Manifold.IsClosedSubmanifold.germMap_inclusionMap {𝕜 : Type} [RCLike 𝕜] {E : Type u_1} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {n : ℕ} {ψ : E ≃L[𝕜] Fin n → 𝕜} {M : Type u} [TopologicalSpace M] [ChartedSpace E M] [T2Space M] [SecondCountableTopology M] {S : Set M} {s : ℕ} (hS : IsClosedSubmanifold ψ S s) (p : hS.toAnalyticManifold.carrier) : germMap ⇑hS.inclusionMap ⋯ p = hS.restrictStalk p

The germ map of the inclusion, as a ring map, is restrictStalk.

theorem Manifold.IsClosedSubmanifold.eventually_preimageVal_iff {𝕜 : Type} [RCLike 𝕜] {E : Type u_1} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {n : ℕ} {ψ : E ≃L[𝕜] Fin n → 𝕜} {M : Type u} [TopologicalSpace M] [ChartedSpace E M] [T2Space M] [SecondCountableTopology M] {S Y : Set M} {s : ℕ} (hS : IsClosedSubmanifold ψ S s) (hYS : Y ⊆ S) {p : hS.toAnalyticManifold.carrier} (hp : p ∈ hS.preimageVal Y) (P : M → Prop) : (∀ᶠ (q : ↑(hS.preimageVal Y)) in nhds ⟨p, hp⟩, P (hS.inclusionMap ↑q)) ↔ ∀ᶠ (y : ↑Y) in nhds ⟨hS.inclusionMap p, hp⟩, P ↑y

Neighbourhood filters of Y ⊆ S read inside the bundled S and of Y in M correspond: a property of the ambient points holds eventually in one iff it holds eventually in the other (the maps ⟨⟨y, _⟩, _⟩ ↦ ⟨y, _⟩ and its inverse are continuous).

theorem Manifold.IsClosedSubmanifold.germMap_mem_idealSheaf_preimageVal_iff {𝕜 : Type} [RCLike 𝕜] {E : Type u_1} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {n : ℕ} {ψ : E ≃L[𝕜] Fin n → 𝕜} {M : Type u} [TopologicalSpace M] [ChartedSpace E M] [IsManifold (modelWithCornersSelf 𝕜 E) ⊤ M] [T2Space M] [SecondCountableTopology M] {S Y : Set M} {s c : ℕ} (hS : IsClosedSubmanifold ψ S s) (hY : IsClosedSubmanifold ψ Y c) (hYS : Y ⊆ S) {p : hS.toAnalyticManifold.carrier} (hp : p ∈ hS.preimageVal Y) (t : ↑((structureSheaf 𝕜 E M).presheaf.stalk (hS.inclusionMap p))) : (germMap ⇑hS.inclusionMap ⋯ p) t ∈ ⋯.idealSheaf.stalkIdeal p ↔ t ∈ hY.idealSheaf.stalkIdeal (hS.inclusionMap p)

A germ on M at a point of Y ⊆ S restricts (along the inclusion's germ map) to a germ on S vanishing on Y iff it vanishes on Y.

theorem Manifold.IsClosedSubmanifold.germMap_inclusionMap_surjective {𝕜 : Type} [RCLike 𝕜] {E : Type u_1} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {n : ℕ} {ψ : E ≃L[𝕜] Fin n → 𝕜} {M : Type u} [TopologicalSpace M] [ChartedSpace E M] [T2Space M] [SecondCountableTopology M] {S : Set M} {s : ℕ} (hS : IsClosedSubmanifold ψ S s) (p : hS.toAnalyticManifold.carrier) : Function.Surjective ⇑(germMap ⇑hS.inclusionMap ⋯ p)

The germ map of the inclusion is surjective (restrictStalk_surjective).

theorem Manifold.idealSheaf_preimageVal_eq_pullback {𝕜 : Type} [RCLike 𝕜] {E : Type u_1} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {n : ℕ} {ψ : E ≃L[𝕜] Fin n → 𝕜} {M : Type u} [TopologicalSpace M] [ChartedSpace E M] [IsManifold (modelWithCornersSelf 𝕜 E) ⊤ M] [T2Space M] [SecondCountableTopology M] {S Y : Set M} {s c : ℕ} (hS : IsClosedSubmanifold ψ S s) (hY : IsClosedSubmanifold ψ Y c) (hYS : Y ⊆ S) : ⋯.idealSheaf = IdealSheaf.pullback ⇑hS.inclusionMap ⋯ hY.idealSheaf

The ideal sheaf of Y ⊆ S as a closed submanifold of the bundled S is the restriction to S of the ideal sheaf I_Y (the centre Z_i ∩ S_i = Z_i of a restricted blow-up sequence, read inside S_i, [Kol07, Definition 30.2]).