Simple normal crossings of the trivial total transform

For a trivial blow-up π : B_Z X ⟶ X (an isomorphism, Z invertible; [Kol07, Warning 20]), Kollár's conditions (1)–(3) for the total transform (π_*^{-1} E^i, F) at a point x' of B_Z X are read off from the snc data of E and Z at x = π(x') ([Kol07, Definition 24 (4)]): the coordinates z at x are carried to x' by the stalk map of π (an isomorphism of local rings, so a regular system of parameters goes to one); the stalk of the strict transform of E^i at x' is the image of the stalk of the saturation E^i.saturate Z at x, which is (E^i)_x = (z_{c(i)}) wherever x' lies on the strict transform (stalkIdeal_saturate_eq_of_mem_support of Hironaka.Scheme.Snc.TrivialTotalTransform), and the stalk of F = Z.comap π is the image of Z_x = (z_j); the component with c(i) = j has died (its strict transform has stalk (1) at x'), so the new index map — c on the surviving old components, j on F — is injective. This is Kollár's π⁻¹_{tot}(E) = E + Z for a trivial blow-up [Kol07, Definition 65], used by Hironaka.Scheme.Snc.TotalTransformSmoothBlowUp and by the single-centre and boundary-clearing arguments of Hironaka.Resolution and Hironaka.BoundaryClearing.

Main declarations

• AlgebraicGeometry.stalkMapEquiv — the stalk map of an isomorphism as a ring equivalence, with the transport of a regular system of parameters (maximalIdeal_eq_span_range_stalkMap, natCast_eq_ringKrullDim_stalk_of_isIso).
• IsRegular AlgebraicGeometry.of_isIso — regularity along an isomorphism of schemes.
• AlgebraicGeometry.stalkIdeal_strictTransformAlong_of_isIso, mem_support_strictTransformAlong_of_isIso_iff, notMem_support_saturate_of_stalkIdeal_eq.
• AlgebraicGeometry.exists_snc_data_trivialTotalTransform — the snc data of the family (strict transforms, F) at a point of B_Z X.

Sources: [Kol07, Definition 24; Definition 65; Warning 20].

noncomputable def AlgebraicGeometry.stalkMapEquiv {X B : Scheme} (π : B ⟶ X) [CategoryTheory.IsIso π] (x' : ↥B) : ↑(X.presheaf.stalk (π x')) ≃+* ↑(B.presheaf.stalk x')

The stalk map of an isomorphism of schemes, as a ring equivalence.

Equations

• AlgebraicGeometry.stalkMapEquiv π x' = (CategoryTheory.asIso (AlgebraicGeometry.Scheme.Hom.stalkMap π x')).commRingCatIsoToRingEquiv

theorem AlgebraicGeometry.stalkMapEquiv_apply {X B : Scheme} (π : B ⟶ X) [CategoryTheory.IsIso π] (x' : ↥B) (a : ↑(X.presheaf.stalk (π x'))) : (stalkMapEquiv π x') a = (CategoryTheory.ConcreteCategory.hom (Scheme.Hom.stalkMap π x')) a

