The cosupport chain in the proof of the going-up theorem

The five cosupport lemmas that the proof of the going-up property of D-balanced ideals [Kol07, Theorem 84], item 90 of Kollár's text, strings together on the hypersurface side of the pushed-forward sequence. Throughout, cosupp(A, c) is the order-≥ c locus {x | (c : ℕ∞) ≤ A.ord x} [Kol07, Definition 59].

• cosupp_pow ([Kol07, Definition 59, (3)]): on a smooth variety, cosupp(A^s, cs) = cosupp(A, c) for s ≥ 1. This is ord_pow, ord_x (A^s) = s · ord_x A, and the cancellation of s ≠ 0, ⊤ in ℕ∞.
• cosupp_markedTransformSeq_subset_of_le ([Kol07, Definition 59, (1)]; the third displayed line of item 90): the marked transform along a sequence is monotone (markedTransformSeq_mono) and the cosupport is antitone (ord_anti), so A ≤ A' gives cosupp Π_*^{-1}(A', c) ⊆ cosupp Π_*^{-1}(A, c).
• cosupp_markedTransformSeq_pow (the fourth displayed line of item 90): for a sequence of order ≥ c for (A, c), the power rule Π_*^{-1}(A^s, cs) = (Π_*^{-1}(A, c))^s (markedTransformSeq_pow, which needs the order hypothesis for the definedness of [Kol07, Definition 60] at every step) turns cosupp_pow on the (smooth) stage into cosupp Π_*^{-1}(A^s, cs) = cosupp Π_*^{-1}(A, c).
• ordAlongEq_map_of_cosupp_subset (the opening of item 90): for a closed immersion g : Y ↪ X, an ideal sheaf A on X with max-ord A ≤ m and a centre Z ⊆ Y along which J has order ≥ m, if cosupp(J, m) maps into cosupp(A, m) then ord_{g_* Z} A = m. Purely topological: a closed immersion is a closed embedding, so the support of g_* Z = Z.map g is the image of the support of Z and its generic points are the images of the generic points of Z (specialization is preserved by g and reflected by injectivity); there J has order ≥ m, hence A has order ≥ m, and max-ord A ≤ m closes the gap.
• cosupp_markedTransformSeq_subset_iInter (the second to fifth displayed lines of item 90): for I D-balanced [Kol07, Definition 83] and T a smooth blow-up sequence of order ≥ m starting with (S, I|_S, m) on the smooth hypersurface S, at every stage i and for every j < m, cosupp(J_i, m) ⊆ cosupp T_*^{-1}((D^j I)|_S, m − j) with J_i = T_*^{-1}(I|_S, m). The chain, read from the bottom of item 90 upwards, with the marks m(m − j) throughout: cosupp(J_i, m) = cosupp(J_i^{m−j}, m(m−j)) (cosupp_pow on the stage S_i, smooth of relative dimension n − 1) = cosupp T_*^{-1}((I|_S)^{m−j}, m(m−j)) (the power rule, equality under the order hypothesis on T) = cosupp T_*^{-1}((I^{m−j})|_S, m(m−j)) (comap_pow) ⊆ cosupp T_*^{-1}(((D^j I)^m)|_S, m(m−j)) (D-balancedness (D^j I)^m ⊆ I^{m−j} restricted to S, monotonicity) ⊆ cosupp((T_*^{-1}((D^j I)|_S, m−j))^m, m(m−j)) (the unconditional power inclusion pow_markedTransformSeq_le, no order hypothesis on (D^j I)|_S needed) = cosupp T_*^{-1}((D^j I)|_S, m−j) (cosupp_pow again). Intersecting over j < m gives the inclusion cosupp(J_i, m) ⊆ ⋂_{j<m} cosupp T_*^{-1}((D^j I)|_S, m − j) that item 90 needs.

Monotonicity of the cosupport of the transform (any scheme)

theorem Hironaka.Sequence.cosupp_markedTransformSeq_subset_of_le {X : AlgebraicGeometry.Scheme} (B : X.BlowUpSequence) {A A' : X.IdealSheafData} (hAA' : A ≤ A') (c : ℕ) (i : Fin (B.length + 1)) : {x : ↥(B.stage i) | ↑c ≤ (B.markedTransformSeq A' c i).ord x} ⊆ {x : ↥(B.stage i) | ↑c ≤ (B.markedTransformSeq A c i).ord x}

Line 3 of [Kol07, 90], from [Kol07, Definition 59, (1)]: the marked transform along a sequence is monotone (markedTransformSeq_mono) and the cosupport is antitone (ord_anti), so at every stage A ≤ A' gives cosupp Π_*^{-1}(A', c) ⊆ cosupp Π_*^{-1}(A, c).

The order along the pushed-forward centre (any schemes)

theorem Hironaka.Sequence.coe_support_map_of_isClosedImmersion {X Y : AlgebraicGeometry.Scheme} (g : Y ⟶ X) [AlgebraicGeometry.IsClosedImmersion g] (Z : Y.IdealSheafData) : ↑(Z.map g).support = ⇑g '' ↑Z.support

