Pullback of a blow-up sequence along a morphism: the stage lifts #
The recursion AlgebraicGeometry.Scheme.BlowUpSequence.pullback pulls a sequence back center by
center, (cons X D rest).pullback h = cons Y (D.comap h) (rest.pullback (blowUpMap h D)), the tail
being pulled back along the morphism of blow-ups blowUpMap h D : blowUp (D.comap h) ⟶ blowUp D
that lies over h (the universal property of the blow-up). For a smooth h : Y → X this is the
pull-back h^* B of [Kol07, 30.1]: the sequence of fibre products X_i ×_X Y with centers
Z_i ×_X Y, together with the induced maps h_i : X_i ×_X Y → X_i. This module defines
pullbackStageIdx,pullbackCenterIdx: the index transports along the length identitylength_pullback(Fin.cast, reducible), so that the stages and centers ofS.pullback hare indexed by those ofS;pullbackStageHom S h i : (S.pullback h).stage _ ⟶ S.stage i: Kollár'sh_i, by recursion on the sequence:hat stage0, and at stagei + 1the liftblowUpMap h_i (S.center i)ofh_ito the blow-ups;CentersInRange S h: every center|Z_i|lies in the image ofh_i(automatic for a surjective flath),
and proves the basic facts about them: the commuting squares h_i ≫ Π_i = Π'_i ≫ h, the centers
(S.pullback h).center i = (S.center i).comap h_i, the cartesian stage squares for flat h, with
smoothness, flatness and surjectivity of the h_i by base change (and that the h_i of an open
immersion are open immersions, used for the locality of maximal contact), the functoriality of
the pullback in h (pullback_comp, pullback_id), and the injectivity of the pullback along a
flat morphism whose stage lifts cover the centers (pullback_injective; Kollár's "if h is
surjective then h^* B determines B uniquely"). The pullback of a smooth sequence is smooth
(Hironaka/Scheme/BlowUpSequence/PullbackSmooth.lean), and the induced ideals and divisors pull
back (Hironaka/Scheme/BlowUpSequence/PullbackInduced.lean); see also [Wlo05, Proposition 2.4.2].
The index transport of stages along length_pullback: a stage index of S read as a stage
index of S.pullback h. Reducible, so that (S.pullback h).stage (S.pullbackStageIdx h ⟨j, _⟩)
unfolds on the constructor shapes.
Equations
- S.pullbackStageIdx h i = Fin.cast ⋯ i
Instances For
The index transport of centers along length_pullback.
Equations
- S.pullbackCenterIdx h i = Fin.cast ⋯ i
Instances For
The stage lifts of h along the pulled-back sequence: h_0 = h and
h_{i+1} = blowUpMap h_i (Z_i), the morphism of blow-ups over h_i given by the universal
property. These are the maps h_i : X_i ×_X Y → X_i of [Kol07, 30.1] and the lifts φ_i of
[Wlo05, Proposition 2.4.2 (1)]: for flat h the stages of S.pullback h are the fibre products
X_i ×_X Y and the h_i their projections (isPullback_pullbackStageHom).
Equations
- (AlgebraicGeometry.Scheme.BlowUpSequence.nil x✝²).pullbackStageHom x✝ x_7 = x✝
- (AlgebraicGeometry.Scheme.BlowUpSequence.cons x✝² D rest).pullbackStageHom x✝ ⟨0, isLt⟩ = x✝
- (AlgebraicGeometry.Scheme.BlowUpSequence.cons x✝² D rest).pullbackStageHom x✝ ⟨j.succ, hj⟩ = rest.pullbackStageHom (AlgebraicGeometry.Scheme.Hom.blowUpMap x✝ D) ⟨j, ⋯⟩
Instances For
The centers of S lie in the images of the stage lifts, |Z_i| ⊆ h_i(X_i ×_X Y) for every
i. This is the hypothesis under which a flat pullback determines the sequence
(pullback_injective); it is automatic when h is surjective and flat
(centersInRange_of_surjective). Compare [Kol07, 30.1]: if h is surjective then h^* B
determines B uniquely, while otherwise "we lose information about the centers living above
X ∖ h(Y)".
Equations
- S.CentersInRange h = ∀ (i : Fin S.length), ↑(S.center i).support ⊆ Set.range ⇑(S.pullbackStageHom h i.castSucc)
Instances For
The recursion on the constructor shapes #
The pullback of the empty sequence (definitional).
The pullback of a cons (definitional).
The stage lift on the empty sequence is h (definitional).
The stage lift at index 0 of a cons is h (definitional).
The stage lift at index j + 1 of a cons is the tail's (definitional).
The stage lifts lie over h, in the ⟨j, hj⟩ form of the indices in which the recursions
unfold.
The stage lifts lie over h: h_i ≫ Π_i = Π'_i ≫ h [Kol07, 30.1].
The centers of the pullback are the inverse images of the centers, in the ⟨j, hj⟩ form.
The i-th center of the pullback is the inverse image of Z_i under the stage lift h_i
(the center Z_i ×_X Y of [Kol07, 30.1]).
The j-th blow-up of the pullback lies over the j-th blow-up of S, in the ⟨j, hj⟩
form.
The i-th blow-up of the pullback lies over the i-th blow-up of S: the square of
h^* π_i over π_i in [Kol07, 30.1].
The exceptional divisor of the i-th blow-up of the pullback is the inverse image of
F_{i+1} under h_{i+1}, for every h [Wlo05, Proposition 2.4.2, proof].
The fibre-product squares (flat base change) #
The stage squares of a flat pullback are cartesian, in the ⟨j, hj⟩ form: the pullback
square of one blow-up map (AlgebraicGeometry.isPullback_blowUpMap) pasted stage by stage.
For flat h the stage squares are cartesian: the stages of the pullback are the fibre
products X_i ×_X Y of [Kol07, 30.1].
The stage lifts of a flat h are flat.
The stage lifts of a smooth h are smooth [Kol07, 30.1].
The stage lifts of an open immersion h are open immersions: base change along the cartesian
squares isPullback_pullbackStageHom (open immersions are flat, so the squares are cartesian).
Used for the locality of maximal contact.
The image of the stage lift is the preimage under Π_i of the image of h.
The stage lifts of a surjective flat h are surjective.
Transport lemmas: equality of sequences, functoriality of the pullback #
Equality of two cons terms is equality of the centers and, after substitution, of the
tails.
The converse direction used by the transport proofs: cons of equal centers and
heterogeneously equal tails are equal.
Pulling back along eqToHom e ≫ h is pulling back along h, up to the transport of the base
along e.
The transport of the blow-up projection along an equality of centers.
The coherence of the morphisms of blow-ups under composition, by the uniqueness clause of the
universal property (AlgebraicGeometry.blowUpMap_comp_eq, restated on the abbreviations of the
sequence vocabulary).
The morphism of blow-ups over the identity is the transport along comap_id.
The pullback is functorial: (f ≫ g)^* S = f^* (g^* S).
Pulling back along the identity is the identity.
The stalk map of the identity is an isomorphism (Mathlib's stalkMap_id).
The stalk of the inverse image along the identity is the stalk.
The index transport sends the last stage to the last stage.
A flat pullback covering the centers determines the sequence #
A surjective flat h covers every center.
Two sequences whose centers lie in the images of the stage lifts of a flat h, and whose
pullbacks along h agree, are equal [Kol07, 30.1]: by induction on the sequence, an ideal sheaf
whose support lies in the image of a flat morphism being determined by its inverse image
(Scheme.IdealSheafData.eq_of_comap_eq_of_flat) at each stage.
A surjective flat pullback is injective on sequences: "if h is surjective then h^* B
determines B uniquely" [Kol07, 30.1].
An isomorphism of schemes is surjective on points.