Tools for the un-isolated ideal

The statement CP6 of the embedded desingularization (Hironaka.Resolution.Algebraic.Wlo05.EmbeddedChainRelative) follows the un-isolated ideal I₀ = I_Γ ⊓ K along the loop bedAux (Hironaka.Resolution.Algebraic.Wlo05.Embedded): at every stage its mark-1 transform is Ĩ_Γ ⊓ K̃, the strict transform of the protected components intersected with the transform of the isolated ideal, and the identity is checked STALKWISE, on the blow-up of a stage, from the chain forms. This module provides the stalk tools for that check and the two structural lemmas that carry it along a sequence:

• the stalk of a finite intersection of ideal sheaves is the intersection of the stalks (localisation commutes with finite intersections); for the ideal of a disjoint union of closed subschemes, at a point of one member the stalk of the intersection is that member's stalk, and off the union it is the unit ideal;
• at a point p ∈ Γ, an ideal chain-relative monomial along Γ is the intersection of the stalk of Γ with the stalk of its colon by Γ (chainIdeal_eq_span_inf_chainKIdeal of Hironaka.Resolution.Algebraic.Wlo05.ChainIdealInf with CP2's chainRelativeKAt_colon);
• locality of the marked transform through the stalk at π q, and the unit stalk of a strict transform off π⁻¹(Γ);
• clause (4′) of [Kol07, Definition 66] at the mark 1: along a sequence of order ≥ 1 the marked transform lies in the ideal of the centre (the centre is smooth, hence reduced), the hypothesis K ≤ Z of the one-blow-up identity of CP4 (Hironaka.Resolution.Algebraic.Wlo05.EmbeddedCP4Sheaf);
• the single-ideal transport markedTransformSeq_eq_inf_of_forall_step: I₀ = P ⊓ K and the one-blow-up identity at every stage give I_j = P̃_j ⊓ K_j at every stage — the induction engine of CP6, by structural recursion on the sequence;
• the bridge for a disjoint union of reduced closed subschemes: its ideal is the vanishing ideal of the union of the supports, it is reduced, its support is the union, and its strict transform along a sequence is the intersection of the members' strict transforms (strictTransformSeq_biInf_of_pairwise_disjoint) — the protected components as a single ideal P = ⨅ γ ∈ Γs, γ, the shape the transport lemma consumes.

These lemmas are not in the literature. Used in Hironaka.Resolution.Algebraic.Wlo05.EmbeddedCP4Sheaf, Hironaka.Resolution.Algebraic.Wlo05.EmbeddedCP6Isolation, Hironaka.Resolution.Algebraic.Wlo05.EmbeddedCP6Stage, Hironaka.Resolution.Algebraic.Wlo05.EmbeddedCP6Loop and Hironaka.Resolution.Algebraic.Wlo05.EmbeddedCP5.

Stalks: finite intersections, disjoint unions, locality

theorem Hironaka.Resolution.stalkIdeal_inf {X : AlgebraicGeometry.Scheme} (I J : X.IdealSheafData) (x : ↥X) : (I ⊓ J).stalkIdeal x = I.stalkIdeal x ⊓ J.stalkIdeal x

The stalk of a finite intersection of ideal sheaves is the intersection of the stalks (localisation of finitely generated ideals commutes with finite intersections).

theorem Hironaka.Resolution.stalkIdeal_finset_biInf {X : AlgebraicGeometry.Scheme} {ι : Type u_1} (A : Finset ι) (I : ι → X.IdealSheafData) (x : ↥X) : (⨅ a ∈ A, I a).stalkIdeal x = ⨅ a ∈ A, (I a).stalkIdeal x

stalkIdeal_inf for a finite family.

theorem Hironaka.Resolution.stalkIdeal_biInf_eq_of_mem_of_pairwise_disjoint {X : AlgebraicGeometry.Scheme} {ι : Type u_1} (A : Finset ι) (I : ι → X.IdealSheafData) (hdisj : (↑A).Pairwise fun (a b : ι) => Disjoint (I a).support (I b).support) {a : ι} (ha : a ∈ A) {x : ↥X} (hx : x ∈ (I a).support) : (⨅ b ∈ A, I b).stalkIdeal x = (I a).stalkIdeal x

The ideal of a disjoint union: at a point of one member of a finite family of ideal sheaves with pairwise disjoint supports, the stalk of the intersection is that member's stalk.

theorem Hironaka.Resolution.stalkIdeal_biInf_eq_top_of_forall_notMem {X : AlgebraicGeometry.Scheme} {ι : Type u_1} (A : Finset ι) (I : ι → X.IdealSheafData) {x : ↥X} (hx : ∀ a ∈ A, x ∉ (I a).support) : (⨅ b ∈ A, I b).stalkIdeal x = ⊤

Off the union of the supports the intersection has the unit stalk.

theorem Hironaka.Resolution.stalkIdeal_eq_inf_colon_of_chainRelativeAt {k : Type u} [Field k] {X : AlgebraicGeometry.Scheme} (f : X ⟶ AlgebraicGeometry.Spec ↧k) [AlgebraicGeometry.Smooth f] {E : X.DivisorFamily} {I Γ : X.IdealSheafData} {p : ↥X} (h : ChainRelativeAt E I Γ p) : I.stalkIdeal p = Γ.stalkIdeal p ⊓ (I.colon Γ).stalkIdeal p

The intersection form at p ∈ Γ on the scheme (CP2's chainRelativeKAt_colon gives the K-shape of the colon in the same coordinates): an ideal chain-relative monomial along Γ at p is, at p, the intersection of the stalk of Γ with the stalk of its colon by Γ, I_p = I_{Γ,p} ⊓ (I : I_Γ)_p.

theorem Hironaka.Resolution.stalkIdeal_markedTransform_eq_of_stalkIdeal_eq {X : AlgebraicGeometry.Scheme} [AlgebraicGeometry.IsLocallyNoetherian X] (D I K : X.IdealSheafData) (m : ℕ) {q : ↥D.blowUp} (h : I.stalkIdeal (D.blowUpπ q) = K.stalkIdeal (D.blowUpπ q)) : (I.markedTransform D m).stalkIdeal q = (K.markedTransform D m).stalkIdeal q

Locality of the marked transform: the mark-m transform along the blow-up of D has, at a point q, a stalk determined by the stalk of the ideal at π q — two ideals with the same stalk at π q have transforms with the same stalk at q (stalkIdeal_comap, the stalk of a colon on a Noetherian scheme).

theorem Hironaka.Resolution.stalkIdeal_strictTransform_eq_top_of_notMem {X : AlgebraicGeometry.Scheme} [AlgebraicGeometry.IsLocallyNoetherian X] (D Γ : X.IdealSheafData) {q : ↥D.blowUp} (h : D.blowUpπ q ∉ Γ.support) : (Γ.strictTransform D).stalkIdeal q = ⊤

The strict transform of Γ has the unit stalk at a point whose image is off Γ (its support lies in π⁻¹(Γ)).

theorem Hironaka.Resolution.markedTransformSeq_le_center_of_isOrderGeSeq {k : Type u} [Field k] {X : AlgebraicGeometry.Scheme} (f : X ⟶ AlgebraicGeometry.Spec ↧k) (S : X.BlowUpSequence) (I : X.IdealSheafData) (E : X.DivisorFamily) (hS : S.IsOrderGeSeq f I 1 E) (i : Fin S.length) : S.markedTransformSeq I 1 i.castSucc ≤ S.center i

For a sequence of order ≥ 1 for (I, 1), the marked transform at a stage lies in the ideal of the centre ([Kol07, Definition 66 (4′)]: the order along the centre is ≥ 1; the centre is smooth, hence reduced). This is the hypothesis K_n ≤ Z_n of the sheaf form of CP4.

The transport of the intersection form along a succession

theorem Hironaka.Resolution.markedTransformSeq_eq_inf_of_forall_step {X : AlgebraicGeometry.Scheme} (S : X.BlowUpSequence) (P I₀ K : X.IdealSheafData) : I₀ = P ⊓ K → (∀ (i : Fin S.length), S.markedTransformSeq I₀ 1 i.castSucc = S.strictTransformSeq P i.castSucc ⊓ S.markedTransformSeq K 1 i.castSucc → (S.markedTransformSeq I₀ 1 i.castSucc).markedTransform (S.center i) 1 = (S.strictTransformSeq P i.castSucc).strictTransform (S.center i) ⊓ (S.markedTransformSeq K 1 i.castSucc).markedTransform (S.center i) 1) → ∀ (i : Fin (S.length + 1)), S.markedTransformSeq I₀ 1 i = S.strictTransformSeq P i ⊓ S.markedTransformSeq K 1 i

The single-ideal form of the transport of the invariant: I₀ = P ⊓ K and the one-step identity at every stage give I_j = P̃_j ⊓ K_j at every stage.

The ideal of a disjoint union of reduced closed subschemes and its strict transforms

theorem Hironaka.Resolution.biInf_eq_vanishingIdeal_biSup_support {X : AlgebraicGeometry.Scheme} (Γs : Finset X.IdealSheafData) (hred : ∀ γ ∈ Γs, AlgebraicGeometry.IsReduced γ.subscheme) : ⨅ γ ∈ Γs, γ = AlgebraicGeometry.Scheme.IdealSheafData.vanishingIdeal (⨆ γ ∈ Γs, γ.support)

A finite intersection of reduced ideal sheaves is the vanishing ideal of the union of their supports (each is the vanishing ideal of its support; vanishingIdeal_iSup).

theorem Hironaka.Resolution.isReduced_biInf_subscheme {X : AlgebraicGeometry.Scheme} (Γs : Finset X.IdealSheafData) (hred : ∀ γ ∈ Γs, AlgebraicGeometry.IsReduced γ.subscheme) : AlgebraicGeometry.IsReduced (⨅ γ ∈ Γs, γ).subscheme

The intersection of finitely many reduced ideal sheaves is reduced.

theorem Hironaka.Resolution.coe_support_biInf {X : AlgebraicGeometry.Scheme} (Γs : Finset X.IdealSheafData) (hred : ∀ γ ∈ Γs, AlgebraicGeometry.IsReduced γ.subscheme) : ↑(⨅ γ ∈ Γs, γ).support = ⋃ γ ∈ Γs, ↑γ.support

The support of a finite intersection of reduced ideal sheaves is the union of the supports.

theorem Hironaka.Resolution.strictTransformSeq_biInf_of_pairwise_disjoint {X : AlgebraicGeometry.Scheme} [AlgebraicGeometry.IsLocallyNoetherian X] (S : X.BlowUpSequence) (Γs : Finset X.IdealSheafData) (hred : ∀ γ ∈ Γs, AlgebraicGeometry.IsReduced γ.subscheme) (hdisj : (↑Γs).Pairwise fun (a b : X.IdealSheafData) => Disjoint a.support b.support) (i : Fin (S.length + 1)) : S.strictTransformSeq (⨅ γ ∈ Γs, γ) i = ⨅ γ ∈ Γs, S.strictTransformSeq γ i

The strict transform of a disjoint union is the intersection of the strict transforms: for reduced ideal sheaves with pairwise disjoint supports, the strict transform of their intersection along a sequence is the intersection of their strict transforms (both reduced with the same support; strictTransformSeq_eq_prod_of_pairwise_disjoint and ⨅ = ∏ for disjoint supports).