Per-stage clauses along a concatenation

BlowUpSequence.concat performs the blow-ups of S and then those of T : BlowUpSequence S.last. Hironaka's Main Theorem II(N) [Hir64, Main Theorem II(N)] is proved by concatenating rounds of order reduction, and its clauses (1)–(3) are statements about every stage i: the center B_i, the weak transform J_i and the boundary E_i. This module transports a per-stage predicate P (B_i, J_i, E_i) along cons and concat, the per-stage form of forall_center_concat and isOrderSeq_concat of Hironaka/Scheme/BlowUpSequence/ConcatApi.lean, by induction on the first sequence, and the last-stage clauses (4) of Main Theorem II(N) along weakTransformSeq_concat_last and boundarySeq_concat_last (the identification eqToHom (last_concat S T) of the end results changes nothing).

theorem AlgebraicGeometry.Scheme.BlowUpSequence.forall_stage_cons_iff {X : Scheme} (P : {Y : Scheme} → Y.IdealSheafData → Y.IdealSheafData → Y.IdealSheafData → Prop) (D : X.IdealSheafData) (rest : D.blowUp.BlowUpSequence) (J E : X.IdealSheafData) : (∀ (i : Fin (cons X D rest).length), P ((cons X D rest).center i) ((cons X D rest).weakTransformSeq J i.castSucc) ((cons X D rest).boundarySeq E i.castSucc)) ↔ P D J E ∧ ∀ (j : Fin rest.length), P (rest.center j) (rest.weakTransformSeq (J.weakTransform D) j.castSucc) (rest.boundarySeq (E.reducedTransform D) j.castSucc)

A per-stage predicate P (D_i, J_i, E_i) along a cons: at stage 0 the data (D, J, E) of the first blow-up, at the later stages the tail's data started at the transforms (weakTransform D J, reducedTransform D E).

theorem AlgebraicGeometry.Scheme.BlowUpSequence.forall_stage_concat {X : Scheme} (P : {Y : Scheme} → Y.IdealSheafData → Y.IdealSheafData → Y.IdealSheafData → Prop) (S : X.BlowUpSequence) (T : S.last.BlowUpSequence) (J E : X.IdealSheafData) (hS : ∀ (i : Fin S.length), P (S.center i) (S.weakTransformSeq J i.castSucc) (S.boundarySeq E i.castSucc)) (hT : ∀ (j : Fin T.length), P (T.center j) (T.weakTransformSeq (S.weakTransformSeq J (Fin.last S.length)) j.castSucc) (T.boundarySeq (S.boundarySeq E (Fin.last S.length)) j.castSucc)) (i : Fin (S.concat T).length) : P ((S.concat T).center i) ((S.concat T).weakTransformSeq J i.castSucc) ((S.concat T).boundarySeq E i.castSucc)

A per-stage predicate holding at every stage of S (data started at (J, E)) and at every stage of T (data started at the last transforms of S) holds at every stage of S.concat T; the per-stage form of forall_center_concat.

theorem AlgebraicGeometry.Scheme.IdealSheafData.IsSncBoundary.comap_eqToHom {Y Z : Scheme} (h : Y = Z) {I : Z.IdealSheafData} (hI : I.IsSncBoundary) : (I.comap (CategoryTheory.eqToHom h)).IsSncBoundary

Having only normal crossings [Hir64, Definition 2] is unchanged by the inverse image along the identification of two equal schemes.

theorem AlgebraicGeometry.Scheme.BlowUpSequence.isSncBoundary_boundarySeq_concat_last {X : Scheme} (S : X.BlowUpSequence) (T : S.last.BlowUpSequence) (E₀ : X.IdealSheafData) (h : (T.boundarySeq (S.boundarySeq E₀ (Fin.last S.length)) (Fin.last T.length)).IsSncBoundary) : ((S.concat T).boundarySeq E₀ (Fin.last (S.concat T).length)).IsSncBoundary

The first part of clause (4) of [Hir64, Main Theorem II(N)] along a concatenation: the last boundary of S.concat T has only normal crossings if the last boundary of T, started at the last boundary of S, has.

theorem AlgebraicGeometry.Scheme.BlowUpSequence.weakTransformSeq_concat_last_eq_top {X : Scheme} (S : X.BlowUpSequence) (T : S.last.BlowUpSequence) (J : X.IdealSheafData) (h : T.weakTransformSeq (S.weakTransformSeq J (Fin.last S.length)) (Fin.last T.length) = ⊤) : (S.concat T).weakTransformSeq J (Fin.last (S.concat T).length) = ⊤

The second part of clause (4) of [Hir64, Main Theorem II(N)] along a concatenation: the last weak transform of S.concat T is the unit ideal if that of T, started at the last weak transform of S, is.