The pull-back of the realised Step 3 along a smooth surjection

For a smooth h : Y ⟶ X and a piece family Φ' of Y refining Φ along h (Hironaka/Resolution/Algebraic/Monomial/Geometric/Refinement.lean), the geometric Step 3 on Y is the pull-back of the geometric Step 3 on X: the first clause of [Kol07, 34.1], "B commutes with every smooth surjection", for the third step of BMO_{n,m}. The centres of the two runs correspond step by step, Kollár's choice on Y being the ρ-preimage of the choice on X (Refines.choice_eq of Hironaka/Resolution/Algebraic/Monomial/Restrict/Refine.lean), and

• centerOf_eq_comap: the centre of the preimage faces is the pull-back of the centre. At a point y over x ∈ Z_P the unique face of Y's centre through y maps onto P, and a child's reduced stalk is the pulled-back parent's (stalkIdeal_vanishingIdeal_piece on both sides). This is the statement of [Kol07, 30.1] that the centres of a pulled-back blow-up sequence are the preimages of the centres, here for the centres of Step 3;

so that the two blow-ups are the same blow-up of Y, and the transported families refine again along the induced morphism of blow-ups (blowUpPieces_refinesAlong, the geometric counterpart of Refines.blowUp). The fold realizeAux_pullback_of_surjective is then one induction along the run on X, and realize_pullback_of_surjective is the statement for realize. Not in the sources beyond Kollár's one sentence. The general case, h not surjective, is Hironaka/Resolution/Algebraic/Monomial/Geometric/PullbackErase.lean; the result is used in Hironaka/Resolution/Algebraic/MarkedOrderReduction/Step3Functorial.lean and, through Hironaka/Resolution/Algebraic/MarkedOrderReduction/SmoothStep3.lean, in the smooth functoriality of BMO_{n,m}.

Members of children and parents

theorem Hironaka.Monomial.PieceFamily.component_comap_memberOf {X Y : AlgebraicGeometry.Scheme} {Φ : PieceFamily X} {h : Y ⟶ X} {ρ : ℕ → ℕ} {Φ' : PieceFamily Y} {E : X.DivisorFamily} {e : E.ι ≃o Fin Φ.nextLabel} (hρ : Φ'.RefinesAlong h ρ Φ) (c' : ℕ) (hc' : c' < Φ'.nextComp) : (E.comap h).component (Φ'.memberOf (e.trans (Fin.castOrderIso ⋯)) c' hc') = (E.component (Φ.memberOf e (ρ c') ⋯)).comap h

The member of a child is the pull-back of the member of its parent, and so its E'-component (E' = E.comap h) is the pull-back of the parent's E-component: the label-matching hypothesis of the general fold in the pulled-back case.

