Corollary 89: the cosupport of the transform on the hypersurface of centers

Kollár's Corollary 89 [Kol07, Corollary 89]: with the notation of [Kol07, Theorem 88], a smooth blow-up sequence of order ≥ m for (X, I, m) and a smooth hypersurface S whose strict transforms S_i contain the centers,

S_r ∩ cosupp Π_*^{-1}(I, m) = ⋂_{j < m} cosupp (Π|_{S_r})_*^{-1}((D^j I)|_S, m − j).

• Logarithmic derivatives restrict, along a closed immersion. Kollár's (87.1) [Kol07, 87], (D^r(−log S)(I))|_S = D^r(I|_S), is proved in Hironaka/Scheme/IdealSheaf/Derivative/LogarithmicSheaf.lean along the inclusion V(S) ↪ X; the same stalkwise argument (the stalk map of a closed immersion is surjective with kernel the stalk of its kernel ideal sheaf, and the stalk of a smooth scheme is formally smooth over k) gives it along any closed immersion g : Y ⟶ X with the hypersurface ker g (logDerivativeIter_comap_of_isClosedImmersion). The stage embeddings S_i ↪ X_i of the restricted sequence are such closed immersions, with kernel S_i.
• Kollár's (89.1). Theorem 88 at stage i, restricted along S_i ↪ X_i: comap commutes with the sum, (87.1) turns D^{s−j}(−log S_i) into D^{s−j} on S_i, and the restriction of the marked transform Π_*^{-1}(D^j I, m − j) is the marked transform of the restricted data along the restricted sequence, [Kol07, Lemma 62] iterated (IsOrderGeSeq.markedTransformSeq_comap_pullbackStageHom) on the sequence of order ≥ m − j for (D^j I, m − j) [Kol07, Corollary 77]. The structure morphisms of the restricted stage agree by pullbackStageHom_stageMap.
• Kollár's (89.2) and (89.3). A marking-one cosupport is a support (one_le_ord_iff) and supports pull back (support_comap); the cosupport of a sum is the intersection of the cosupports ([Kol07, Definition 59 (4)]) because the stalk of a sum is the sum of the stalks and ⨆ ≤ 𝔪^c iff each summand is.
• Corollary 89. For m ≥ 1, (89.1) at s = m − 1: the left cosupport is cosupp (Π_*^{-1}(I, m), m) pulled back to S_i (cosupp(I, m) = cosupp(D^{m−1} I, 1), [Kol07, Lemma 74 (3)], coe_support_MC at the stage X_i), the right one is the intersection of the cosupp (J_j, m − j), j ≤ m − 1 (Lemma 74 (3) at the mark m − j on the restricted stage S_i, smooth of relative dimension n − 1 over k). For m = 0 both sides are the whole space.

Corollary 89 is the input of the going-up theorem for D-balanced ideals (Hironaka/Resolution/Algebraic/Kol07/GoingUp.lean), where it is read on a pushed-forward sequence.

Cosupports of a restriction and of a sum

theorem Hironaka.Sequence.cosupp_one_comap {X Y : AlgebraicGeometry.Scheme} (g : Y ⟶ X) (A : X.IdealSheafData) : {y : ↥Y | 1 ≤ (A.comap g).ord y} = ⇑g ⁻¹' {x : ↥X | 1 ≤ A.ord x}