The support of the pushforward of a centre along a closed immersion is the image of its support (a closed immersion is a closed embedding, so the image is closed and Mathlib's support_map needs no closure).

theorem Hironaka.Sequence.mem_genericPoints_support_map_iff {X Y : AlgebraicGeometry.Scheme} (g : Y ⟶ X) [AlgebraicGeometry.IsClosedImmersion g] (Z : Y.IdealSheafData) (η' : ↥X) : η' ∈ (Z.map g).support.genericPoints ↔ ∃ η ∈ Z.support.genericPoints, g η = η'

The generic points of the pushed-forward centre are the images of the generic points of the centre: g preserves specialization (continuity) and, being injective, reflects equality.

theorem Hironaka.Sequence.ordAlongEq_map_of_cosupp_subset {X Y : AlgebraicGeometry.Scheme} (g : Y ⟶ X) [AlgebraicGeometry.IsClosedImmersion g] (A : X.IdealSheafData) (J Z : Y.IdealSheafData) {m : ℕ} (hmax : A.maxOrd ≤ ↑m) (hJ : J.LeOrdAlong Z.support ↑m) (hsub : ∀ (y : ↥Y), ↑m ≤ J.ord y → ↑m ≤ A.ord (g y)) : A.OrdAlongEq (Z.map g).support ↑m

The opening of [Kol07, 90]: for a closed immersion g : Y ↪ X, an ideal sheaf A on X with max-ord A ≤ m, and a centre Z ⊆ Y along which an ideal sheaf J on Y has order ≥ m: if cosupp(J, m) maps into cosupp(A, m), then ord_{g_* Z} A = m — at a generic point g η of g_* Z, η is a generic point of Z, so m ≤ ord_η J and hence m ≤ ord_{g η} A ≤ max-ord A ≤ m.

The chain on a smooth variety

theorem Hironaka.Sequence.cosupp_pow {X : AlgebraicGeometry.Scheme} {k : Type u} [Field k] [CharZero k] (f : X ⟶ AlgebraicGeometry.Spec ↧k) (n : ℕ) [AlgebraicGeometry.SmoothOfRelativeDimension n f] (A : X.IdealSheafData) (c : ℕ) {s : ℕ} (hs : 1 ≤ s) : {x : ↥X | ↑(c * s) ≤ (A ^ s).ord x} = {x : ↥X | ↑c ≤ A.ord x}

Line 2 of [Kol07, 90], from [Kol07, Definition 59, (3)]: on a smooth variety, cosupp(A^s, cs) = cosupp(A, c) for s ≥ 1 — ord_pow, ord_x (A^s) = s · ord_x A, and cancellation of s in ℕ∞.

theorem Hironaka.Sequence.cosupp_markedTransformSeq_pow {X : AlgebraicGeometry.Scheme} {k : Type u} [Field k] [CharZero k] (f : X ⟶ AlgebraicGeometry.Spec ↧k) (n : ℕ) [AlgebraicGeometry.SmoothOfRelativeDimension n f] (B : X.BlowUpSequence) (E : X.DivisorFamily) {A : X.IdealSheafData} {c : ℕ} (h : B.IsOrderGeSeq f A c E) {s : ℕ} (hs : 1 ≤ s) (i : Fin (B.length + 1)) : {x : ↥(B.stage i) | ↑(c * s) ≤ (B.markedTransformSeq (A ^ s) (c * s) i).ord x} = {x : ↥(B.stage i) | ↑c ≤ (B.markedTransformSeq A c i).ord x}

Line 4 of [Kol07, 90], from [Kol07, Definition 59, (3)]: along a smooth blow-up sequence of order ≥ c for (A, c), for s ≥ 1 and at every stage, cosupp Π_*^{-1}(A^s, cs) = cosupp Π_*^{-1}(A, c) — the power rule and cosupp_pow on the stage, which is smooth of relative dimension n.

theorem Hironaka.Sequence.cosupp_markedTransformSeq_subset_iInter {X : AlgebraicGeometry.Scheme} {k : Type u} [Field k] [CharZero k] (f : X ⟶ AlgebraicGeometry.Spec ↧k) (n : ℕ) [AlgebraicGeometry.SmoothOfRelativeDimension n f] (S I : X.IdealSheafData) (m : ℕ) (T : S.subscheme.BlowUpSequence) (hI : AlgebraicGeometry.Scheme.IdealSheafData.IsDBalanced f I m) (hS : AlgebraicGeometry.IsSmoothDivisor S) {E' : S.subscheme.DivisorFamily} (hT : T.IsOrderGeSeq (CategoryTheory.CategoryStruct.comp S.subschemeι f) (I.comap S.subschemeι) m E') (i : Fin (T.length + 1)) : {y : ↥(T.stage i) | ↑m ≤ (T.markedTransformSeq (I.comap S.subschemeι) m i).ord y} ⊆ ⋂ (j : ℕ), ⋂ (_ : j < m), {y : ↥(T.stage i) | ↑(m - j) ≤ (T.markedTransformSeq ((AlgebraicGeometry.Scheme.IdealSheafData.derivativeIter f j I).comap S.subschemeι) (m - j) i).ord y}

Lines 2–5 of [Kol07, 90] with [Kol07, Definition 83]: for I D-balanced with respect to m, S a smooth hypersurface and T a smooth blow-up sequence of order ≥ m starting with (S, I|_S, m), at every stage i the cosupport of J_i = T_*^{-1}(I|_S, m) lies in every cosupp T_*^{-1}((D^j I)|_S, m − j), j < m — the chain of the module docstring, pointwise at y ∈ S_i.