Step 1 of order reduction: the reduced functor inherits clauses (1) and (2) #
OrderSeqAssignment.ofTuned B hDom is
Step 1 of the proof of [Kol07, Theorem 103] read as a construction: from a smooth blow-up sequence
functor B of order s(m) on tuned triples, the functor of order m on BOClass n m whose value
on (X, I, E) is B(X, W_{s(m)}(I), E) when max-ord I = m and the empty sequence when max-ord I < m. This module shows that the clauses of Theorem 103 pass from B to the reduced functor.
The two values (ofTuned_seq_of_maxOrd_eq, ofTuned_seq_of_maxOrd_lt) are the two branches of
the definition.
Clause (1) (ofTuned_maxOrd_lt). Above the mark the value is B on the tuned triple, a
sequence of order m for (X, I, E) by [Kol07, Corollary 101] (isOrderSeq_tuned_iff), along
which max-ord W_r < s(m), clause (1) for B, gives max-ord I_r < m
(maxOrd_weakTransformSeq_lt_iff_tuned). Below the mark the value is empty, I_r = I, and
max-ord I < m is the case hypothesis.
Clause (2), smooth morphisms (ofTuned_commutesWithSmooth, [Kol07, 34.1]). The case splits of
the two triples must align, and they do: the maximal order does not increase under a smooth
pull-back (maxOrd_comap_le_of_smooth, the order being preserved pointwise) and does not decrease
under a surjection (maxOrd_le_maxOrd_comap_of_surjective, every point having a preimage). For a
smooth surjection both triples are above the mark or both below; above, the tuned triples are
again a pull-back pair (isPullbackOf_tuned) and B commutes; below, both values are empty. For
an arbitrary smooth morphism the same holds except in one case, T above the mark and its
pull-back T' below. There the value on T' is empty, and the pulled-back sequence with its empty
blow-ups deleted is a smooth blow-up sequence of order m for T' without empty centres
(isOrderSeq_eraseEmpty_pullback_of_equidim), which must itself be empty: its first centre would
carry a generic point of a component where I' has order m, above max-ord I' < m
(eq_nil_of_isOrderSeq_of_maxOrd_lt).
Clause (2), change of fields (ofTuned_commutesWithBaseChange, [Kol07, 34.2]). The maximal
order is preserved under a change of fields in characteristic zero
(maxOrd_comap_of_isPullback_specMap): it does not decrease because the projection is surjective
and the order can only grow under pull-back, and it does not increase because max-ord I ≤ μ iff
the iterated derivative D^μ I is the unit ideal (derivativeIter_eq_top_iff_maxOrd_le) and the
derivative commutes with the base-change square (derivativeIter_comap_of_isPullback_specMap). No
pointwise comparison of orders under a transcendental extension is needed. The case splits
therefore align, and the tuned triples are again a base-change pair (isBaseChangeOf_tuned).
The general form. The construction and the three transfers depend on the class BOClass n m
only through 1 ≤ m and max-ord I ≤ m, so they are stated first for
OrderSeqAssignment.ofTunedClass on an arbitrary class C with hypotheses hmC : ∀ T, C T → 1 ≤ m
and hmax : ∀ T, C T → max-ord I ≤ m (ofTunedClass_seq_of_maxOrd_eq,
ofTunedClass_seq_of_maxOrd_lt, ofTunedClass_seq_isOrderSeq, ofTunedClass_seq_noEmptyCenters,
ofTunedClass_maxOrd_lt, ofTunedClass_commutesWithSmooth, ofTunedClass_commutesWithBaseChange);
the ofTuned_* lemmas are their instances at C := BOClass n m, and the boundary-clearing
functor Hironaka.BD.tunedFunctor takes its instances at C := BDClass n m j.
The last section shows that a change of fields preserves the order of an ideal at every point
(Hironaka.BMO.ord_comap_of_isPullback_specMap), the pointwise form of
maxOrd_comap_of_isPullback_specMap; it serves the change-of-fields clause of the marked functor
of [Kol07, Theorem 107]
(Hironaka/Resolution/Algebraic/MarkedOrderReduction/BaseChangeParameters.lean).
The maximal order under pull-back #
A smooth pull-back does not raise the maximal order: the order is preserved pointwise
(ord_comap_of_smooth). Not in the sources; an auxiliary lemma for [Kol07, 34.1].
A surjective morphism does not lower the maximal order: the order can only grow under
pull-back (ord_le_ord_comap) and every point has a preimage. Not in the sources.
A change of fields preserves the maximal order in characteristic zero: max-ord I ≤ μ iff the
iterated derivative D^μ I is the unit ideal, the derivative commutes with the base-change square
(derivativeIter_comap_of_isPullback_specMap), and the projection is surjective. Not in the
sources; an auxiliary lemma for [Kol07, 34.2].
A smooth blow-up sequence of order m without empty blow-ups ([Kol07, Definition 66 and 32])
for an ideal of maximal order < m is the empty sequence: its first centre, being nonempty, has a
generic point of a component (Closeds.exists_mem_genericPoints_specializes) at which the order
is m, above the maximal order. Not in the sources.
Congruence of the final maximal order along an equality of sequences (the index Fin.last _
depends on the sequence, so this is stated once and used in place of rw).
The reduced functor on an arbitrary class #
Above the mark, the reduced functor on C returns B on the tuned triple (Step 1 of the
proof of [Kol07, Theorem 103]).
Below the mark, the reduced functor on C returns the empty sequence (the remark after
[Kol07, Theorem 68]: the case max-ord I < m is trivial).
The value of the reduced functor on C is a smooth blow-up sequence of order m starting
with (X, I, E): the first proof field of ofTunedClass.
The value of the reduced functor on C contains no empty blow-up ([Kol07, 32]): the second
proof field of ofTunedClass.
Clause (1) of [Kol07, Theorem 103] for the reduced functor on a class C of triples with
max-ord I ≤ m (hmax), from clause (1) for B on the tuned triples.
Clause (2) of [Kol07, Theorem 103] for smooth morphisms ([Kol07, 34.1]): the reduced functor
on a class C of triples with max-ord I ≤ m commutes with smooth morphisms when B does. The
case splits align because the maximal order does not rise under a smooth pull-back and is
preserved by a surjection; in the one mixed case the pulled-back sequence, an order-m sequence
without empty centres for a triple below the mark, is empty.
Clause (2) of [Kol07, Theorem 103] for change of fields ([Kol07, 34.2]): the reduced functors
on a class C of triples over k with max-ord I ≤ m and on a class C' over L commute with a
change of fields when B and B' do. The maximal order is preserved under a change of fields in
characteristic zero, so the case splits align.
The reduced functor on BOClass n m #
Above the mark, the reduced functor returns B on the tuned triple.
Below the mark, the reduced functor returns the empty sequence.
The value of the reduced functor is a smooth blow-up sequence of order m starting with
(X, I, E): the first proof field of ofTuned.
The value of the reduced functor contains no empty blow-up ([Kol07, 32]): the second proof
field of ofTuned.
Clause (1) of [Kol07, Theorem 103] for the reduced functor, from clause (1) for B on the
tuned triples.
Clause (2) of [Kol07, Theorem 103] for smooth morphisms ([Kol07, 34.1]): the reduced functor
commutes with smooth morphisms when B does.
Clause (2) of [Kol07, Theorem 103] for change of fields ([Kol07, 34.2]): the reduced functors
over k and over L commute with a change of fields when B and B' do.
Along the projection p of a base-change square over a field extension σ : k → L, the order
of the inverse image of I at a point is the order of I at its image: for every μ ≥ 1,
ord_y (p^* I) ≥ μ iff y lies in the support of D^{μ-1}(p^* I) = p^*(D^{μ-1} I), iff
ord_{p y} I ≥ μ (the support of a marked ideal through iterated derivatives,
[Wlo05, Lemma 2.6.2]). The pointwise form of maxOrd_comap_of_isPullback_specMap.