The globalised order-reduction functor is indifferent to empty boundary members

Kollár's convention [Kol07, 32] and the reindexing of [Kol07, 34.1] for the order-reduction functor BO_{n,m} of [Kol07, Theorem 103] (Hironaka.BO.functor, the descent of the maximal-contact case along the local covers of Step 3 of the proof): deleting unit-ideal members of the boundary does not change its value. The identity is local. Both values pull back along the surjective open-immersion coproduct g : X^* → X of a local cover (the same cover for both boundaries: the inverse image keeps the index set, and the local class does not read the boundary) to the values of the local functor (functor_seq_pullback_localCover), which are the maximal-contact case maxContactCase for a common smooth hypersurface of maximal contact (localFunctor_seq); these agree by maxContactCase_indifferentToEmptyMembers of Hironaka/Resolution/Algebraic/OrderReduction/EmptyIndifferentStep2.lean, the deletion being pulled back along g (IsTopErasure.comap); and pulling back along a surjective flat morphism is injective on blow-up sequences (pullback_injective_of_surjective). The empty scheme is the degenerate case, where every value is nil.

• functor_indifferentToEmptyMembers: the statement for Hironaka.BO.functor n m bd, under the two hypotheses on the boundary-clearing data of [Kol07, Lemma 102] at every mark, indifference to empty members (hind) and vanishing at a unit member (hnil).
• data_indifferentToEmptyMembers: the statement for the functor of Hironaka.BO.data, where the two hypotheses are discharged by Hironaka.BD.bdData_indifferentToEmptyMembers and Hironaka.BD.bdData_nilAtUnitMember, so that the conclusion holds under the indifference of the inductive input alone. This is the form used for the marked functor of [Kol07, Theorem 107] (Hironaka/Resolution/Algebraic/MarkedOrderReduction/Theorem107.lean).

theorem Hironaka.Sequence.IsTopErasure.of_eq {X : AlgebraicGeometry.Scheme} {E' E₁ E₂ : X.DivisorFamily} {e : E'.ι ↪o E₁.ι} (h : IsTopErasure E' E₁ e) (hEq : E₂ = E₁) : ∃ (e₂ : E'.ι ↪o E₂.ι), IsTopErasure E' E₂ e₂

A deletion of unit members with target E₁ is one with target any family equal to E₁, the embedding transported along the equality.

theorem Hironaka.BO.functor_indifferentToEmptyMembers (n m : ℕ) (bd : (m j : ℕ) → BDData n m j) (hind : ∀ (m : ℕ), BDFamily.IndifferentToEmptyMembers (bd m)) (hnil : ∀ (m : ℕ), BDFamily.NilAtUnitMember (bd m)) (k : Type u) [Field k] [CharZero k] : (functor n m bd).IndifferentToEmptyMembers

BO_{n,m} is indifferent to empty boundary members ([Kol07, 32] and the reindexing of [Kol07, 34.1] for the functor of [Kol07, Theorem 103]), over every field of characteristic zero, under the hypotheses that the boundary-clearing data of [Kol07, Lemma 102] at every mark are indifferent to empty members (hind) and nil at a unit member (hnil). By descent along a local cover, the identity on the pieces being maxContactCase_indifferentToEmptyMembers.

theorem Hironaka.BO.data_indifferentToEmptyMembers (n m : ℕ) (Dom : (k : Type u) → [inst : Field k] → [CharZero k] → MarkedTriple k → Prop) (B : (k : Type u) → [inst : Field k] → [inst_1 : CharZero k] → OrderGeSeqAssignment k (Dom k)) (hDom : ∀ (m : ℕ) (k : Type u) [inst : Field k] [inst_1 : CharZero k] (T' : MarkedTriple k), T'.HasDimLE (n - 1) → T'.m = IsLocalRing.tuningParam m → Dom k T') (hB : ∀ (k : Type u) [inst : Field k] [inst_1 : CharZero k] (T' : MarkedTriple k) (hT' : Dom k T'), ((B k).endTriple T' hT').I.maxOrd < ↑T'.m) (hsm : ∀ (k : Type u) [inst : Field k] [inst_1 : CharZero k], (B k).CommutesWithSmooth) (hbc : ∀ (k L : Type u) [inst : Field k] [inst_1 : CharZero k] [inst_2 : Field L] [inst_3 : CharZero L] (σ : k →+* L), (B k).CommutesWithBaseChange (B L) σ) (hBind : ∀ (k : Type u) [inst : Field k] [inst_1 : CharZero k], (B k).IndifferentToEmptyMembers) (k : Type u) [Field k] [CharZero k] : ((data n m Dom B hDom hB hsm hbc hBind).functor k).IndifferentToEmptyMembers

The functor of Hironaka.BO.data is indifferent to empty boundary members ([Kol07, 32] for the functor of [Kol07, Theorem 103]) under the indifference hBind of the inductive input alone: functor_indifferentToEmptyMembers at the boundary-clearing data Hironaka.BD.bdData, whose two hypotheses are Hironaka.BD.bdData_indifferentToEmptyMembers and Hironaka.BD.bdData_nilAtUnitMember.