Base change of a blow-up sequence along a field extension

The change of fields of [Kol07, 34.2]: for a field extension σ : K ↪ L, the L-scheme X_{L,σ} := X_K ×_{Spec K} Spec L and the base-changed sequence (π_i)_{L,σ} with centers (Z_i)_{L,σ}. The base-change data are the predicate Triple.IsBaseChangeOf T' T σ p of Hironaka/Scheme/BlowUpSequence/FunctorVocabulary.lean (the square of p : T'.X.left ⟶ T.X.left, the structure morphisms and Spec σ is cartesian, and I, E pull back), and the base-changed sequence is the pullback S.pullback p of Hironaka/Scheme/BlowUpSequence/Pullback.lean. This module proves the routine transports:

• flat_and_surjective_specMap: Spec σ is flat and surjective, σ being faithfully flat (L is a nonzero free k-module; flat_and_surjective_SpecMap_iff);
• Triple.IsBaseChangeOf.flat, .surjective: so is the projection p of a base-change square (Flat and Surjective are stable under base change);
• Triple.IsBaseChangeOf.isPullback_pullbackStageHom: the stages of S.pullback p are the base changes (X_i)_{L,σ} = X_i ×_{Spec k} Spec L; the stage squares of the pullback (isPullback_pullbackStageHom, for flat p) pasted vertically on the base-change square;
• Triple.IsBaseChangeOf.isSmooth_pullback: the centers (Z_i)_{L,σ} are smooth over L; the closed-subscheme square AlgebraicGeometry.isPullback_subschemeι_comap pasted on the stage square exhibits V((Z_i)_{L,σ}) → Spec L as the base change of V(Z_i) → Spec k, and smoothness is stable under base change;
• Triple.IsBaseChangeOf.noEmptyCenters_pullback: no center becomes empty; the stage lifts of the surjective flat p are surjective (surjective_pullbackStageHom) and the inverse image of a proper ideal sheaf along a surjective morphism is proper (support_comap).

The order along the centers and the simple normal crossings under a field extension, and the construction Triple.baseChange, are in Hironaka/Scheme/BlowUpSequence/BaseChangeOrder.lean, BaseChangeParameters.lean and BaseChangeTriple.lean.

theorem AlgebraicGeometry.flat_and_surjective_specMap {k : Type u} [Field k] {L : Type u} [Field L] (σ : k →+* L) : Flat (Spec.map (CommRingCat.ofHom σ)) ∧ Surjective (Spec.map (CommRingCat.ofHom σ))

Spec σ is flat and surjective for a field extension σ : k → L (Kollár's Spec L → Spec K, "possibly not of finite type", [Kol07, 34.2]): σ is faithfully flat, L being a nonzero free k-module.

theorem AlgebraicGeometry.Triple.IsBaseChangeOf.flat {k : Type u} [Field k] {L : Type u} [Field L] {T : Triple k} {T' : Triple L} {σ : k →+* L} {p : T'.X.left ⟶ T.X.left} (hp : T'.IsBaseChangeOf T σ p) : Flat p

The projection p : X_{L,σ} → X of a base-change square is flat, being the base change of the flat Spec σ.

theorem AlgebraicGeometry.Triple.IsBaseChangeOf.surjective {k : Type u} [Field k] {L : Type u} [Field L] {T : Triple k} {T' : Triple L} {σ : k →+* L} {p : T'.X.left ⟶ T.X.left} (hp : T'.IsBaseChangeOf T σ p) : Function.Surjective ⇑p

The projection of a base-change square is surjective, being the base change of the surjective Spec σ.

theorem AlgebraicGeometry.Triple.IsBaseChangeOf.isPullback_pullbackStageHom {k : Type u} [Field k] {L : Type u} [Field L] {T : Triple k} {T' : Triple L} {σ : k →+* L} {p : T'.X.left ⟶ T.X.left} (hp : T'.IsBaseChangeOf T σ p) (S : T.X.left.BlowUpSequence) (i : Fin (S.length + 1)) : CategoryTheory.IsPullback (S.pullbackStageHom p i) (CategoryTheory.CategoryStruct.comp ((S.pullback p).stageMap (S.pullbackStageIdx p i)) (T'.X.left ↘ Spec ↧L)) (CategoryTheory.CategoryStruct.comp (S.stageMap i) (T.X.left ↘ Spec ↧k)) (Spec.map (CommRingCat.ofHom σ))

The stages of the pulled-back sequence are the base changes (X_i)_{L,σ} of the stages [Kol07, 34.2]: the stage square of the pullback (for flat p) pasted on the base-change square.

theorem AlgebraicGeometry.Triple.IsBaseChangeOf.isSmooth_pullback {k : Type u} [Field k] {L : Type u} [Field L] {T : Triple k} {T' : Triple L} {σ : k →+* L} {p : T'.X.left ⟶ T.X.left} (hp : T'.IsBaseChangeOf T σ p) {S : T.X.left.BlowUpSequence} (hS : S.IsSmooth (T.X.left ↘ Spec ↧k)) : (S.pullback p).IsSmooth (T'.X.left ↘ Spec ↧L)

The base change of a smooth blow-up sequence is smooth over L (the centers (Z_i)_{L,σ} of [Kol07, 34.2]): V((Z_i)_{L,σ}) → Spec L is the base change of V(Z_i) → Spec k along Spec σ (the closed-subscheme square pasted on the stage square), and smoothness is stable under base change.

theorem AlgebraicGeometry.Triple.IsBaseChangeOf.noEmptyCenters_pullback {k : Type u} [Field k] {L : Type u} [Field L] {T : Triple k} {T' : Triple L} {σ : k →+* L} {p : T'.X.left ⟶ T.X.left} (hp : T'.IsBaseChangeOf T σ p) {S : T.X.left.BlowUpSequence} (hS : S.NoEmptyCenters) : (S.pullback p).NoEmptyCenters

Base change along a field extension creates no empty center ([Kol07, 34.2] displays every center, none deleted): the stage lifts of the surjective flat p are surjective, and the inverse image of a proper ideal sheaf along a surjective morphism is proper.