Colon, saturation and strict transform along an isomorphism

For a trivial blow-up the projection π : B_Z X ⟶ X is an isomorphism [Kol07, Warning 20], and the strict transform (J.comap π).saturate (Z.comap π) of a closed subscheme J is the inverse image along π of the saturation J.saturate Z computed on X: inverse images along an isomorphism commute with colons (the inequality comap_colon_le applied to π and to π⁻¹) and hence with saturations. This is used for the total transforms of divisors under trivial blow-ups and for the order along a trivial blow-up in the resolution sequences.

Main declarations

• AlgebraicGeometry.Scheme.IdealSheafData.comap_colon_of_isIso, comap_saturate_of_isIso.
• AlgebraicGeometry.strictTransformAlong_of_isIso — strictTransformAlong π (Z.comap π) J = (J.saturate Z).comap π for an isomorphism π.

theorem AlgebraicGeometry.Scheme.IdealSheafData.comap_colon_of_isIso {Y X : Scheme} (e : Y ⟶ X) [CategoryTheory.IsIso e] (I K : X.IdealSheafData) : (I.colon K).comap e = (I.comap e).colon (K.comap e)

Inverse image along an isomorphism commutes with the colon.

theorem AlgebraicGeometry.Scheme.IdealSheafData.comap_saturate_of_isIso {Y X : Scheme} (e : Y ⟶ X) [CategoryTheory.IsIso e] (I K : X.IdealSheafData) : (I.saturate K).comap e = (I.comap e).saturate (K.comap e)

Inverse image along an isomorphism commutes with the saturation.

theorem AlgebraicGeometry.strictTransformAlong_of_isIso {B X : Scheme} (π : B ⟶ X) [CategoryTheory.IsIso π] (Z J : X.IdealSheafData) : J.strictTransformAlong π (Z.comap π) = (J.saturate Z).comap π

For an isomorphism π, the strict transform of J along π with respect to the divisor Z.comap π is the inverse image of the saturation J.saturate Z computed on X.