The geometric Step 3 under an arbitrary smooth morphism, up to unit members

The second clause of [Kol07, 34.1] for Step 3 of the proof of [Kol07, Theorem 107], on a marked triple T' that is the pull-back of T up to unit boundary members: the geometric Step 3 of T' is the pull-back of the geometric Step 3 of T with the empty blow-ups deleted. Two facts combine:

• realize_pullback_eraseEmpty (Hironaka/Resolution/Algebraic/Monomial/Geometric/PullbackErase.lean): for the full pull-back family h^{-1} E, the run on the refining family refinesAlong_ofDivisorFamily is the erased pull-back of the run on X; the exponents agree with Step 3's exponents at the generic points of the components (exponentAt_step3Family_of_mem_genericPoints, ord_comap_of_smooth), and the enumeration of the components is Step 3's own on T' transported by compEquivOfIsTopErasure;
• realize_congr_of_rel (Hironaka/Resolution/Algebraic/Monomial/Geometric/RealizeCongr.lean): Step 3's input family on T' (boundary E') and the family on the full pull-back boundary h^{-1} E are related by a renumbering, since the components are the same (a unit member has no irreducible components, compEquivOfIsTopErasure), the pieces and exponents coincide, and the labels are re-embedded along the order embedding E'.ι ↪o E.ι (rel_ofDivisorFamily_of_isTopErasure).

The result step3Seq_eraseEmpty_pullback enters the assembly of clause (2) in Hironaka/Resolution/Algebraic/MarkedOrderReduction/Smooth.lean.

noncomputable def Hironaka.Monomial.compEquivOfIsTopErasure {X : AlgebraicGeometry.Scheme} {E' E : X.DivisorFamily} {e : E'.ι ↪o E.ι} (he : Sequence.IsTopErasure E' E e) : PieceFamily.Components E' ≃ PieceFamily.Components E

The irreducible components of the members of a family with unit members deleted are those of the family ([Kol07, 32]): a unit member has empty support, hence no generic point.

Equations

• Hironaka.Monomial.compEquivOfIsTopErasure he = Equiv.ofBijective (fun (c : Hironaka.Monomial.PieceFamily.Components E') => ⟨e c.fst, ⟨↑c.snd, ⋯⟩⟩) ⋯

theorem Hironaka.Monomial.compEquivOfIsTopErasure_fst {X : AlgebraicGeometry.Scheme} {E' E : X.DivisorFamily} {e : E'.ι ↪o E.ι} (he : Sequence.IsTopErasure E' E e) (c : PieceFamily.Components E') : ((compEquivOfIsTopErasure he) c).fst = e c.fst

theorem Hironaka.Monomial.compEquivOfIsTopErasure_snd {X : AlgebraicGeometry.Scheme} {E' E : X.DivisorFamily} {e : E'.ι ↪o E.ι} (he : Sequence.IsTopErasure E' E e) (c : PieceFamily.Components E') : ↑((compEquivOfIsTopErasure he) c).snd = ↑c.snd

noncomputable def Hironaka.Monomial.PieceFamily.labelMapOfIsTopErasure {X : AlgebraicGeometry.Scheme} {E' E : X.DivisorFamily} (e : E'.ι ↪o E.ι) {L L' : ℕ} (f' : E'.ι ≃o Fin L') (f : E.ι ≃o Fin L) (ℓ : ℕ) : ℕ

The label renumbering of a deletion of unit members: the label of a member of E' (through f') goes to the label of the same member in E (through f, along e).

Equations

• Hironaka.Monomial.PieceFamily.labelMapOfIsTopErasure e f' f ℓ = if hℓ : ℓ < L' then ↑(f (e (f'.symm ⟨ℓ, hℓ⟩))) else ℓ

theorem Hironaka.Monomial.PieceFamily.labelMapOfIsTopErasure_apply {X : AlgebraicGeometry.Scheme} {E' E : X.DivisorFamily} (e : E'.ι ↪o E.ι) {L L' : ℕ} (f' : E'.ι ≃o Fin L') (f : E.ι ≃o Fin L) (i : E'.ι) : labelMapOfIsTopErasure e f' f ↑(f' i) = ↑(f (e i))

theorem Hironaka.Monomial.PieceFamily.rel_ofDivisorFamily_of_isTopErasure {X : AlgebraicGeometry.Scheme} {E' E : X.DivisorFamily} {e : E'.ι ↪o E.ι} (he : Sequence.IsTopErasure E' E e) (a : ↥X → ℕ) {k : ℕ} (σ : Fin k ≃ Components E') {L L' : ℕ} (f' : E'.ι ≃o Fin L') (f : E.ι ≃o Fin L) : (ofDivisorFamily E' a f' σ).Rel id (labelMapOfIsTopErasure e f' f) (ofDivisorFamily E a f (σ.trans (compEquivOfIsTopErasure he)))

Step 3's input family for a boundary with unit members deleted is the input family for the full boundary, renumbered: the same components (enumerated through compEquivOfIsTopErasure), the same pieces and exponents, the labels re-embedded along e.

theorem Hironaka.BMO.step3Seq_eraseEmpty_pullback {k : Type u} [Field k] [CharZero k] {n m : ℕ} (T T' : MarkedTriple k) (h : T'.X.left ⟶ T.X.left) [AlgebraicGeometry.Smooth h] (hp : T'.IsPullbackOfUpToUnits T h) (hT : MarkedTriple.BMOClass n m T) (hT' : MarkedTriple.BMOClass n m T') : step3Seq T' hT' = ((step3Seq T hT).pullback h).eraseEmpty

The geometric Step 3 of a marked triple that is a pull-back up to unit members is the pull-back of the geometric Step 3 with the empty blow-ups deleted (the second clause of [Kol07, 34.1] for Step 3; realize_pullback_eraseEmpty with refinesAlong_ofDivisorFamily and realize_congr_of_rel): Step 3's family on T' is, up to the renumbering of the labels along the deletion (rel_ofDivisorFamily_of_isTopErasure), the family on the full pull-back boundary, which is the refining family up to the exponents (they agree at the generic points of the components).