Strict transforms of finite unions, monotonicity, reducedness

Three general facts about the strict transform of a closed subscheme along a blow-up sequence ([Kol07, Definition 30, 30.2]; the saturation of the pulled-back ideal by the exceptional ideal):

• the support of the strict transform of a finite union is the union of the strict transforms' supports (coe_support_strictTransformSeq_biUnion; one blow-up: coe_support_strictTransform describes the support as the closure of the preimage of V(J) minus the preimage of the centre, and closure commutes with finite unions);
• the strict transform is monotone in the ideal (strictTransformSeq_mono);
• the strict transform of a reduced closed subscheme is reduced (isReduced_strictTransformSeq_subscheme).

They are used by the embedded desingularization (Hironaka.Resolution.Algebraic.Wlo05.EmbeddedPullbackTools) and by the resolution functor on reduced schemes with several irreducible components (Hironaka.Resolution.Algebraic.Kol07.Thm36.EqualAbsorbingIndex), where the centre containing the strict transform of the whole scheme is compared with the centres containing the strict transforms of its components.

Strict transforms of finite unions; monotonicity; reduced ideals of closed sets

theorem Hironaka.Resolution.coe_support_strictTransform_biUnion {X : AlgebraicGeometry.Scheme} [AlgebraicGeometry.IsLocallyNoetherian X] (D : X.IdealSheafData) {ι : Type u_1} (s : Set ι) (hs : s.Finite) (c : ι → X.IdealSheafData) (J : X.IdealSheafData) (hJ : ↑J.support = ⋃ i ∈ s, ↑(c i).support) : ↑(J.strictTransform D).support = ⋃ i ∈ s, ↑((c i).strictTransform D).support

One blow-up (coe_support_strictTransform): if V(J) is the finite union of the V(c i), the strict transform of V(J) is the union of the strict transforms of the V(c i).

theorem Hironaka.Resolution.coe_support_strictTransformSeq_biUnion_mk {X : AlgebraicGeometry.Scheme} (hX : AlgebraicGeometry.IsLocallyNoetherian X) (S : X.BlowUpSequence) {ι : Type u_1} (s : Set ι) (hs : s.Finite) (c : ι → X.IdealSheafData) (J : X.IdealSheafData) (hJ : ↑J.support = ⋃ i ∈ s, ↑(c i).support) (j : ℕ) (hj : j < S.length + 1) : ↑(S.strictTransformSeq J ⟨j, hj⟩).support = ⋃ i ∈ s, ↑(S.strictTransformSeq (c i) ⟨j, hj⟩).support

Along a sequence (⟨j, hj⟩ form): the strict transform of a finite union is the union of the strict transforms.

theorem Hironaka.Resolution.coe_support_strictTransformSeq_biUnion {X : AlgebraicGeometry.Scheme} [hX : AlgebraicGeometry.IsLocallyNoetherian X] (S : X.BlowUpSequence) {ι : Type u_1} (s : Set ι) (hs : s.Finite) (c : ι → X.IdealSheafData) (J : X.IdealSheafData) (hJ : ↑J.support = ⋃ i ∈ s, ↑(c i).support) (i : Fin (S.length + 1)) : ↑(S.strictTransformSeq J i).support = ⋃ l ∈ s, ↑(S.strictTransformSeq (c l) i).support

Along a sequence: the strict transform of a finite union is the union of the strict transforms.

theorem Hironaka.Resolution.strictTransform_mono {X : AlgebraicGeometry.Scheme} (D : X.IdealSheafData) {J K : X.IdealSheafData} (h : J ≤ K) : J.strictTransform D ≤ K.strictTransform D

The strict transform is monotone in the ideal (the saturation of a pull-back is).

theorem Hironaka.Resolution.strictTransformSeq_mono_mk {X : AlgebraicGeometry.Scheme} (S : X.BlowUpSequence) {J K : X.IdealSheafData} (h : J ≤ K) (j : ℕ) (hj : j < S.length + 1) : S.strictTransformSeq J ⟨j, hj⟩ ≤ S.strictTransformSeq K ⟨j, hj⟩

The strict transform along a sequence is monotone in the ideal (⟨j, hj⟩ form).

theorem Hironaka.Resolution.strictTransformSeq_mono {X : AlgebraicGeometry.Scheme} (S : X.BlowUpSequence) {J K : X.IdealSheafData} (h : J ≤ K) (i : Fin (S.length + 1)) : S.strictTransformSeq J i ≤ S.strictTransformSeq K i

The strict transform along a sequence is monotone in the ideal.

theorem Hironaka.Resolution.isReduced_strictTransformSeq_subscheme_mk {X : AlgebraicGeometry.Scheme} (S : X.BlowUpSequence) (J : X.IdealSheafData) (hJ : AlgebraicGeometry.IsReduced J.subscheme) (j : ℕ) (hj : j < S.length + 1) : AlgebraicGeometry.IsReduced (S.strictTransformSeq J ⟨j, hj⟩).subscheme

The strict transform of a reduced closed subscheme along a sequence is reduced (⟨j, hj⟩ form; isReduced_strictTransform_subscheme at each step).

theorem Hironaka.Resolution.isReduced_strictTransformSeq_subscheme {X : AlgebraicGeometry.Scheme} (S : X.BlowUpSequence) (J : X.IdealSheafData) [hJ : AlgebraicGeometry.IsReduced J.subscheme] (i : Fin (S.length + 1)) : AlgebraicGeometry.IsReduced (S.strictTransformSeq J i).subscheme

The strict transform of a reduced closed subscheme along a sequence is reduced.