Blow-ups of reduced schemes are reduced; the strict transform of a reduced subscheme is reduced

The chart rings Γ(X, U)[I(U)/a] of the blow-up are subalgebras of the localizations Γ(X, U)_a (affineBlowUpAlgebra), hence reduced when X is; the charts cover blowUp I, so blowUp I is reduced [TSPA, Tag 0808]. The strict transform of a closed subscheme V(J) is the blow-up of V(J) along the restricted centre [TSPA, Tag 080E], hence reduced when V(J) is. These are used for the generic points of the strict transforms in the resolution of a reduced scheme, where the strict transform of a component is again integral [Kol07, Corollary 22, proof].

Conventions

D.blowUp and D.blowUpπ are the blow-up along D and its projection, D.exceptionalDivisor is D.comap D.blowUpπ, and J.strictTransform D is strictTransformAlong (D.blowUpπ) (D.exceptionalDivisor) J.

Reduced chart rings

instance AlgebraicGeometry.isReduced_affineBlowUpAlgebra {R : Type u} [CommRing R] [_root_.IsReduced R] (I : Ideal R) (a : R) : _root_.IsReduced ↥(affineBlowUpAlgebra I a)

The chart ring R[I/a] is a subalgebra of R_a (affineBlowUpAlgebra), hence reduced when R is (localizations of reduced rings are reduced).

The blow-up of a reduced scheme is reduced

theorem AlgebraicGeometry.Scheme.IdealSheafData.blowUp.isReduced {X : Scheme} (I : X.IdealSheafData) [IsReduced X] : IsReduced I.blowUp

The blow-up of a reduced scheme is reduced [TSPA, Tag 0808] — every point lies in a chart Spec Γ(X, U)[I(U)/a] (blowUp.iUnion_range_chart), an open immersion, and the chart ring is reduced.

The strict transform of a reduced closed subscheme is reduced

theorem AlgebraicGeometry.isReduced_strictTransformAlong_subscheme {X : Scheme} (D J : X.IdealSheafData) [IsReduced J.subscheme] : IsReduced (J.strictTransformAlong D.blowUpπ (D.comap D.blowUpπ)).subscheme

The strict transform V(Jˢ) ⊆ blowUp D of a reduced closed subscheme V(J) is isomorphic to the blow-up of V(J) along the restricted centre (exists_iso_strictTransform_subscheme) [TSPA, Tag 080E], which is reduced.

theorem AlgebraicGeometry.isReduced_strictTransform_subscheme {X : Scheme} (D J : X.IdealSheafData) [IsReduced J.subscheme] : IsReduced (J.strictTransform D).subscheme

The strict transform J.strictTransform D of the vocabulary of the main theorems, of a reduced closed subscheme, is reduced.