The ideal sheaf of the centre and the total transform

The ideal sheaf I_Y of a closed submanifold Y (the specification IsIdealSheafOf: cosupport Y, stalks on Y spanned by the adapted coordinates) exists and is unique, so the classically chosen IsClosedSubmanifold.idealSheaf satisfies the specification. The construction is IdealSheaf.ofStalks applied to the stalks given by the kernel of the restriction of germs 𝒪_{M,a} → 𝒪_{Y,a} at points of Y and by the unit ideal off Y: these stalks have local generators; over an adapted chart, the coordinate sections ψ_{σ i} ∘ φ (their germs span the kernel at points of Y, and one of them is a unit at a point of the chart off Y, since its value there is nonzero); off Y, the section 1 on the open complement. Uniqueness is stalkwise (IdealSheaf.ext): both stalks are the span of the adapted coordinates on Y and the unit ideal off Y. The stalks of the total transform are those of the pullback of an ideal sheaf [Hir64, Ch. 0, §5, p. 142]. On an open subset U ⊆ M the trace Y ∩ U is a closed submanifold of U (its adapted charts are the restrictions subtypeRestr of those of Y) whose ideal sheaf is the pullback of I_Y along the inclusion (IsClosedSubmanifold.preimage_val, isIdealSheafOf_pullback_val, IsClosedSubmanifold.idealSheaf_preimage_val).

These are the objects on which the transforms of Hironaka.Manifold.BlowUp.Transform.Colon and the sequences of blowings-up (FiniteSuccession) operate.

noncomputable def Manifold.IsClosedSubmanifold.centerStalk {𝕜 : Type} [RCLike 𝕜] {E : Type u_1} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {n : ℕ} {ψ : E ≃L[𝕜] Fin n → 𝕜} {M : Type u} [TopologicalSpace M] [ChartedSpace E M] {Y : Set M} {c : ℕ} (hY : IsClosedSubmanifold ψ Y c) (a : M) : Ideal ↑((structureSheaf 𝕜 E M).presheaf.stalk a)

The stalks of the ideal sheaf of the closed submanifold Y: the kernel of the restriction of germs 𝒪_{M,a} → 𝒪_{Y,a} at a point of Y, the unit ideal off Y.

Equations

• hY.centerStalk a = if h : a ∈ Y then RingHom.ker (hY.restrictStalk ⟨a, h⟩) else ⊤

theorem Manifold.IsClosedSubmanifold.centerStalk_of_mem {𝕜 : Type} [RCLike 𝕜] {E : Type u_1} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {n : ℕ} {ψ : E ≃L[𝕜] Fin n → 𝕜} {M : Type u} [TopologicalSpace M] [ChartedSpace E M] {Y : Set M} {c : ℕ} (hY : IsClosedSubmanifold ψ Y c) {a : M} (ha : a ∈ Y) : hY.centerStalk a = RingHom.ker (hY.restrictStalk ⟨a, ha⟩)

The stalk of the centre's ideal at a point of Y.

theorem Manifold.IsClosedSubmanifold.centerStalk_of_notMem {𝕜 : Type} [RCLike 𝕜] {E : Type u_1} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {n : ℕ} {ψ : E ≃L[𝕜] Fin n → 𝕜} {M : Type u} [TopologicalSpace M] [ChartedSpace E M] {Y : Set M} {c : ℕ} (hY : IsClosedSubmanifold ψ Y c) {a : M} (ha : a ∉ Y) : hY.centerStalk a = ⊤

The stalk of the centre's ideal off Y is the unit ideal.

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

At a point of Y in an adapted chart, the kernel of the restriction of germs is spanned by the adapted coordinates (which vanish at that point).

theorem Manifold.IsClosedSubmanifold.hasLocalGenerators_centerStalk {𝕜 : Type} [RCLike 𝕜] {E : Type u_1} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {n : ℕ} {ψ : E ≃L[𝕜] Fin n → 𝕜} {M : Type u} [TopologicalSpace M] [ChartedSpace E M] {Y : Set M} {c : ℕ} (hY : IsClosedSubmanifold ψ Y c) : IdealSheaf.HasLocalGenerators hY.centerStalk

The stalks of the centre's ideal have local generators: the coordinate sections of an adapted chart on Y, the section 1 on the complement of Y.