theorem AlgebraicGeometry.maximalIdeal_eq_span_range_stalkMap {X B : Scheme} (π : B ⟶ X) [CategoryTheory.IsIso π] (x' : ↥B) {n : ℕ} {z : Fin n → ↑(X.presheaf.stalk (π x'))} (hz : IsLocalRing.maximalIdeal ↑(X.presheaf.stalk (π x')) = Ideal.span (Set.range z)) : IsLocalRing.maximalIdeal ↑(B.presheaf.stalk x') = Ideal.span (Set.range fun (i : Fin n) => (CategoryTheory.ConcreteCategory.hom (Scheme.Hom.stalkMap π x')) (z i))

A regular system of parameters at π x' is carried by the stalk map to one at x' (𝔪 goes to 𝔪 under a surjective local homomorphism).

theorem AlgebraicGeometry.natCast_eq_ringKrullDim_stalk_of_isIso {X B : Scheme} (π : B ⟶ X) [CategoryTheory.IsIso π] (x' : ↥B) {n : ℕ} (hn : ↑n = ringKrullDim ↑(X.presheaf.stalk (π x'))) : ↑n = ringKrullDim ↑(B.presheaf.stalk x')

The Krull dimension is carried along the stalk map of an isomorphism.

theorem AlgebraicGeometry.stalkIdeal_strictTransformAlong_of_isIso {X B : Scheme} (π : B ⟶ X) [CategoryTheory.IsIso π] (Z J : X.IdealSheafData) (x' : ↥B) : (J.strictTransformAlong π (Z.comap π)).stalkIdeal x' = Ideal.map (CommRingCat.Hom.hom (Scheme.Hom.stalkMap π x')) ((J.saturate Z).stalkIdeal (π x'))

The stalk at x' of the strict transform along the isomorphism π is the image of the stalk of the saturation at π x'.

theorem AlgebraicGeometry.mem_support_strictTransformAlong_of_isIso_iff {X B : Scheme} (π : B ⟶ X) [CategoryTheory.IsIso π] (Z J : X.IdealSheafData) (x' : ↥B) : x' ∈ (J.strictTransformAlong π (Z.comap π)).support ↔ π x' ∈ (J.saturate Z).support

x' lies on the strict transform iff π x' lies on the saturation.

theorem AlgebraicGeometry.mem_support_comap_of_isIso_iff {X B : Scheme} (π : B ⟶ X) (Z : X.IdealSheafData) (x' : ↥B) : x' ∈ (Z.comap π).support ↔ π x' ∈ Z.support

x' lies on F = Z.comap π iff π x' lies on Z.

theorem AlgebraicGeometry.IsRegular.of_isIso {Y Y' : Scheme} (e : Y ⟶ Y') [CategoryTheory.IsIso e] (h : IsRegular Y) : IsRegular Y'

Regularity of a scheme transports along an isomorphism (stalks are isomorphic).

theorem AlgebraicGeometry.notMem_support_saturate_of_stalkIdeal_eq {X : Scheme} (D Z : X.IdealSheafData) (hZ : Z.IsInvertible) {x : ↥X} (hD : D.stalkIdeal x = Z.stalkIdeal x) : x ∉ (D.saturate Z).support

A component equal to the centre near x dies: x is not on the support of its saturation.

noncomputable def AlgebraicGeometry.trivialTotalTransformFamily {X B : Scheme} (π : B ⟶ X) (Z : X.IdealSheafData) {ι : Type u_1} (E : ι → X.IdealSheafData) : ι ⊕ PUnit.{u + 1} → B.IdealSheafData

The family (π_*^{-1} E^i, F) of the total transform under the isomorphism π, as an unbundled family on B indexed by ι ⊕ PUnit.

Equations

• AlgebraicGeometry.trivialTotalTransformFamily π Z E = Sum.elim (fun (i : ι) => (E i).strictTransformAlong π (Z.comap π)) fun (x : PUnit.{?u.2 + 1}) => Z.comap π

theorem AlgebraicGeometry.exists_snc_data_trivialTotalTransform {X B : Scheme} (π : B ⟶ X) [CategoryTheory.IsIso π] (hreg : ∀ (x : ↥X), IsRegularLocalRing ↑(X.presheaf.stalk x)) (Z : X.IdealSheafData) (hZ : Z.IsInvertible) {ι : Type u_1} (E : ι → X.IdealSheafData) (hdata : ∀ (i : ι), ∀ x ∈ (E i).support, x ∈ Z.support → SncDataAt (E i) Z x) (x' : ↥B) {n : ℕ} {z : Fin n → ↑(X.presheaf.stalk (π x'))} (c : { i : ι // π x' ∈ (E i).support } → Fin n) (hcinj : Function.Injective c) (hc : ∀ (i : { i : ι // π x' ∈ (E i).support }), (E ↑i).stalkIdeal (π x') = Ideal.span {z (c i)}) (hj : π x' ∈ Z.support → ∃ (j : Fin n), Z.stalkIdeal (π x') = Ideal.span {z j}) : ∃ (c' : { k : ι ⊕ PUnit.{u + 1} // x' ∈ (trivialTotalTransformFamily π Z E k).support } → Fin n), Function.Injective c' ∧ ∀ (k : { k : ι ⊕ PUnit.{u + 1} // x' ∈ (trivialTotalTransformFamily π Z E k).support }), (trivialTotalTransformFamily π Z E ↑k).stalkIdeal x' = Ideal.span {(CategoryTheory.ConcreteCategory.hom (Scheme.Hom.stalkMap π x')) (z (c' k))}

Kollár's conditions (1)–(3) at a point x' of B_Z X for the trivial total transform — given coordinates z at x = π x', an injective assignment c of coordinates to the components of E through x, and (if x ∈ Z) the coordinate z_j of Z, the assignment c on the surviving old components, j on F, is an injective assignment of the coordinates π♯ z at x' to the members of (π_*^{-1} E^i, F) through x' (the transport of the regular system of parameters itself is maximalIdeal_eq_span_range_stalkMap).