The exceptional divisor under a flat base change

The smoothness of F → Z of relative dimension r − 1 for a smooth blow-up over an arbitrary field k (Hironaka/Scheme/Smooth/ExceptionalDivisorSmooth.lean) is obtained from its perfect-field form (Hironaka/Scheme/Smooth/ExceptionalDivisor.lean) by base change to a perfect extension field K of k and descent along Spec K → Spec k (Hironaka/Scheme/Smooth/DescentRelativeDimension.lean). This file is the base-change bookkeeping.

Why the lemmas hold. Blowing up commutes with flat base change ([TSPA, Tag 0805]: for flat h : Y ⟶ X, B_{h⁻¹Z} Y = Y ×_X B_Z X, the square isPullback_blowUpMap). The exceptional divisor of B_{h⁻¹Z} Y is the inverse image of that of B_Z X along the projection (inverse images of ideal sheaves compose and the square commutes), so the exceptional divisors form a cartesian square over h, and, cancelling the square h⁻¹Z = Y ×_X Z of the centers from the bottom, F_Y → Z_Y is the base change of F → Z along Z_Y → Z (isPullback_exceptionalMap_of_flat). For Y = X ×_k K with K/k a field extension: X_K → Spec K is smooth of relative dimension n and Z_K → Spec K of relative dimension n − r as base changes (Mathlib's smoothOfRelativeDimension_isStableUnderBaseChange), and Z_K → Z is surjective, flat and quasi-compact as the base change of Spec K → Spec k (every morphism to Spec k is flat, flat_of_field, stalkwise since a ring map out of a ring isomorphic to a field is flat, RingHom.Flat.of_ringEquiv_field; Spec of a field extension is surjective between one-point spaces and affine).

Main declarations

• AlgebraicGeometry.comap_π_comap_eq_comap_blowUpMap: the exceptional divisor of the base-changed blow-up is the inverse image of F along blowUpMap.
• AlgebraicGeometry.isPullback_exceptionalMap_of_flat: F_Y → Z_Y is the base change of F → Z.
• AlgebraicGeometry.smoothOfRelativeDimension_pullback_snd_fieldExtension, isPullback_subschemeMap_comap_fst, smoothOfRelativeDimension_subschemeι_comap_fst_comp, fpqcCover_subschemeMap_comap_fst: the field-extension base change.
• AlgebraicGeometry.smoothOfRelativeDimension_subschemeMap_exceptional_of_descendsAlong: the smoothness of F → Z over any field from its perfect-field form, given the descent of smoothness of relative dimension r − 1 along fpqc coverings as a hypothesis (supplied by descendsAlong_smoothOfRelativeDimension where the two are combined).

theorem RingHom.Flat.of_ringEquiv_field {k : Type u_1} {A : Type u_2} {B : Type u_3} [Field k] [CommRing A] [CommRing B] (e : k ≃+* A) (φ : A →+* B) : φ.Flat

A ring map out of a ring isomorphic to a field is flat: every vector space is free, and flatness passes along the isomorphism.

theorem AlgebraicGeometry.flat_of_field {k : Type u} [Field k] {Z : Scheme} (f : Z ⟶ Spec ↧k) : Flat f

Every morphism to the spectrum of a field is flat: at each point the stalk of Spec k is k (isIso_toStalk_Spec_of_field) and a ring map out of a field is flat. This is the hypothesis under which Hauser's product formula over a field [Hau14, Corollary 5.2 (e)] is flat base change along the projection.

theorem AlgebraicGeometry.comap_π_comap_eq_comap_blowUpMap {X Y : Scheme} (h : Y ⟶ X) (Z : X.IdealSheafData) : (Z.comap h).comap (Z.comap h).blowUpπ = (Z.comap Z.blowUpπ).comap (Scheme.Hom.blowUpMap h Z)

The exceptional divisor of B_{h⁻¹Z} Y is the inverse image of the exceptional divisor of B_Z X along blowUpMap h Z (π_Y ≫ h = blowUpMap ≫ π, and inverse images compose).

theorem AlgebraicGeometry.le_map_exceptional_blowUpMap {X Y : Scheme} (h : Y ⟶ X) (Z : X.IdealSheafData) : Z.comap Z.blowUpπ ≤ ((Z.comap h).comap (Z.comap h).blowUpπ).map (Scheme.Hom.blowUpMap h Z)

F ≤ (blowUpMap h Z)_* F_Y.

theorem AlgebraicGeometry.isPullback_subschemeMap_comap {X Y : Scheme} (h : Y ⟶ X) (Z : X.IdealSheafData) : CategoryTheory.IsPullback ((Z.comap h).subschemeMap Z h ⋯) (Z.comap h).subschemeι Z.subschemeι h

The centres form a cartesian square: h⁻¹Z = Y ×_X Z.

theorem AlgebraicGeometry.isPullback_exceptionalMap_of_flat {X Y : Scheme} (h : Y ⟶ X) (Z : X.IdealSheafData) [Flat h] : CategoryTheory.IsPullback (((Z.comap h).comap (Z.comap h).blowUpπ).subschemeMap (Z.comap h) (Z.comap h).blowUpπ ⋯) (((Z.comap h).comap (Z.comap h).blowUpπ).subschemeMap (Z.comap Z.blowUpπ) (Scheme.Hom.blowUpMap h Z) ⋯) ((Z.comap h).subschemeMap Z h ⋯) ((Z.comap Z.blowUpπ).subschemeMap Z Z.blowUpπ ⋯)

For flat h : Y ⟶ X, the map F_Y → Z_Y of the base-changed blow-up is the base change of F → Z along Z_Y = h⁻¹Z → Z (blow-ups commute with flat base change, [TSPA, Tag 0805]).

@[reducible, inline]

noncomputable abbrev AlgebraicGeometry.specMapField (k K : Type u) [Field k] [Field K] [Algebra k K] : Spec ↧K ⟶ Spec ↧k

Spec K → Spec k for a field extension K/k.

Equations

• AlgebraicGeometry.specMapField k K = AlgebraicGeometry.Spec.map (CommRingCat.ofHom (algebraMap k K))

theorem AlgebraicGeometry.flat_pullback_fst_fieldExtension {k K : Type u} [Field k] [Field K] [Algebra k K] {X : Scheme} (f : X ⟶ Spec ↧k) : Flat (CategoryTheory.Limits.pullback.fst f (specMapField k K))

Every morphism to Spec k is flat, in particular the base change X_K → X.

theorem AlgebraicGeometry.smoothOfRelativeDimension_pullback_snd_fieldExtension {k K : Type u} [Field k] [Field K] [Algebra k K] {X : Scheme} (f : X ⟶ Spec ↧k) (n : ℕ) [SmoothOfRelativeDimension n f] : SmoothOfRelativeDimension n (CategoryTheory.Limits.pullback.snd f (specMapField k K))

X_K → Spec K is smooth of relative dimension n when X → Spec k is.

theorem AlgebraicGeometry.isPullback_subschemeMap_comap_fst {k K : Type u} [Field k] [Field K] [Algebra k K] {X : Scheme} (f : X ⟶ Spec ↧k) (Z : X.IdealSheafData) : CategoryTheory.IsPullback (CategoryTheory.CategoryStruct.comp (Z.comap (CategoryTheory.Limits.pullback.fst f (specMapField k K))).subschemeι (CategoryTheory.Limits.pullback.snd f (specMapField k K))) ((Z.comap (CategoryTheory.Limits.pullback.fst f (specMapField k K))).subschemeMap Z (CategoryTheory.Limits.pullback.fst f (specMapField k K)) ⋯) (specMapField k K) (CategoryTheory.CategoryStruct.comp Z.subschemeι f)

Z_K → Spec K is the base change of Z → Spec k along Spec K → Spec k.

theorem AlgebraicGeometry.smoothOfRelativeDimension_subschemeι_comap_fst_comp {k K : Type u} [Field k] [Field K] [Algebra k K] {X : Scheme} (f : X ⟶ Spec ↧k) (n r : ℕ) (Z : X.IdealSheafData) [SmoothOfRelativeDimension (n - r) (CategoryTheory.CategoryStruct.comp Z.subschemeι f)] : SmoothOfRelativeDimension (n - r) (CategoryTheory.CategoryStruct.comp (Z.comap (CategoryTheory.Limits.pullback.fst f (specMapField k K))).subschemeι (CategoryTheory.Limits.pullback.snd f (specMapField k K)))

Z_K → Spec K is smooth of relative dimension n − r when Z → Spec k is.

@[reducible, inline]

abbrev AlgebraicGeometry.fpqcCover : CategoryTheory.MorphismProperty Scheme

The property surjective, flat and quasi-compact of Mathlib's descent instances (Mathlib/AlgebraicGeometry/Morphisms/LocalFlatDescent.lean): an fpqc covering by one morphism.

Equations

• AlgebraicGeometry.fpqcCover = @AlgebraicGeometry.Surjective ⊓ @AlgebraicGeometry.Flat ⊓ @AlgebraicGeometry.QuasiCompact

theorem AlgebraicGeometry.surjective_specMapField {k K : Type u} [Field k] [Field K] [Algebra k K] : Surjective (specMapField k K)

Spec K → Spec k is surjective: both spaces are points.

theorem AlgebraicGeometry.fpqcCover_specMapField {k K : Type u} [Field k] [Field K] [Algebra k K] : fpqcCover (specMapField k K)

Spec K → Spec k is surjective, flat and quasi-compact: an fpqc covering.

theorem AlgebraicGeometry.fpqcCover_subschemeMap_comap_fst {k K : Type u} [Field k] [Field K] [Algebra k K] {X : Scheme} (f : X ⟶ Spec ↧k) (Z : X.IdealSheafData) : fpqcCover ((Z.comap (CategoryTheory.Limits.pullback.fst f (specMapField k K))).subschemeMap Z (CategoryTheory.Limits.pullback.fst f (specMapField k K)) ⋯)

Z_K → Z is surjective, flat and quasi-compact, as the base change of Spec K → Spec k (each of the three properties is stable under base change; the meet is assembled by hand rather than through the base-change instance of the meet).

theorem AlgebraicGeometry.smoothOfRelativeDimension_subschemeMap_exceptional_of_descendsAlong {k : Type u} [Field k] {X : Scheme} (f : X ⟶ Spec ↧k) (n r : ℕ) [SmoothOfRelativeDimension n f] (Z : X.IdealSheafData) [SmoothOfRelativeDimension (n - r) (CategoryTheory.CategoryStruct.comp Z.subschemeι f)] (hrn : r ≤ n) (hdesc : CategoryTheory.MorphismProperty.DescendsAlong (@SmoothOfRelativeDimension (r - 1)) fpqcCover) : SmoothOfRelativeDimension (r - 1) ((Z.comap Z.blowUpπ).subschemeMap Z Z.blowUpπ ⋯)

If smoothness of relative dimension r − 1 descends along fpqc coverings, then for a smooth blow-up over any field k the map F → Z from the exceptional divisor to the center is smooth of relative dimension r − 1 (the smoothness of F in [Kol07, Notation 19], relative to Z): base change along Spec K → Spec k for K the algebraic closure of k (perfect, so the perfect-field form applies to F_K → Z_K), the square isPullback_exceptionalMap_of_flat, and descent along the surjective, flat, quasi-compact Z_K → Z.