theorem Hironaka.Monomial.PieceFamily.stalkIdeal_vanishingIdeal_piece_comap {X Y : AlgebraicGeometry.Scheme} {Φ : PieceFamily X} {h : Y ⟶ X} {ρ : ℕ → ℕ} {Φ' : PieceFamily Y} {E : X.DivisorFamily} {e : E.ι ≃o Fin Φ.nextLabel} {E' : Y.DivisorFamily} {e' : E'.ι ≃o Fin Φ'.nextLabel} (hE : E.IsSnc) (hΦ : Φ.Realizes E e) (hE' : E'.IsSnc) (hρ : Φ'.RefinesAlongW h ρ Φ) (hΦ' : Φ'.Realizes E' e') (hlab : ∀ (c' : ℕ) (hc' : c' < Φ'.nextComp), E'.component (Φ'.memberOf e' c' hc') = (E.component (Φ.memberOf e (ρ c') ⋯)).comap h) {c' : ℕ} (hc' : c' < Φ'.nextComp) {y : ↥Y} (hy : y ∈ Φ'.piece c') : (AlgebraicGeometry.Scheme.IdealSheafData.vanishingIdeal (Φ'.piece c')).stalkIdeal y = Ideal.map (CommRingCat.Hom.hom (AlgebraicGeometry.Scheme.Hom.stalkMap h y)) ((AlgebraicGeometry.Scheme.IdealSheafData.vanishingIdeal (Φ.piece (ρ c'))).stalkIdeal (h y))

The reduced stalk of a child at a point is the pull-back of the reduced stalk of its parent.

The center of the preimage faces is the pull-back of the center

theorem Hironaka.Monomial.PieceFamily.centerOf_eq_comap {X Y : AlgebraicGeometry.Scheme} {Φ : PieceFamily X} {h : Y ⟶ X} {ρ : ℕ → ℕ} {Φ' : PieceFamily Y} {E : X.DivisorFamily} {e : E.ι ≃o Fin Φ.nextLabel} {E' : Y.DivisorFamily} {e' : E'.ι ≃o Fin Φ'.nextLabel} {n m : ℕ} (hE : E.IsSnc) (hΦ : Φ.Realizes E e) (hE' : E'.IsSnc) (hρ : Φ'.RefinesAlongW h ρ Φ) (hΦ' : Φ'.Realizes E' e') (hlab : ∀ (c' : ℕ) (hc' : c' < Φ'.nextComp), E'.component (Φ'.memberOf e' c' hc') = (E.component (Φ.memberOf e (ρ c') ⋯)).comap h) {hV : Φ.IsValid n m} {S : Finset (Finset ℕ)} (hS : (Φ.toState n m hV).IsCenter S) {hV' : Φ'.IsValid n m} {S' : Finset (Finset ℕ)} (hS' : (Φ'.toState n m hV').IsCenter S') (hS'S : ∀ Q ∈ S', Finset.image ρ Q ∈ S) (hlift : ∀ P ∈ S, ∀ (y : ↥Y), h y ∈ Φ.faceSet P → ∃ Q ∈ S', y ∈ Φ'.faceSet Q) : Φ'.centerOf S' = (Φ.centerOf S).comap h

The centre of the faces of Y mapping into a centre S of X is the pull-back of the centre of S, provided every point over a face of S lies on a face of the Y-centre ([Kol07, 30.1]: the centres of the pull-back are the inverse images of the centres). At a point y over x ∈ Z_P the unique face of the Y-centre through y maps onto P (the faces of a centre are pairwise disjoint), the two centres have the stalks of the ideals of these faces, and a child's reduced stalk is the pulled-back parent's.

The transported families refine again

theorem Hironaka.Monomial.PieceFamily.RefinesAlongW.total_image {X Y : AlgebraicGeometry.Scheme} {Φ : PieceFamily X} {h : Y ⟶ X} {ρ : ℕ → ℕ} {Φ' : PieceFamily Y} (hρ : Φ'.RefinesAlongW h ρ Φ) {Q : Finset ℕ} (hQ : Q ∈ Φ'.nerve) : Φ.total (Finset.image ρ Q) = Φ'.total Q

The exponent sum of a face is preserved by the parent map.

theorem Hironaka.Monomial.PieceFamily.strictTransform_comap_eqToHom {Y : AlgebraicGeometry.Scheme} {D D' : Y.IdealSheafData} (e : D' = D) (J : Y.IdealSheafData) : (J.strictTransform D).comap (CategoryTheory.eqToHom ⋯) = J.strictTransform D'

Transport of a strict transform along an equality of centers.

theorem Hironaka.Monomial.PieceFamily.exceptionalDivisor_comap_eqToHom {Y : AlgebraicGeometry.Scheme} {D D' : Y.IdealSheafData} (e : D' = D) : D.exceptionalDivisor.comap (CategoryTheory.eqToHom ⋯) = D'.exceptionalDivisor

Transport of the exceptional divisor along an equality of centers.

theorem Hironaka.Monomial.PieceFamily.blowUpPieces_refinesAlongW {X Y : AlgebraicGeometry.Scheme} {Φ : PieceFamily X} {h : Y ⟶ X} {ρ : ℕ → ℕ} {Φ' : PieceFamily Y} {n m : ℕ} {k k' : Type u} [Field k] [Field k'] (f : X ⟶ AlgebraicGeometry.Spec ↧k) [AlgebraicGeometry.LocallyOfFiniteType f] (g : Y ⟶ AlgebraicGeometry.Spec ↧k') [AlgebraicGeometry.LocallyOfFiniteType g] [AlgebraicGeometry.Flat h] (hρ : Φ'.RefinesAlongW h ρ Φ) {hV : Φ.IsValid n m} {S : Finset (Finset ℕ)} (hS : (Φ.toState n m hV).IsCenter S) {hV' : Φ'.IsValid n m} {S' : Finset (Finset ℕ)} (hS' : (Φ'.toState n m hV').IsCenter S') (hS'S : ∀ Q ∈ S', Finset.image ρ Q ∈ S) (hlift : ∀ P ∈ S, ∀ (y : ↥Y), h y ∈ Φ.faceSet P → ∃ Q ∈ S', y ∈ Φ'.faceSet Q) (hc : Φ'.centerOf S' = (Φ.centerOf S).comap h) : (Φ'.blowUpPieces S' m).RefinesAlongW (CategoryTheory.CategoryStruct.comp (CategoryTheory.eqToHom ⋯) (AlgebraicGeometry.Scheme.Hom.blowUpMap h (Φ.centerOf S))) (MonomialState.extendComp ρ (Φ'.toState n m hV') (Φ.toState n m hV) S' S) (Φ.blowUpPieces S m)

The transported families refine again, the geometric counterpart of Refines.blowUp: after blowing up the centre S on X and the centre S' of the faces mapping into S on Y (the same blow-up of Y, centerOf_eq_comap), the transported family of Y refines the transported family of X along the induced morphism of blow-ups, with extendComp as the parent map. Old children go to old parents (the strict transform of a child lies in the pull-back of the strict transform of the parent, and the pull-back of a strict transform along a flat morphism is the strict transform of the pull-back, strictTransform_comap_of_flat of Hironaka/Scheme/BlowUpSequence/PullbackInduced.lean); the new piece F_Q = π⁻¹(Z_Q) of a face Q goes to the new piece F_{ρ(Q)}, whose pull-back is the union of the F_Q over Q mapping onto the same face.

theorem Hironaka.Monomial.PieceFamily.blowUpPieces_refinesAlong {X Y : AlgebraicGeometry.Scheme} {Φ : PieceFamily X} {h : Y ⟶ X} {ρ : ℕ → ℕ} {Φ' : PieceFamily Y} {n m : ℕ} {k k' : Type u} [Field k] [Field k'] (f : X ⟶ AlgebraicGeometry.Spec ↧k) [AlgebraicGeometry.LocallyOfFiniteType f] (g : Y ⟶ AlgebraicGeometry.Spec ↧k') [AlgebraicGeometry.LocallyOfFiniteType g] [AlgebraicGeometry.Flat h] (hρ : Φ'.RefinesAlong h ρ Φ) {hV : Φ.IsValid n m} {S : Finset (Finset ℕ)} (hS : (Φ.toState n m hV).IsCenter S) {hV' : Φ'.IsValid n m} {S' : Finset (Finset ℕ)} (hS' : (Φ'.toState n m hV').IsCenter S') (hS'S : ∀ Q ∈ S', Finset.image ρ Q ∈ S) (hlift : ∀ P ∈ S, ∀ (y : ↥Y), h y ∈ Φ.faceSet P → ∃ Q ∈ S', y ∈ Φ'.faceSet Q) (hc : Φ'.centerOf S' = (Φ.centerOf S).comap h) : (Φ'.blowUpPieces S' m).RefinesAlong (CategoryTheory.CategoryStruct.comp (CategoryTheory.eqToHom ⋯) (AlgebraicGeometry.Scheme.Hom.blowUpMap h (Φ.centerOf S))) (MonomialState.extendComp ρ (Φ'.toState n m hV') (Φ.toState n m hV) S' S) (Φ.blowUpPieces S m)

The transported families refine again, with the labels: blowUpPieces_refinesAlongW and the two label clauses (both families gain exactly one label).

theorem Hironaka.Monomial.PieceFamily.totalTransform_component_memberOf_blowUpPieces {X Y : AlgebraicGeometry.Scheme} {Φ : PieceFamily X} {h : Y ⟶ X} {ρ : ℕ → ℕ} {Φ' : PieceFamily Y} {E : X.DivisorFamily} {e : E.ι ≃o Fin Φ.nextLabel} {E' : Y.DivisorFamily} {e' : E'.ι ≃o Fin Φ'.nextLabel} {n m : ℕ} [AlgebraicGeometry.Flat h] (hρ : Φ'.RefinesAlongW h ρ Φ) (hlab : ∀ (c' : ℕ) (hc' : c' < Φ'.nextComp), E'.component (Φ'.memberOf e' c' hc') = (E.component (Φ.memberOf e (ρ c') ⋯)).comap h) {hV : Φ.IsValid n m} {S : Finset (Finset ℕ)} {hV' : Φ'.IsValid n m} {S' : Finset (Finset ℕ)} (hc : Φ'.centerOf S' = (Φ.centerOf S).comap h) {c'' : ℕ} (hc'' : c'' < (Φ'.blowUpPieces S' m).nextComp) (hlt : MonomialState.extendComp ρ (Φ'.toState n m hV') (Φ.toState n m hV) S' S c'' < (Φ.blowUpPieces S m).nextComp) : (E'.totalTransform (Φ'.centerOf S')).component ((Φ'.blowUpPieces S' m).memberOf (extendIso e') c'' hc'') = ((E.totalTransform (Φ.centerOf S)).component ((Φ.blowUpPieces S m).memberOf (extendIso e) (MonomialState.extendComp ρ (Φ'.toState n m hV') (Φ.toState n m hV) S' S c'') hlt)).comap (CategoryTheory.CategoryStruct.comp (CategoryTheory.eqToHom ⋯) (AlgebraicGeometry.Scheme.Hom.blowUpMap h (Φ.centerOf S)))

The member of a transported child is the pull-back of the member of its transported parent: an old child's member is the strict transform of its member (strictTransform_comap_of_flat), a new child's member is the exceptional divisor (exceptionalDivisor_comap).

The fold: the run on Y is the pull-back of the run on X

theorem Hironaka.Monomial.PieceFamily.realizeAux_pullback_of_surjective {k k' : Type u} [Field k] [PerfectField k] [Field k'] [PerfectField k'] (L : List (Finset (Finset ℕ))) {X Y : AlgebraicGeometry.Scheme} (f : X ⟶ AlgebraicGeometry.Spec ↧k) [AlgebraicGeometry.Smooth f] [AlgebraicGeometry.QuasiCompact f] (g : Y ⟶ AlgebraicGeometry.Spec ↧k') [AlgebraicGeometry.Smooth g] [AlgebraicGeometry.QuasiCompact g] (h : Y ⟶ X) [AlgebraicGeometry.Flat h] : Function.Surjective ⇑h → ∀ (Φ : PieceFamily X) {E : X.DivisorFamily} {e : E.ι ≃o Fin Φ.nextLabel}, E.IsSnc → Φ.Realizes E e → ∀ {n m : ℕ} (hV : Φ.IsValid n m), (∃ n' ≤ n, AlgebraicGeometry.SmoothOfRelativeDimension n' f) → ∀ {st' : MonomialState}, (Φ.toState n m hV).IsRun L st' → ∀ (Φ' : PieceFamily Y) {E' : Y.DivisorFamily} {e' : E'.ι ≃o Fin Φ'.nextLabel} {ρ : ℕ → ℕ} (hρ : Φ'.RefinesAlongW h ρ Φ), E'.IsSnc → Φ'.Realizes E' e' → (∀ (c' : ℕ) (hc' : c' < Φ'.nextComp), E'.component (Φ'.memberOf e' c' hc') = (E.component (Φ.memberOf e (ρ c') ⋯)).comap h) → ∀ (hV' : Φ'.IsValid n m), (∃ n' ≤ n, AlgebraicGeometry.SmoothOfRelativeDimension n' g) → MonomialState.Refines ρ (Φ'.toState n m hV') (Φ.toState n m hV) → Φ'.realizeAux m (MonomialState.chainRun ρ (Φ'.toState n m hV') (Φ.toState n m hV) L) = (Φ.realizeAux m L).pullback h

Along a run on X, the chain run on a family of Y refining along a flat surjection h realises the pull-back of the realisation, by one induction on the run: the centre of Y is the pull-back of the centre of X (centerOf_eq_comap), the transported families refine again along the induced morphism of blow-ups (blowUpPieces_refinesAlong), which is again a flat surjection, and pullback_eqToHom_comp of Hironaka/Scheme/BlowUpSequence/Pullback.lean identifies the tails. The general form, h flat with the snc of the pulled-back boundary as a hypothesis.

The statement for a smooth surjection

theorem Hironaka.Monomial.PieceFamily.realize_pullback_of_surjective {X Y : AlgebraicGeometry.Scheme} {Φ : PieceFamily X} {h : Y ⟶ X} {ρ : ℕ → ℕ} {Φ' : PieceFamily Y} {E : X.DivisorFamily} {e : E.ι ≃o Fin Φ.nextLabel} {n m : ℕ} {k : Type u} [Field k] [PerfectField k] (f : X ⟶ AlgebraicGeometry.Spec ↧k) [AlgebraicGeometry.Smooth f] [AlgebraicGeometry.QuasiCompact f] [AlgebraicGeometry.Smooth h] [AlgebraicGeometry.QuasiCompact (CategoryTheory.CategoryStruct.comp h f)] (hs : Function.Surjective ⇑h) (hE : E.IsSnc) (hΦ : Φ.Realizes E e) (hV : Φ.IsValid n m) (hn : ∃ n' ≤ n, AlgebraicGeometry.SmoothOfRelativeDimension n' f) (hn' : ∃ n' ≤ n, AlgebraicGeometry.SmoothOfRelativeDimension n' (CategoryTheory.CategoryStruct.comp h f)) (hρ : Φ'.RefinesAlong h ρ Φ) (hΦ' : Φ'.Realizes (E.comap h) (e.trans (Fin.castOrderIso ⋯))) (hV' : Φ'.IsValid n m) : Φ'.realize n m hV' = (Φ.realize n m hV).pullback h

The first clause of [Kol07, 34.1] for the geometric Step 3: for a smooth surjection h, the geometric Step 3 on Y is the pull-back of the geometric Step 3 on X. The run on Y is the chain run of the run on X (step3_chain of Hironaka/Resolution/Algebraic/Monomial/Geometric/ChainRun.lean on refines_toState_of_surjective) and the chain run realises the pull-back (realizeAux_pullback_of_surjective with Y's structure morphism h ≫ f).