A marking-one cosupport is the support, and the support of a restriction is the preimage of the support (Kollár's (89.2), [Kol07, Corollary 89]).

theorem Hironaka.Sequence.cosupp_iSup_eq_iInter {X : AlgebraicGeometry.Scheme} {ι : Sort u_1} (A : ι → X.IdealSheafData) (c : ℕ) : {x : ↥X | ↑c ≤ (⨆ (i : ι), A i).ord x} = ⋂ (i : ι), {x : ↥X | ↑c ≤ (A i).ord x}

The cosupport of a sum is the intersection of the cosupports ([Kol07, Definition 59 (4)] iterated, as in Kollár's (89.3)): the stalk of the sum is the sum of the stalks, and it lies in 𝔪^c iff every summand does.

Restriction of logarithmic derivatives along a closed immersion

theorem Hironaka.Sequence.logDerivativeIter_comap_of_isClosedImmersion {X : AlgebraicGeometry.Scheme} {k : Type u} [Field k] (f : X ⟶ AlgebraicGeometry.Spec ↧k) (n : ℕ) [AlgebraicGeometry.SmoothOfRelativeDimension n f] {Y : AlgebraicGeometry.Scheme} (g : Y ⟶ X) [AlgebraicGeometry.IsClosedImmersion g] (I : X.IdealSheafData) (r : ℕ) : (AlgebraicGeometry.Scheme.IdealSheafData.logDerivativeIter f (AlgebraicGeometry.Scheme.Hom.ker g) r I).comap g = AlgebraicGeometry.Scheme.IdealSheafData.derivativeIter (CategoryTheory.CategoryStruct.comp g f) r (I.comap g)

Kollár's (87.1) [Kol07, 87] along any closed immersion g : Y ⟶ X with hypersurface ker g (logDerivativeIter_comap_subschemeι is the case g = S.subschemeι): (D^r(−log (ker g))(I))|_Y = D^r(I|_Y). Stalkwise: the stalk map of a closed immersion is surjective with kernel the stalk of ker g (ker_stalkMap_of_isClosedImmersion), and the stalk of a smooth scheme is formally smooth over k.

Kollár's (89.1) and Corollary 89

theorem Hironaka.Sequence.derivativeIter_comap_pullbackStageHom_eq_iSup {X : AlgebraicGeometry.Scheme} {k : Type u} [Field k] [CharZero k] (f : X ⟶ AlgebraicGeometry.Spec ↧k) (n : ℕ) [AlgebraicGeometry.SmoothOfRelativeDimension n f] (B : X.BlowUpSequence) (S I : X.IdealSheafData) (E : X.DivisorFamily) (m : ℕ) (hS : AlgebraicGeometry.IsSmoothDivisor S) (h : B.IsOrderGeSeq f I m E) (hZS : ∀ (i : Fin B.length), B.strictTransformSeq S i.castSucc ≤ B.center i) {s : ℕ} (hs : s ≤ m) (i : Fin (B.length + 1)) : (AlgebraicGeometry.Scheme.IdealSheafData.derivativeIter (CategoryTheory.CategoryStruct.comp (B.stageMap i) f) s (B.markedTransformSeq I m i)).comap (B.pullbackStageHom S.subschemeι i) = ⨆ (j : ℕ), ⨆ (_ : j ≤ s), AlgebraicGeometry.Scheme.IdealSheafData.derivativeIter (CategoryTheory.CategoryStruct.comp ((B.pullback S.subschemeι).stageMap (B.pullbackStageIdx S.subschemeι i)) (CategoryTheory.CategoryStruct.comp S.subschemeι f)) (s - j) ((B.pullback S.subschemeι).markedTransformSeq ((AlgebraicGeometry.Scheme.IdealSheafData.derivativeIter f j I).comap S.subschemeι) (m - j) (B.pullbackStageIdx S.subschemeι i))

Kollár's (89.1) in the proof of [Kol07, Corollary 89]: Theorem 88 at stage i, restricted along S_i ↪ X_i; (87.1) for the logarithmic derivatives, [Kol07, Lemma 62] iterated for the marked transforms, on the sequence of order ≥ m − j for (D^j I, m − j).

theorem Hironaka.Sequence.cosupp_markedTransformSeq_inter_eq_iInter {X : AlgebraicGeometry.Scheme} {k : Type u} [Field k] [CharZero k] (f : X ⟶ AlgebraicGeometry.Spec ↧k) (n : ℕ) [AlgebraicGeometry.SmoothOfRelativeDimension n f] (B : X.BlowUpSequence) (S I : X.IdealSheafData) (E : X.DivisorFamily) (m : ℕ) (hS : AlgebraicGeometry.IsSmoothDivisor S) (h : B.IsOrderGeSeq f I m E) (hZS : ∀ (i : Fin B.length), B.strictTransformSeq S i.castSucc ≤ B.center i) (i : Fin (B.length + 1)) : {y : ↥((B.pullback S.subschemeι).stage (B.pullbackStageIdx S.subschemeι i)) | ↑m ≤ (B.markedTransformSeq I m i).ord ((B.pullbackStageHom S.subschemeι i) y)} = ⋂ (j : ℕ), ⋂ (_ : j < m), {y : ↥((B.pullback S.subschemeι).stage (B.pullbackStageIdx S.subschemeι i)) | ↑(m - j) ≤ ((B.pullback S.subschemeι).markedTransformSeq ((AlgebraicGeometry.Scheme.IdealSheafData.derivativeIter f j I).comap S.subschemeι) (m - j) (B.pullbackStageIdx S.subschemeι i)).ord y}

Kollár's Corollary 89 [Kol07, Corollary 89] at every stage: (89.1) at s = m − 1, the cosupports taken by cosupp_one_comap, cosupp_iSup_eq_iInter and [Kol07, Lemma 74 (3)] at the marks m (on X_i) and m − j (on S_i); for m = 0 both sides are the whole space.