CP3 across the deletion of empty blow-ups and along a cover

Two more transports of the universal form CP3For of the statement CP3 of the embedded desingularization (Hironaka.Resolution.Algebraic.Wlo05.EmbeddedChainRelative, Hironaka.Resolution.Algebraic.Wlo05.EmbeddedCP3Predicates): the convention of [Kol07, 34.1] deletes the blow-ups with empty centre, and [Kol07, Theorem 105] builds the functor of the algorithm on a coproduct of open immersions covering the triple. CP1 has both transports (cp1For_eraseEmpty, cp1For_of_pullback_cover); here they are proved for CP3.

• cp3For_eraseEmpty — by structural induction on the sequence, as IsOrderGeSeq.eraseEmpty: cp3For_cons_iff splits the first centre from the tail; a non-empty first centre is kept; an empty one is deleted and the tail carried back along the inverse of the trivial blow-up (cp3For_pullback_of_isIso, the stalk-isomorphism transport at every stage, with the marked-transform identity of [Kol07, Lemma 62] under the order hypothesis, which is why the statement carries the order-sequence binders as cp1For_eraseEmpty does), the mark-1 transform along the trivial blow-up being the pull-back (markedTransform_top_left) and the induced family the original one extended by an empty member (extendsByEmpty_totalTransform_top_comap_inv), which the classification ignores (cp3For_iff_of_extendsByEmpty, through centerClassifiedAt_iff_of_embeds).
• cp3For_of_pullback_cover — a point of a centre lifts to the pulled-back run (surjective_pullbackStageHom), where the centre, the marked transform ([Kol07, Lemma 62] under the order hypothesis) and the total transform are the pull-backs of the data of the run along the stage lift, whose stalk map is an isomorphism (openImmersionCoprods_pullbackStageHom); the classification descends (centerClassifiedAt_comap_of_isIso_stalkMap).

These transports are not in the literature. Used in Hironaka.Resolution.Algebraic.Wlo05.EmbeddedCP3Step21, Hironaka.Resolution.Algebraic.Wlo05.EmbeddedCP3Step22, Hironaka.Resolution.Algebraic.Wlo05.EmbeddedCP3Tower and Hironaka.Resolution.Algebraic.Wlo05.EmbeddedCP5.

theorem Hironaka.Resolution.cp3For_cons_iff {X : AlgebraicGeometry.Scheme} (D : X.IdealSheafData) (rest : D.blowUp.BlowUpSequence) (I : X.IdealSheafData) (E : X.DivisorFamily) : CP3For (AlgebraicGeometry.Scheme.BlowUpSequence.cons X D rest) I E ↔ (∀ q ∈ D.support, CenterClassifiedAt E I D q) ∧ CP3For rest (I.markedTransform D 1) (E.totalTransform D)

CP3For on a cons: the first centre classified at each of its points for the starting data, and CP3For for the tail with the transformed data.

theorem Hironaka.Resolution.cp3For_pullback_of_isIso {k : Type u} [Field k] [CharZero k] {X Y : AlgebraicGeometry.Scheme} (f : X ⟶ AlgebraicGeometry.Spec ↧k) (n : ℕ) [AlgebraicGeometry.SmoothOfRelativeDimension n f] (S : X.BlowUpSequence) (φ : Y ⟶ X) [CategoryTheory.IsIso φ] (I : X.IdealSheafData) (E : X.DivisorFamily) (hS : S.IsOrderGeSeq f I 1 E) (h : CP3For S I E) : CP3For (S.pullback φ) (I.comap φ) (E.comap φ)

CP3For pulls back along an isomorphism of the ambient scheme ([Kol07, Lemma 62] for the marked transform).

theorem Hironaka.Resolution.extendsByEmpty_totalTransformSeq {X : AlgebraicGeometry.Scheme} (S : X.BlowUpSequence) {E₁ E₂ : X.DivisorFamily} : AlgebraicGeometry.ExtendsByEmpty E₁ E₂ → ∀ (i : Fin (S.length + 1)), AlgebraicGeometry.ExtendsByEmpty (S.totalTransformSeq E₁ i) (S.totalTransformSeq E₂ i)

An extension by empty components persists along the total transforms of a sequence.

theorem Hironaka.Resolution.centerClassifiedAt_iff_of_extendsByEmpty {X : AlgebraicGeometry.Scheme} {E₁ E₂ : X.DivisorFamily} (hext : AlgebraicGeometry.ExtendsByEmpty E₁ E₂) (K Z : X.IdealSheafData) (q : ↥X) : CenterClassifiedAt E₁ K Z q ↔ CenterClassifiedAt E₂ K Z q

The classification sees a family only through its non-empty members.

theorem Hironaka.Resolution.cp3For_iff_of_extendsByEmpty {X : AlgebraicGeometry.Scheme} (S : X.BlowUpSequence) (I : X.IdealSheafData) {E₁ E₂ : X.DivisorFamily} (hext : AlgebraicGeometry.ExtendsByEmpty E₁ E₂) : CP3For S I E₁ ↔ CP3For S I E₂

CP3For sees a family only through its non-empty members.

theorem Hironaka.Resolution.cp3For_eraseEmpty {k : Type u} [Field k] [CharZero k] {X : AlgebraicGeometry.Scheme} (f : X ⟶ AlgebraicGeometry.Spec ↧k) (n : ℕ) [AlgebraicGeometry.SmoothOfRelativeDimension n f] (S : X.BlowUpSequence) (I : X.IdealSheafData) (E : X.DivisorFamily) (hS : S.IsOrderGeSeq f I 1 E) (h : CP3For S I E) : CP3For S.eraseEmpty I E

CP3 passes to the erased run (the deletion of empty blow-ups of [Kol07, 34.1]; the counterpart of cp1For_eraseEmpty).

theorem Hironaka.Resolution.cp3For_of_pullback_cover {k : Type u} [Field k] [CharZero k] (T T' : AlgebraicGeometry.Triple k) (g : T'.X.left ⟶ T.X.left) (hg : AlgebraicGeometry.openImmersionCoprods g) (hsurj : Function.Surjective ⇑g) (hpb : T'.IsPullbackOf T g) (S : T.X.left.BlowUpSequence) (hS : S.IsOrderGeSeq (T.X.left ↘ AlgebraicGeometry.Spec ↧k) T.I 1 T.E) (h : CP3For (S.pullback g) T'.I T'.E) : CP3For S T.I T.E

CP3 descends along a coproduct of open immersions covering the triple ([Kol07, Theorem 105]; the counterpart of cp1For_of_pullback_cover).