Consequences of a cartesian square of schemes

The stages of a blow-up sequence pulled back along a morphism h : Y → X are the fibre products Xᵢ ×_X Y [Kol07, Definition 30, 30.1], and for flat h the base-change square of the induced morphism of blow-ups is cartesian [TSPA, Tag 0805]; this is used to transfer properties of h to its lifts (étale, smooth, flat, image = π⁻¹(im h)). The two transfers are pure pullback bookkeeping and are stated here for an arbitrary cartesian square of schemes IsPullback fst snd f g (fst ≫ f = snd ≫ g):

• range_fst_of_isPullback: the image of fst is f⁻¹(im g) — Mathlib's Scheme.Pullback.range_fst for the chosen pullback, transported along the comparison isomorphism;
• property_of_isPullback: a property stable under base change passes from g to fst (Mathlib's MorphismProperty.IsStableUnderBaseChange).

They are applied to the square IsPullback (blowUpMap h D) π_Y π_X h of isPullback_blowUpMap and to the base change of blow-up sequences.

theorem AlgebraicGeometry.range_fst_of_isPullback {P X Y Z : Scheme} {fst : P ⟶ X} {snd : P ⟶ Y} {f : X ⟶ Z} {g : Y ⟶ Z} (H : CategoryTheory.IsPullback fst snd f g) : Set.range ⇑fst = ⇑f ⁻¹' Set.range ⇑g

In a cartesian square of schemes the image of fst is the preimage under f of the image of g (Mathlib's Scheme.Pullback.range_fst).

theorem AlgebraicGeometry.property_of_isPullback {P X Y Z : Scheme} {fst : P ⟶ X} {snd : P ⟶ Y} {f : X ⟶ Z} {g : Y ⟶ Z} (Q : CategoryTheory.MorphismProperty Scheme) [Q.IsStableUnderBaseChange] (H : CategoryTheory.IsPullback fst snd f g) (hg : Q g) : Q fst

A property of morphisms stable under base change passes from g to fst in a cartesian square (Mathlib's MorphismProperty.IsStableUnderBaseChange).