Push-forward of a blow-up sequence from a closed subscheme #
For a closed subscheme j : S ↪ X and a blow-up sequence B(S) with centers Z_i^S ⊂ S_i, the
push-forward j_* B of [Kol07, 30.3] is the sequence starting with X whose centers are
Z_i^X := (j_i)_* Z_i^S, the j_i : S_i ↪ X_i being the natural inclusions built inductively
(S_{i+1} = B_{Z_i^S} S_i ↪ B_{Z_i^X} X_i = X_{i+1}); "for all practical purposes
Z_i^X = Z_i^S", and the push-forward of a smooth blow-up sequence is smooth. The recursion is
AlgebraicGeometry.Scheme.BlowUpSequence.pushforward
(cons X (Z.map j) (rest.pushforward (pushforwardBlowUp j Z))), with
pushforwardBlowUp j Z : Z.blowUp ⟶ (Z.map j).blowUp the morphism of blow-ups over j on
Z.blowUp = blowUp Y ((Z.map j).comap j).
This module defines the stage inclusions
pushforwardStageHom j S i : S.stage i ⟶ (S.pushforward j).stage _ (j at stage 0,
pushforwardBlowUp at stage i + 1, the pattern of pullbackStageHom) with the index transports
pushforwardStageIdx, pushforwardCenterIdx, and proves: the push-forward has the length of the
sequence; the stage inclusions are closed immersions over j whose images are the strict
transforms of S, and the centers of j_* B are the pushed centers; the push-forward of a smooth
sequence is smooth; restriction and push-forward are inverse to each other (pullback_pushforward,
pushforward_pullback_of_strictTransformSeq_le), which is the injectivity of [Kol07, 51.1] and
the correspondence of [Kol07, Corollary 85]; the push-forward commutes with flat pullback along a
cartesian square (used in the proof of [Kol07, Lemma 102]) and is functorial in the closed
embedding ([Kol07, 34.3]). The last section gives the descent of the identity B(X) = j_* B(Y)
along a smooth surjection, used for the closed-embedding clause [Kol07, Claim 71.2].
Pushing forward a sequence does not change its length.
The index transport of stages along length_pushforward.
Equations
- S.pushforwardStageIdx j i = Fin.cast ⋯ i
Instances For
The index transport of centers along length_pushforward.
Equations
- S.pushforwardCenterIdx j i = Fin.cast ⋯ i
Instances For
The stage inclusions of a pushed-forward sequence, j_0 = j and
j_{i+1} = pushforwardBlowUp j_i Z_i, the closed immersion B_{Z_i} S_i ↪ B_{(j_i)_* Z_i} X_i
given by the universal property of the blow-up: "the j_i : S_i ↪ X_i are the natural
inclusions" [Kol07, 30.3].
Equations
- (AlgebraicGeometry.Scheme.BlowUpSequence.nil x✝³).pushforwardStageHom x✝¹ x_9 = x✝¹
- (AlgebraicGeometry.Scheme.BlowUpSequence.cons x✝³ D rest).pushforwardStageHom x✝¹ ⟨0, isLt⟩ = x✝¹
- (AlgebraicGeometry.Scheme.BlowUpSequence.cons x✝³ Z rest).pushforwardStageHom x✝¹ ⟨n.succ, hn⟩ = rest.pushforwardStageHom (AlgebraicGeometry.Scheme.Hom.pushforwardBlowUp x✝¹ Z) ⟨n, ⋯⟩
Instances For
The recursion, the square over j, closed immersions, centers, kernels #
The push-forward of the empty sequence.
The recursion of pushforward on a cons.
The one-step inclusion B_Z S ↪ B_{j_* Z} X lies over j (blowUpMap_π after the transport
AlgebraicGeometry.eqToHom_comp_blowUpπ).
The kernel of the one-step inclusion is the strict transform of the image of j under the
blow-up of X along j_* Z (Scheme.Hom.ker_comp_of_isIso for the transport).
The stage inclusions lie over j, in the ⟨n, hn⟩ form of the indices.
The stage inclusions j_i : S_i ↪ X_i lie over j [Kol07, 30.3].
The stage inclusions are closed immersions, in the ⟨n, hn⟩ form of the indices.
Every stage inclusion is a closed immersion [Kol07, 30.3].
The centers of the push-forward are the pushed centers, in the ⟨n, hn⟩ form.
The centers of the push-forward are the pushed centers, along the stage inclusions:
"Z_i^X := (j_i)_* Z_i^S" [Kol07, 30.3].
The kernel of the n-th stage inclusion is the n-th strict transform of the image of j
under the pushed-forward sequence, in the ⟨n, hn⟩ form.
The image of the stage inclusion j_i : S_i ↪ X_i is the strict transform of S (the
identification of [Kol07, 30.2] on the push-forward side).
The push-forward of a smooth blow-up sequence is smooth #
"If B is a smooth blow-up sequence, then so is j_* B" [Kol07, 30.3]: a smooth closed
subscheme of S_i is a smooth closed subscheme of X_i, the center (j_i)_* Z_i^S having
subscheme isomorphic to that of Z_i^S (Scheme.Hom.toImage of the closed immersion
Z_i^S ↪ S_i ↪ X_i), over the same structure morphism by pushforwardStageHom_stageMap;
Smooth respects isomorphisms.
Restriction and push-forward are inverse to each other #
Transport of the pushforward along an equality of targets and of the closed immersions
(bookkeeping for cons_congr).
The one-step inclusion pushforwardBlowUp j Z is blowUpMap j D up to the identification of
its source, whenever Z.map j = D (the transport eqToHom of its body is heterogeneously
trivial, eqToHom_comp_heq).
j^* j_* B = B: the first center comes back by comap_map_of_isClosedImmersion, and the rest
by induction along the inclusion pushforwardBlowUp j Z, the transport of its source being
invisible to pullback (pullback_eqToHom_comp). One half of the correspondence of
[Kol07, 51.1].
j_* j^* B = B when every center lies in the strict transform of S: the first center by
map_comap_of_ker_le, the rest by induction along blowUpMap j D (whose kernel is the strict
transform), the inclusion pushforwardBlowUp j (D.comap j) being blowUpMap j D up to
pushforwardBlowUp_heq. The other half of the correspondence of [Kol07, 51.1].
The centers of j_* B lie in the strict transforms of S: ker j_i ≤ Z.map j_i (map_bot,
map_mono) read through ker_pushforwardStageHom and center_pushforward.
j_* is injective, with pullback · j as a left inverse ("gives an injection",
[Kol07, 51.1]).
Push-forward commutes with smooth (flat) pullback #
Transport of the one-step blow-up morphism along an equality of centers (bookkeeping).
For h flat and a cartesian square j' ≫ h = hS ≫ j with j, j' closed immersions,
h^*(j_* B) = (j')_*(hS^* B) (the flat form of the compatibility used in the proof of
[Kol07, Lemma 102]). Induction on B: the first centers agree by comap_map_of_isPullback; the
square of the next stage, the inclusions pushforwardBlowUp over the flat base changes
blowUpMap, is again cartesian by isPullback_blowUpMap_of_isPullback, transported along the
identifications of the sources (comap_map_of_isClosedImmersion, comap_comap_eq_of_comm) by
isPullback_of_heq; the rest follows by the hypothesis and pushforward_heq.
For h : X' → X smooth and the cartesian square j' ≫ h = hS ≫ j (S' = h⁻¹(S),
hS = h|_{S'}), pulling back the push-forward along h is pushing forward the pullback along
hS: h^*(j_* B) = (j')_*(hS^* B) (pulling back and restricting commute, "we get the same result"
either way, [Kol07, Lemma 102, proof]). The flat form,
smooth morphisms being flat.
pullback_pushforward_of_isPullback for the closed subscheme V(J): S' = V(J.comap h) with
hS = subschemeMap (J.comap h) J h (the square is cartesian by
AlgebraicGeometry.isPullback_subschemeι_comap).
The inverse images of a divisor family match on a commutative square,
h⁻¹(E)|_{S'} = hS⁻¹(E|_S): DivisorFamily.comap_comp twice.
Functoriality of the push-forward in the closed embedding #
The one-step inclusions of a composite Z ↪ Y ↪ X compose: both sides are lifts over
π_D ≫ j' ≫ j to the blow-up of X along (D.map j').map j = D.map (j' ≫ j)
(blowUp.hom_ext).
The push-forward is functorial in the closed embedding, j_* j'_* B = (j' ≫ j)_* B (the
independence from further embeddings Z ↪ Y ↪ X of [Kol07, 34.3]): the centers agree by
map_comp and the one-step inclusions by pushforwardBlowUp_comp, transported by
pushforward_heq.
Push-forwards along isomorphisms; descent of the closed-embedding identity along a #
smooth surjection
The push-forward depends on the closed immersion only through its value: two equal closed immersions give equal push-forwards (the instance is a proof).
Pushing forward along an isomorphism the pullback along it gives the sequence back: pulling
back along the isomorphism (flat and surjective, surjective_of_isIso) is injective
(pullback_injective_of_surjective) and inverts the push-forward (pullback_pushforward).
A marked blow-up sequence functor commuting with smooth surjections ([Kol07, 34.1], first
clause) takes, at a triple carrying the pullback data along an isomorphism, the pullback of its
value. Stated on an abstract morphism so that the surjectivity of the isomorphism
(surjective_of_isIso) is checked on it.
The identity of [Kol07, Claim 71.2] descends along a smooth surjection ("the claimed
identity in (71.2) is a local question on X", [Kol07, 108]). For g : X' → X smooth and
surjective, the closed immersion j : Y → X, and a cartesian square j' ≫ g = h_S ≫ j with h_S
smooth and surjective, if the marked triples of X' and Y' carry the pullback data of those of
X and Y and B(X') = j'_* B(Y'), then B(X) = j_* B(Y): both sides of the latter pull back
along g to the two sides of the former (the first clause of [Kol07, 34.1] and
pullback_pushforward_of_isPullback), and pullback along the flat surjection g is injective.