theorem Manifold.IsClosedSubmanifold.exists_isIdealSheafOf {𝕜 : Type} [RCLike 𝕜] {E : Type u_1} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {n : ℕ} {ψ : E ≃L[𝕜] Fin n → 𝕜} {M : Type u} [TopologicalSpace M] [ChartedSpace E M] {Y : Set M} {c : ℕ} (hY : IsClosedSubmanifold ψ Y c) : ∃ (J : IdealSheaf (structureSheaf 𝕜 E M)), IsIdealSheafOf ψ Y c J

The ideal sheaf of a closed submanifold exists (the specification IsIdealSheafOf).

theorem Manifold.IsIdealSheafOf.stalkIdeal_of_notMem {𝕜 : Type} [RCLike 𝕜] {E : Type u_1} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {n : ℕ} {ψ : E ≃L[𝕜] Fin n → 𝕜} {M : Type u} [TopologicalSpace M] [ChartedSpace E M] {Y : Set M} {c : ℕ} {J : IdealSheaf (structureSheaf 𝕜 E M)} (hJ : IsIdealSheafOf ψ Y c J) {a : M} (ha : a ∉ Y) : J.stalkIdeal a = ⊤

Off Y, the stalk of an ideal sheaf of Y is the unit ideal.

theorem Manifold.totalTransform_stalkIdeal_eq_span {𝕜 : Type} [RCLike 𝕜] {E : Type u_1} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {n : ℕ} {ψ : E ≃L[𝕜] Fin n → 𝕜} {M : Type u} [TopologicalSpace M] [ChartedSpace E M] {Y : Set M} {c : ℕ} {M' : Type u} [TopologicalSpace M'] [ChartedSpace E M'] [IsManifold (modelWithCornersSelf 𝕜 E) ⊤ M'] [T2Space M'] [SecondCountableTopology M'] {π : M' → M} (h : IsBlowUp ψ Y c π) (I : IdealSheaf (structureSheaf 𝕜 E M)) {U : TopologicalSpace.Opens M} {k : ℕ} {f : Fin k → ↑((structureSheaf 𝕜 E M).presheaf.obj (Opposite.op U))} (hgen : ∀ (b : M) (hb : b ∈ U), I.stalkIdeal b = Ideal.span (Set.range fun (j : Fin k) => (CategoryTheory.ConcreteCategory.hom ((structureSheaf 𝕜 E M).presheaf.germ U b hb)) (f j))) {a' : M'} (ha' : π a' ∈ U) : (IdealSheaf.pullback π ⋯ I).stalkIdeal a' = Ideal.span (Set.range fun (j : Fin k) => (germMap π ⋯ a') ((CategoryTheory.ConcreteCategory.hom ((structureSheaf 𝕜 E M).presheaf.germ U (π a') ha')) (f j)))

The total transform is generated by the f ∘ π for local generators f of I.

theorem Manifold.IsClosedSubmanifold.isIdealSheafOf_idealSheaf {𝕜 : Type} [RCLike 𝕜] {E : Type u_1} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {n : ℕ} {ψ : E ≃L[𝕜] Fin n → 𝕜} {M : Type u} [TopologicalSpace M] [ChartedSpace E M] {Y : Set M} {c : ℕ} (hY : IsClosedSubmanifold ψ Y c) : IsIdealSheafOf ψ Y c hY.idealSheaf

The chosen ideal sheaf hY.idealSheaf satisfies the specification IsIdealSheafOf.

theorem Manifold.IsIdealSheafOf.eq_idealSheaf {𝕜 : Type} [RCLike 𝕜] {E : Type u_1} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {n : ℕ} {ψ : E ≃L[𝕜] Fin n → 𝕜} {M : Type u} [TopologicalSpace M] [ChartedSpace E M] {Y : Set M} {c : ℕ} (hY : IsClosedSubmanifold ψ Y c) {J : IdealSheaf (structureSheaf 𝕜 E M)} (hJ : IsIdealSheafOf ψ Y c J) : J = hY.idealSheaf

The ideal sheaf of a closed submanifold is unique.

theorem Manifold.IsClosedSubmanifold.cosupport_idealSheaf {𝕜 : Type} [RCLike 𝕜] {E : Type u_1} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {n : ℕ} {ψ : E ≃L[𝕜] Fin n → 𝕜} {M : Type u} [TopologicalSpace M] [ChartedSpace E M] {Y : Set M} {c : ℕ} (hY : IsClosedSubmanifold ψ Y c) : hY.idealSheaf.support = Y

The cosupport of the ideal sheaf of Y is Y.

theorem Manifold.IsClosedSubmanifold.stalkIdeal_idealSheaf_of_mem {𝕜 : Type} [RCLike 𝕜] {E : Type u_1} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {n : ℕ} {ψ : E ≃L[𝕜] Fin n → 𝕜} {M : Type u} [TopologicalSpace M] [ChartedSpace E M] {Y : Set M} {c : ℕ} (hY : IsClosedSubmanifold ψ Y c) {a : M} (ha : a ∈ Y) : hY.idealSheaf.stalkIdeal a = RingHom.ker (hY.restrictStalk ⟨a, ha⟩)

At a point of Y, the stalk of the ideal sheaf of Y is the kernel of the restriction of germs.

theorem Manifold.IsClosedSubmanifold.stalkIdeal_idealSheaf_of_notMem {𝕜 : Type} [RCLike 𝕜] {E : Type u_1} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {n : ℕ} {ψ : E ≃L[𝕜] Fin n → 𝕜} {M : Type u} [TopologicalSpace M] [ChartedSpace E M] {Y : Set M} {c : ℕ} (hY : IsClosedSubmanifold ψ Y c) {a : M} (ha : a ∉ Y) : hY.idealSheaf.stalkIdeal a = ⊤

Off Y the stalk of the ideal sheaf of Y is the unit ideal.

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

At a point of Y, the stalk of the ideal sheaf of Y is spanned by the adapted coordinates of any adapted chart.

The centre on an open subset

theorem Manifold.IsClosedSubmanifold.preimage_val {𝕜 : Type} [RCLike 𝕜] {E : Type u_1} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {n : ℕ} {ψ : E ≃L[𝕜] Fin n → 𝕜} {M : Type u} [TopologicalSpace M] [ChartedSpace E M] {Y : Set M} {c : ℕ} [IsManifold (modelWithCornersSelf 𝕜 E) ⊤ M] (hY : IsClosedSubmanifold ψ Y c) (U : TopologicalSpace.Opens M) : IsClosedSubmanifold ψ (Subtype.val ⁻¹' Y) c

The trace of a closed submanifold on an open subset U is a closed submanifold of U of the same codimension — its adapted charts are the restrictions of the adapted charts of Y.

theorem Manifold.isIdealSheafOf_pullback_val {𝕜 : Type} [RCLike 𝕜] {E : Type u_1} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {n : ℕ} {ψ : E ≃L[𝕜] Fin n → 𝕜} {M : Type u} [TopologicalSpace M] [ChartedSpace E M] {Y : Set M} {c : ℕ} [IsManifold (modelWithCornersSelf 𝕜 E) ⊤ M] (hY : IsClosedSubmanifold ψ Y c) (U : TopologicalSpace.Opens M) : IsIdealSheafOf ψ (Subtype.val ⁻¹' Y) c (IdealSheaf.pullback Subtype.val ⋯ hY.idealSheaf)

The pullback of the ideal sheaf of Y along the inclusion of an open subset U is the ideal sheaf of the trace Y ∩ U — cosupport Y ∩ U, and in an adapted chart of the trace, extended to M, the stalk spanned by the coordinate germs, which the stalk map of the inclusion carries to the coordinate germs of the chart of U.

theorem Manifold.IsClosedSubmanifold.idealSheaf_preimage_val {𝕜 : Type} [RCLike 𝕜] {E : Type u_1} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {n : ℕ} {ψ : E ≃L[𝕜] Fin n → 𝕜} {M : Type u} [TopologicalSpace M] [ChartedSpace E M] {Y : Set M} {c : ℕ} [IsManifold (modelWithCornersSelf 𝕜 E) ⊤ M] (hY : IsClosedSubmanifold ψ Y c) (U : TopologicalSpace.Opens M) (hY' : IsClosedSubmanifold ψ (Subtype.val ⁻¹' Y) c) : hY'.idealSheaf = IdealSheaf.pullback Subtype.val ⋯ hY.idealSheaf

The ideal sheaf of the trace is the pullback of the ideal sheaf of the centre (uniqueness of the ideal sheaf of a closed submanifold).