Pulling back a concatenation

The pullback of a concatenation is the concatenation of the pullbacks, h^*(S · T) = (h^*S) · (h_r^* T), where h_r is the lift of h to the last stage (pullbackLastHom: pullbackStageHom of Hironaka/Scheme/BlowUpSequence/Pullback.lean at the last index, typed at S.last through the identification pullbackStageIdx_last of the last indices). This is the bookkeeping behind [Kol07, 104, Step 2.3]: the functoriality of a sequence assembled from rounds follows from the functoriality of each round, with the pullback of [Kol07, 30.1].

noncomputable def AlgebraicGeometry.Scheme.BlowUpSequence.pullbackLastHom {X Y : Scheme} (S : X.BlowUpSequence) (h : Y ⟶ X) : (S.pullback h).last ⟶ S.last

The lift of h to the last stage of the pulled-back sequence [Kol07, 30.1], typed at the last stages (pullbackStageHom at the last index through the identification pullbackStageIdx_last).

Equations

• S.pullbackLastHom h = CategoryTheory.CategoryStruct.comp (CategoryTheory.eqToHom ⋯) (S.pullbackStageHom h (Fin.last S.length))

theorem AlgebraicGeometry.pullbackLastHom_nil {X Y : Scheme} (h : Y ⟶ X) : (Scheme.BlowUpSequence.nil X).pullbackLastHom h = h

The lift at the last stage of the empty sequence is h.

theorem AlgebraicGeometry.pullbackLastHom_cons {X Y : Scheme} (D : X.IdealSheafData) (rest : D.blowUp.BlowUpSequence) (h : Y ⟶ X) : (Scheme.BlowUpSequence.cons X D rest).pullbackLastHom h = rest.pullbackLastHom (Scheme.Hom.blowUpMap h D)

The lift at the last stage of a cons is the tail's lift along blowUpMap h D (definitional).

theorem AlgebraicGeometry.pullback_concat {X : Scheme} (S : X.BlowUpSequence) (T : S.last.BlowUpSequence) {Y : Scheme} (h : Y ⟶ X) : (S.concat T).pullback h = (S.pullback h).concat (T.pullback (S.pullbackLastHom h))

The pullback of a concatenation is the concatenation of the pullbacks, the second along the lift of h to the last stage [Kol07, 30.1 and Definition 29].