Deleting unit members of the boundary: the exceptional family and the positions

A member of the boundary equal to the unit ideal is invisible: the empty blow-up convention [Kol07, 32] and the reindexing in the second clause of [Kol07, 34.1]. IsTopErasure E' E e (Hironaka/Resolution/Algebraic/Kol07/EraseEmptyEmbedding.lean) names the relation "E' is E with unit members deleted along the order embedding e". This module proves what the boundary-clearing rounds of the proof of Theorem 103 [Kol07, 104, Steps 2.1 and 2.2] (one round per member of the boundary, then the restriction to the hypersurface with the exceptional sub-family F_r) need about it:

• strictTransformSeq_top: the strict transform of the unit ideal along any sequence is the unit ideal (strictTransform_top_right iterated), so a deleted member's transform is ⊤ at every stage;
• exists_isTopErasure_totalTransformSeq_exceptional: the deletion induced at the end of a sequence (exists_isTopErasure_totalTransformSeq) sends the exceptional indices, those not of the form originalIdx, onto the exceptional indices; hence exists_orderEmbedding_exceptionalFamily: the exceptional sub-families of the two boundaries are the same family up to a surjective order embedding matching the members;
• card_subtype_lt_eq_symm_monoEquivOfFin: in a finite linear order the number of elements below x is the position of x in the enumeration monoEquivOfFin, used to count the surviving positions below a given one;
• eraseEmpty_cons_nil_eq_nil, concat_eq_of_eq_nil: a one-step sequence with an empty center erases to the empty sequence; concatenating the empty sequence changes nothing.

The unit ideal along a sequence, the empty center, the empty tail

theorem Hironaka.Sequence.strictTransformSeq_top {X : AlgebraicGeometry.Scheme} (S : X.BlowUpSequence) (i : Fin (S.length + 1)) : S.strictTransformSeq ⊤ i = ⊤

The strict transform of the unit ideal along a blow-up sequence is the unit ideal at every stage (strictTransform_top_right iterated).

theorem Hironaka.Sequence.eraseEmpty_cons_nil_eq_nil {X : AlgebraicGeometry.Scheme} (D : X.IdealSheafData) (hD : D = ⊤) : (AlgebraicGeometry.Scheme.BlowUpSequence.cons X D (AlgebraicGeometry.Scheme.BlowUpSequence.nil D.blowUp)).eraseEmpty = AlgebraicGeometry.Scheme.BlowUpSequence.nil X

A one-step sequence whose center is the unit ideal (the empty blow-up) erases to the empty sequence [Kol07, 32].

theorem Hironaka.Sequence.concat_nil_right {X : AlgebraicGeometry.Scheme} (S : X.BlowUpSequence) : S.concat (AlgebraicGeometry.Scheme.BlowUpSequence.nil S.last) = S

Concatenating the empty sequence does not change a sequence (the empty sequence is a right unit for concat).

theorem Hironaka.Sequence.concat_eq_of_eq_nil {X : AlgebraicGeometry.Scheme} (S : X.BlowUpSequence) {R : S.last.BlowUpSequence} (hR : R = AlgebraicGeometry.Scheme.BlowUpSequence.nil S.last) : S.concat R = S

Concatenating a tail equal to the empty sequence does not change a sequence (the form used when the tail is a functor's value).

Counting positions in a finite linear order

theorem Hironaka.Sequence.card_subtype_lt_eq_symm_monoEquivOfFin (α : Type u_1) [Fintype α] [LinearOrder α] (x : α) : Fintype.card { a : α // a < x } = ↑((monoEquivOfFin α ⋯).symm x)

In a finite linear order the number of elements strictly below x is the position of x in the enumeration monoEquivOfFin; this is how the reindexing of [Kol07, 34.1] is counted.

theorem Hironaka.Sequence.card_subtype_le_eq_symm_monoEquivOfFin (α : Type u_1) [Fintype α] [LinearOrder α] (x : α) : Fintype.card { a : α // a ≤ x } = ↑((monoEquivOfFin α ⋯).symm x) + 1

The number of elements at most x is the position of x plus one.

The deletion at the end of a sequence sends exceptional indices onto exceptional indices

theorem Hironaka.Sequence.exists_isTopErasure_totalTransformSeq_exceptional {X : AlgebraicGeometry.Scheme} (S : X.BlowUpSequence) (E' E : X.DivisorFamily) (e : E'.ι ↪o E.ι) (_he : IsTopErasure E' E e) : ∃ (e' : (S.totalTransformSeq E' (Fin.last S.length)).ι ↪o (S.totalTransformSeq E (Fin.last S.length)).ι), IsTopErasure (S.totalTransformSeq E' (Fin.last S.length)) (S.totalTransformSeq E (Fin.last S.length)) e' ∧ (∀ (a : E'.ι), e' (S.originalIdx E' (Fin.last S.length) a) = S.originalIdx E (Fin.last S.length) (e a)) ∧ (∀ (b : (S.totalTransformSeq E (Fin.last S.length)).ι), (∀ (a : E.ι), b ≠ S.originalIdx E (Fin.last S.length) a) → ∃ (b' : (S.totalTransformSeq E' (Fin.last S.length)).ι), e' b' = b) ∧ ∀ (b' : (S.totalTransformSeq E' (Fin.last S.length)).ι) (a : E.ι), e' b' = S.originalIdx E (Fin.last S.length) a → ∃ (a' : E'.ι), b' = S.originalIdx E' (Fin.last S.length) a'

A deletion of unit members of the starting family induces a deletion between the families at the end of any sequence which carries the transforms of the original members to the transforms of the original members, hits every index that is not the transform of an original member, and sends an index onto the transform of an original member only if it is one (exists_isTopErasure_totalTransformSeq with the exceptional indices tracked).

theorem Hironaka.Sequence.exists_orderEmbedding_exceptionalFamily {X : AlgebraicGeometry.Scheme} (S : X.BlowUpSequence) (E' E : X.DivisorFamily) (e : E'.ι ↪o E.ι) (he : IsTopErasure E' E e) : ∃ (g : (S.exceptionalFamily E').ι ↪o (S.exceptionalFamily E).ι), Function.Surjective ⇑g ∧ ∀ (b : (S.exceptionalFamily E').ι), (S.exceptionalFamily E).component (g b) = (S.exceptionalFamily E').component b

Deleting unit members of the starting family does not change the exceptional sub-family at the end of a sequence: the two exceptional sub-families are matched by a surjective order embedding with equal members [Kol07, 32 and 34.1].