The refinement of a piece family along a smooth morphism #
For a smooth h : Y ⟶ X and a piece family Φ realising an snc boundary E on X, the
irreducible components of the preimages h⁻¹(D_c) of the pieces form a piece family of Y
refining Φ along h (RefinesAlong of
Hironaka/Resolution/Algebraic/Monomial/Geometric/Pieces.lean): each child lies in the preimage of
its parent, the preimage of a piece is the disjoint union of its children, and labels and exponents
pass through the parent map. This is the geometric side of the functoriality of Step 3 under smooth
morphisms, [Kol07, 34.1] for the third step of BMO_{n,m}, which Kollár dismisses with "the
functoriality conditions are just as obvious as before" at the end of [Kol07, 111]. Not in the
sources as statements. This module proves the combinatorial and local facts:
exists_refinesAlong: such a family exists,ofDivisorFamilyonh⁻¹Ewith the exponentΦ.exponentAt ∘ h. The parent of a component is the unique piece through the image of its generic point, which is a generic point of the parent member since a flat morphism is generalising (mem_genericPoints_support_of_flatofHironaka/Scheme/BlowUpSequence/PullbackInduced.lean).refines_toState,refines_toState_of_surjective: the state of a refining family isRefines(Hironaka/Resolution/Algebraic/Monomial/Restrict.lean) the state ofXrestricted to the faces with a point overY(the full state whenhis surjective). Faces map to faces (a common point maps to a common point), the parent map is injective on a face (children of one parent are disjoint), and a face with a point overYlifts (one child of each parent through that point).sub_restrictState,mem_nerve_restrictState: the restricted state isSubthe state, with the nerve{T : Z_T ∩ im h ≠ ∅}(definitional).monomial_comap_exponentAt: the marked monomial ideal of the refining family is the pull-back of the marked monomial ideal. Stalk by stalk, the components ofh⁻¹E^ithroughymap to the components ofE^ithroughh ywith the same exponent (stalkIdeal_monomialofHironaka/Resolution/Algebraic/MarkedOrderReduction/Split.leanon both sides, andIdeal.mapof the finite product).
The runs are compared in Hironaka/Resolution/Algebraic/Monomial/Geometric/PullbackRun.lean and
Hironaka/Resolution/Algebraic/Monomial/Geometric/PullbackErase.lean.
The label-free part of RefinesAlong #
The label-free part of RefinesAlong: the parent map, the exponents and the pieces without
the two label clauses. It is the invariant of the general fold (realizeAux_pullback_eraseEmpty
of Hironaka/Resolution/Algebraic/Monomial/Geometric/PullbackErase.lean): across an empty blow-up
of X (a centre missing the image of h) the family on X gains a label the family on Y does
not, so nextLabel_eq fails while everything geometric survives; the labels are then carried by the
member transport hlab.
Instances For
RefinesAlong forgets to its label-free part.
Consequences of RefinesAlongW #
A point of a child lies over a point of its parent.
A point over a piece lies on one of its children.
The parent map is injective on a set of children with a common point (children of one parent are disjoint).
A common point of a face of Y maps to a common point of the image face.
The image of a face of Y is a face of X.
A face of X with a point over Y is the image of a face of Y through that point: one child
of each of its pieces through the point.
The restricted state and the refinement of states #
The restricted state is Sub the state of X: the same counters, labels and exponents, a
subnerve.
The nerve of the restricted state: the faces whose face set meets the image of h.
The state of a refining family refines, along the parent map, the state of X restricted to
the faces with a point over Y.
For surjective h every face of X has a point over Y, and the state of a refining family
refines the full state of X. This is why a smooth surjection needs no deletion of empty
blow-ups in the first clause of [Kol07, 34.1].
The refining family: the components of the preimages #
The parent of a component of the pulled-back family: the piece of Φ through the image of its
generic point (a singleton face, faceAt_eq_singleton_of_mem_genericPoints).
Equations
Instances For
The parent of a component: the image of the generic point is a generic point of the parent member (flat morphisms are generalizing), through which exactly one piece passes.
The family of the irreducible components of the preimages h⁻¹(D_c), ofDivisorFamily on
h⁻¹E with the exponent Φ.exponentAt ∘ h, refines Φ along a flat h through parentOf:
labels and exponents pass to the parent (the image of the generic point lies on the parent piece
only), each child lies in the preimage of its parent, the preimage of a piece is the union of
its children (a generic point of h⁻¹(D_c) is a generic point of the member's preimage, the
pieces of a label being disjoint), and children of one parent are disjoint (two components of
the regular member h⁻¹E^j through a point coincide). The snc of h⁻¹E is a hypothesis.
A piece family of Y refining Φ along a flat h exists, the irreducible components of the
preimages of the pieces (finitely many, Y being Noetherian), and it realises h^{-1}E through
the same label isomorphism (ofDivisorFamily_realizes on the snc boundary h^{-1}E).
The smooth form: for a smooth h with Y quasi-compact over k, a refining family exists
(exists_refinesAlong_of_flat, with h⁻¹E snc by isSnc_comap_of_smooth of
Hironaka/Scheme/BlowUpSequence/PullbackSnc.lean and Y Noetherian).
The marked monomial ideal pulls back #
The marked monomial ideal of the refining family is the pull-back of the marked monomial
ideal: stalk by stalk, the one component of h⁻¹E^i through y maps to the one component of
E^i through h y (flat morphisms are generalising), and the exponents agree, the child through
the generic point lying over the parent through its image.