Documentation

Hironaka.Resolution.Algebraic.Monomial.Geometric.PullbackErase

Functoriality of the realised Step 3 under flat morphisms: the general fold #

The second clause of [Kol07, 34.1] for the third step of BMO_{n,m}: for a family Φ' on Y refining Φ on X along a flat h : Y ⟶ X (no surjectivity), the realised Step 3 on Y is the pull-back of the realised Step 3 on X with the empty blow-ups deleted, Kollár's "deleting every blow-up h^*π_i whose centre is empty and reindexing", in the form BlowUpSequence.pullback and BlowUpSequence.eraseEmpty. Not in the sources beyond that sentence.

The result is used for the smooth functoriality of BMO_{n,m} in Hironaka/Resolution/Algebraic/MarkedOrderReduction/SmoothStep3.lean; the helper strictTransform_of_eq_top is used in Hironaka/Resolution/Algebraic/Kol07/Thm36/EraseEmptyIndex.lean.

Centres missing, or meeting, the image of h #

source
theorem Hironaka.Monomial.PieceFamily.comap_centerOf_eq_top {X Y : AlgebraicGeometry.Scheme} {Φ : PieceFamily X} {h : Y ⟶ X} {ρ : ℕ → ℕ} {Φ' : PieceFamily Y} (hρ : Φ'.RefinesAlongW h ρ Φ) {S : Finset (Finset ℕ)} (hS : S ⊆ Φ.nerve) (hno : {Q ∈ Φ'.nerve | Finset.image ρ Q ∈ S} = ∅) :
(Φ.centerOf S).comap h = ⊤

A centre of X with no face of Y over it has empty preimage: every point over a face of the centre lies on a face of Y mapping onto it (RefinesAlongW.exists_image_eq).

source
theorem Hironaka.Monomial.PieceFamily.comap_centerOf_ne_top {X Y : AlgebraicGeometry.Scheme} {Φ : PieceFamily X} {h : Y ⟶ X} {ρ : ℕ → ℕ} {Φ' : PieceFamily Y} (hρ : Φ'.RefinesAlongW h ρ Φ) {S : Finset (Finset ℕ)} (hne : {Q ∈ Φ'.nerve | Finset.image ρ Q ∈ S}.Nonempty) :
(Φ.centerOf S).comap h ≠ ⊤

A centre of X with a face of Y over it has nonempty preimage.

Transport across an empty blow-up #

source
theorem Hironaka.Monomial.PieceFamily.strictTransform_of_eq_top {W : AlgebraicGeometry.Scheme} {D : W.IdealSheafData} (hD : D = ⊤) (J : W.IdealSheafData) :
J.strictTransform D = J.comap D.blowUpπ

The strict transform under a centre propositionally equal to ⊤ is the pull-back (strictTransform_top_left).

source
theorem Hironaka.Monomial.PieceFamily.comap_strictTransform_skip {X Y : AlgebraicGeometry.Scheme} (h : Y ⟶ X) [AlgebraicGeometry.Flat h] {Z : X.IdealSheafData} [CategoryTheory.IsIso (Z.comap h).blowUpπ] (hZ : Z.comap h = ⊤) (J : X.IdealSheafData) :
(J.strictTransform Z).comap (CategoryTheory.CategoryStruct.comp (CategoryTheory.inv (Z.comap h).blowUpπ) (AlgebraicGeometry.Scheme.Hom.blowUpMap h Z)) = J.comap h

Along a skip (h misses the centre Z, and Y maps into Bl_Z X through the inverse of the trivial blow-up of Y) the strict transform of J pulls back to the pull-back of J (strictTransform_comap_of_flat of Hironaka/Scheme/BlowUpSequence/PullbackInduced.lean).

source
theorem Hironaka.Monomial.PieceFamily.preimage_strictTransformCloseds_skip {X Y : AlgebraicGeometry.Scheme} (h : Y ⟶ X) [AlgebraicGeometry.Flat h] {k : Type u} [Field k] (f : X ⟶ AlgebraicGeometry.Spec ↧k) [AlgebraicGeometry.Smooth f] {Z : X.IdealSheafData} [CategoryTheory.IsIso (Z.comap h).blowUpπ] (hZ : Z.comap h = ⊤) (C : TopologicalSpace.Closeds ↥X) :
(strictTransformCloseds Z C).preimage ⋯ = C.preimage ⋯

The closed-set form of comap_strictTransform_skip.

source
theorem Hironaka.Monomial.PieceFamily.π_skip {X Y : AlgebraicGeometry.Scheme} (h : Y ⟶ X) {Z : X.IdealSheafData} [CategoryTheory.IsIso (Z.comap h).blowUpπ] (y : ↥Y) :
Z.blowUpπ ((CategoryTheory.CategoryStruct.comp (CategoryTheory.inv (Z.comap h).blowUpπ) (AlgebraicGeometry.Scheme.Hom.blowUpMap h Z)) y) = h y

The square of a skip: π_X ∘ (inv π_Y ≫ blowUpMap) = h.

source
theorem Hironaka.Monomial.PieceFamily.refinesAlongW_skip {X Y : AlgebraicGeometry.Scheme} {Φ : PieceFamily X} (h : Y ⟶ X) {ρ : ℕ → ℕ} {Φ' : PieceFamily Y} {m : ℕ} [AlgebraicGeometry.Flat h] {k : Type u} [Field k] (f : X ⟶ AlgebraicGeometry.Spec ↧k) [AlgebraicGeometry.Smooth f] (hρ : Φ'.RefinesAlongW h ρ Φ) {S : Finset (Finset ℕ)} [CategoryTheory.IsIso ((Φ.centerOf S).comap h).blowUpπ] (hZ : (Φ.centerOf S).comap h = ⊤) :
Φ'.RefinesAlongW (CategoryTheory.CategoryStruct.comp (CategoryTheory.inv ((Φ.centerOf S).comap h).blowUpπ) (AlgebraicGeometry.Scheme.Hom.blowUpMap h (Φ.centerOf S))) ρ (Φ.blowUpPieces S m)

The skip: across an empty blow-up of X the refinement persists. Y's family is unchanged, X's becomes blowUpPieces; the old pieces' strict transforms pull back to the pieces (preimage_strictTransformCloseds_skip), the new pieces have empty preimage (they lie over the centre, which h misses).

source
theorem Hironaka.Monomial.PieceFamily.totalTransform_component_memberOf_blowUpPieces_skip {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} {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) {S : Finset (Finset ℕ)} [CategoryTheory.IsIso ((Φ.centerOf S).comap h).blowUpπ] (hZ : (Φ.centerOf S).comap h = ⊤) (c' : ℕ) (hc' : c' < Φ'.nextComp) (hlt : ρ c' < (Φ.blowUpPieces S m).nextComp) :
E'.component (Φ'.memberOf e' c' hc') = ((E.totalTransform (Φ.centerOf S)).component ((Φ.blowUpPieces S m).memberOf (extendIso e) (ρ c') hlt)).comap (CategoryTheory.CategoryStruct.comp (CategoryTheory.inv ((Φ.centerOf S).comap h).blowUpπ) (AlgebraicGeometry.Scheme.Hom.blowUpMap h (Φ.centerOf S)))

Across a skip the member transport persists: the member of a child on Y is the pull-back of the strict transform of the member of its parent.

source
theorem Hironaka.Monomial.PieceFamily.eraseEmpty_pullback_eqToHom_comp {X Y : AlgebraicGeometry.Scheme} (S : X.BlowUpSequence) {Y' : AlgebraicGeometry.Scheme} (e : Y' = Y) (h : Y ⟶ X) :
(S.pullback (CategoryTheory.CategoryStruct.comp (CategoryTheory.eqToHom e) h)).eraseEmpty ≍ (S.pullback h).eraseEmpty

Deleting the empty blow-ups commutes with the transport of the base along an equality (pullback_eqToHom_comp of Hironaka/Scheme/BlowUpSequence/Pullback.lean under eraseEmpty).

The fold #

source
theorem Hironaka.Monomial.PieceFamily.realizeAux_pullback_eraseEmpty {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] (Φ : 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.IsChainE ρ (Φ'.toState n m hV') (Φ.toState n m hV) L → Φ'.realizeAux m (MonomialState.chainRunE ρ (Φ'.toState n m hV') (Φ.toState n m hV) L) = ((Φ.realizeAux m L).pullback h).eraseEmpty

The second clause of [Kol07, 34.1] along a run: the chain run with skips on a family of Y refining along a flat h realises the pull-back of the realisation with the empty blow-ups deleted, by one induction on the run. At a step with a face of Y over the centre, the argument of realizeAux_pullback_of_surjective (the centre of Y is the pull-back of the centre of X, the transported families refine again, eraseEmpty_cons_of_ne_top keeps the cell); at a skip, the pulled-back centre is ⊤, eraseEmpty_cons_of_eq_top deletes the cell and carries the tail back along the inverse of the trivial blow-up of Y, and the refinement persists along inv π_Y ≫ blowUpMap (refinesAlongW_skip).

The statement for a smooth morphism #

source
theorem Hironaka.Monomial.PieceFamily.realize_pullback_eraseEmpty {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)] (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).eraseEmpty

The second clause of [Kol07, 34.1] for the geometric Step 3: for a smooth h, the geometric Step 3 on Y is the pull-back of the geometric Step 3 on X with the empty blow-ups deleted. The run on Y is the chain run with skips of the run on X (step3_chainE on refines_toState, sub_restrictState and Rel.refl, combining step3_restrict and step3_refine of Hironaka/Resolution/Algebraic/Monomial/Restrict/) and the chain run realises the deleted pull-back (realizeAux_pullback_eraseEmpty with Y's structure morphism h ≫ f).