Theorem 107 (3) at the mark 1: the marked order reduction of an ideal of order ≤ 1 #
Clause (3) of [Kol07, Theorem 107] says that the marked order reduction BMO_{n,m}(X, I, m, ∅)
is the order reduction BO_{n,m}(X, I, ∅) when m is the maximal order of I. This module
proves it for the library's three-step construction of BMO_{n,m} (bmoSeqOn, the chain of
[Kol07, 111]) at the mark 1 and for an ideal sheaf of order ≤ 1 with the empty boundary, the
case the commutation with closed embeddings uses ([Kol07, 108]: every local equation of the
submanifold lies in I, so the maximal order is 1):
- with the empty boundary the nonmonomial part of the ideal is the ideal itself
(
nonmonomialTriple_eq_self_of_isEmpty), so the bound of the rounds on the nonmonomial part isD ≤ 1, and at the thresholdt = m = 1the first step runsDlinks: none whenD = 0, one round ofBO_{n,1}whenD = 1; - after the first step the controlled transform of
(I, 1)has order< 1at every point of the last stage (descentState_ord_lt_one): with no link it is the restriction ofI, of order0; with one link it is the last marked transform of the round, of order< 1by [Kol07, Theorem 103 (1)], carried along the corestricted lift (induced_pullback); - the separation step has
t − 1 = 0links, and the monomial step is idle: the monomial part of an ideal of order< 1has order< 1(le_monomialPart,ord_anti), the value of the procedure is a sequence of order≥ 1for it without empty centres, hence empty (MonomialStep3Fam.seqOn_eq_nil), and a link with the empty value restricts the list (SState.step3Link_L_of_ord_lt); - the value of
BMO_{n,1}onUis therefore the value of the first step onU(bmoSeqOn_one_eq_stepAFamOn), which is the value ofBO_{n,1}onU(descentState_eraseEmpty_pullback_eq_bo_one: with no link both are empty; with one link the round read on the second chain open and restricted toUis the value onUby the commutation ofBO_{n,1}with the inclusion of the outer open and its compatibility under restriction, the argument ofcomposeOn_eq_of_firstList_eq_nil) —bmoSeqOn_one_eq_bo_one.
Consequence: the marked family of the library's tower at the mark 1 commutes with closed
embeddings of hypersurfaces of empty divisor through the marked family one dimension down
(concreteBMOanFam_commutesWithClosedEmbeddings_one, [Kol07, Claim 71.2] for hypersurfaces as
in [Kol07, 108]: Theorem 103 (3), BOanFamAllOf_commutesWithClosedEmbeddingsOfEmptyDivisorFam,
and Theorem 107 (3) above), and, by the chaining along flags
(BMOanFam_commutesWithClosedEmbeddingsOfEmptyDivisorFam_all), in every codimension
(concreteBMOanFam_commutesWithClosedEmbeddings).
The empty boundary #
With the empty boundary the nonmonomial triple is the triple itself: the monomial part of the
ideal is the unit ideal (monomialPart_eq_top_of_activeMembers_eq_empty, no member), so the
nonmonomial part is the ideal (nonmonomialTriple_I_eq_of_monomialPart_eq_top).
The order of the ideal of the nonmonomial triple of a triple with empty boundary is the order of the ideal.
The monomial step is idle on an ideal of order < 1 #
The empty-value lemma for the monomial procedure ([Kol07, Definition 66 (4′)] with
[Kol07, 32]): on an open where the monomial part of the ideal has order < m everywhere the value
of the procedure is the empty list, since a first centre would lie where that order is ≥ m and
be nonempty. The counterpart of BOanFam.seqOn_eq_nil.
The monomial link with an empty value restricts the list #
When the controlled transform of (𝓘, 1) at the exit state has order < 1 at every point, the
value of the monomial procedure is empty: the monomial part of the induced ideal contains it
(le_monomialPart), so has order < 1 too (ord_anti), and MonomialStep3Fam.seqOn_eq_nil.
A monomial link with an empty value restricts the list to V (shrinkAppend with the empty
list: pullback_nil, concat_nil_right).
The first step at the threshold 1 on an ideal of order ≤ 1: no link or one round #
With the empty boundary, the nonmonomial triple of the induced triple of the initial state (the triple restricted to the first chain open) is that triple itself.
After one round of BO_{n,1} from the initial state the controlled transform of (𝓘, 1) has
order < 1 at every point of the last stage: Theorem 103 (1) for the round (ord_lt), on the
triple restricted to the reading open, carried along the corestricted lift (induced_pullback)
and through the concatenation (pred_induced_concat), as in SState.step3Link_ord_lt.
The value of one round of BO_{n,1} from the initial state, restricted to U ⊆ V and
cleaned, is the value of BO_{n,1} on U: the round is the value of BO_{n,1} on the triple
restricted to W₀, read on the reading open, whose image under the inclusion of W₀ is V
(CommutesWithLocalIsos.seqOn_eq_of_image_eq); the pull-backs compose to the inclusion U ⊆ V,
and the compatibility of the family of BO_{n,1} closes (the argument of
composeOn_eq_of_firstList_eq_nil).
At the threshold 1 with a bound D ≤ 1, the controlled transform at the exit of the first
step has order < 1 everywhere: with D = 0 there is no link and the induced ideal is the
restriction of 𝓘, of order 0; with D = 1 there is one link,
inducedTriple_descentLink_initialOf_ord_lt.
At the threshold 1 with a bound D ≤ 1, the value of the first step on U is the value of
BO_{n,1} on U: with D = 0 both are empty (BOanFam.seqOn_eq_nil: ord 𝓘 = 0 on U); with
D = 1, descentLink_initialOf_eraseEmpty_pullback_eq.
Theorem 107 (3) at the mark 1 for the three-step construction #
With the empty boundary and ord 𝓘 ≤ 1, the bound of the rounds is at most 1.
After the first step at the threshold 1 the controlled transform of (𝓘, 1) has order < 1
at every point of the last stage.
The value of the first step on U at the threshold 1 is the value of BO_{n,1} on
U.
Theorem 107 (3) at the mark 1 ([Kol07, Theorem 107 (3)]: BMO_{n,m}(X, I, m, ∅) = BO_{n,m}(X, I, ∅) when m = max-ord I), for the three-step construction: on a triple with the
empty boundary and ord 𝓘 ≤ 1, the value of BMO_{n,1} on U is the value of BO_{n,1} on U.
The separation step has 1 − 1 = 0 links; the monomial link is idle since the controlled transform
already has order < 1 (stepAChainState_ord_lt_one, SState.step3Link_L_of_ord_lt); the terminal
list is the first step's list restricted, so the value is the first step's value
(stepAFamOn_one_eq_bo_one).
The concrete marked tower commutes with closed embeddings of empty divisor #
Theorem 107 (3) at the mark 1 for the library's tower: on a triple with the empty boundary and
ord 𝓘 ≤ 1, the value of concreteBMOanFam 𝕜 n is the value of concreteBOanFam 𝕜 n 1. In
dimension 0 both are the trivial functor.
[Kol07, Claim 71.2] for hypersurfaces ([Kol07, 108]): the marked family of the tower in
dimension n + 1 at the mark 1 commutes with closed embeddings of hypersurfaces of empty divisor
through the marked family in dimension n: the ideal 𝓘 ⊇ I_S has order ≤ 1
(ord_le_one_of_idealSheaf_le), so BMO_{n+1,1} agrees with BO_{n+1,1} on it
(concreteBMOanFam_seqOn_eq_concreteBOanFam_one, Theorem 107 (3)), and BO_{n+1,1} is the
push-forward of BMO_{n,1} (BOanFamAllOf_commutesWithClosedEmbeddingsOfEmptyDivisorFam,
Theorem 103 (3)).
[Kol07, Claim 71.2], [Kol07, Theorem 35 (5)] for the concrete marked tower: the marked order
reduction at the mark 1 in dimension n commutes with closed embeddings of empty divisor in every
codimension s, through the one in dimension n − s: the hypersurface case
(concreteBMOanFam_commutesWithClosedEmbeddings_one) chained along flags
(BMOanFam_commutesWithClosedEmbeddingsOfEmptyDivisorFam_all, [Kol07, 108]).