The base change of a triple and of a smooth blow-up sequence along a field extension

[Kol07, 34.2]: the base change of a triple along σ : K ↪ L is the fiber product X_{L,σ} := X_K ×_{Spec K} Spec L, "an L-scheme of finite type", with the ideal I_{L,σ} and the divisor E_{L,σ} obtained similarly; the change of fields "will hold automatically for all blow-up sequence functors that we construct". This module provides

• the base change AlgebraicGeometry.Triple.baseChange T σ : Triple L of a triple: the fibre product pullback (T.X.left ↘ Spec k) (Spec.map σ) over L through its second projection, with T.I and T.E pulled back along the first. Every field but simple normal crossings is base-change stability (the IsStableUnderBaseChange instances through property_of_isPullback; nonvanishing on components by flat pullback); the simple normal crossing field is isSnc_comap_of_isPullback_specMap of Hironaka/Scheme/BlowUpSequence/BaseChangeParameters.lean. The construction carries the base-change data IsBaseChangeOf through the first projection (isBaseChangeOf_baseChange); the marked version keeps the mark;
• the base change S.pullback p of a smooth blow-up sequence of order m (resp. ≥ m) starting with (X, I, E) is one starting with (X_{L,σ}, I_{L,σ}, E_{L,σ}) (Triple.IsBaseChangeOf.isOrderSeq_pullback, MarkedTriple.IsBaseChangeOf.isOrderGeSeq_pullback), stage by stage as for a smooth pullback: the centers are the inverse images of the centers, the induced families and ideals the inverse images of the induced ones (totalTransformSeq_pullback for E, the transports of Hironaka/Scheme/BlowUpSequence/BaseChangeOrder.lean for I), simple normal crossings and the order transport along the stage lifts through the stage squares of Hironaka/Scheme/BlowUpSequence/BaseChange.lean; and the induced data are the base change of the induced data (induced_isBaseChangeOf);
• the corresponding statement for the pullback along a smooth morphism (IsPullbackOf.induced_isPullbackOf) and two transports along an equality of stage indices.

The base change of a triple

noncomputable def AlgebraicGeometry.Triple.baseChange {k : Type u} [Field k] {L : Type u} [Field L] [CharZero k] (T : Triple k) (σ : k →+* L) : Triple L

The base change of a triple over k along σ : k →+* L [Kol07, 34.2]: the fibre product pullback (T.X.left ↘ Spec k) (Spec.map σ) over L through its second projection, with the inverse images of T.I and T.E along the first projection. Finite type, quasi-compactness, separatedness, smoothness and the relative dimension over L are base-change stability; nonvanishing on components is flat pullback; simple normal crossings is isSnc_comap_of_isPullback_specMap.

Equations

• One or more equations did not get rendered due to their size.

theorem AlgebraicGeometry.Triple.baseChange_X {k : Type u} [Field k] {L : Type u} [Field L] [CharZero k] (T : Triple k) (σ : k →+* L) : (T.baseChange σ).X.left = CategoryTheory.Limits.pullback (T.X.left ↘ Spec ↧k) (Spec.map (CommRingCat.ofHom σ))

The ambient scheme of the base change is the fibre product.

theorem AlgebraicGeometry.Triple.isBaseChangeOf_baseChange {k : Type u} [Field k] {L : Type u} [Field L] [CharZero k] (T : Triple k) (σ : k →+* L) : (T.baseChange σ).IsBaseChangeOf T σ (CategoryTheory.Limits.pullback.fst (T.X.left ↘ Spec ↧k) (Spec.map (CommRingCat.ofHom σ)))

The base change of T carries the base-change data of T (IsBaseChangeOf) through the first projection.

noncomputable def Hironaka.MarkedTriple.baseChange {k : Type u} [Field k] {L : Type u} [Field L] [CharZero k] (T : MarkedTriple k) (σ : k →+* L) : MarkedTriple L

The base change of a marked triple, the mark unchanged ([Kol07, 34.2]; the pair (I, m) is one item, footnote to [Kol07, Notation 64]).

Equations

• T.baseChange σ = { toTriple := T.baseChange σ, m := T.m }

theorem Hironaka.MarkedTriple.isBaseChangeOf_baseChange {k : Type u} [Field k] {L : Type u} [Field L] [CharZero k] (T : MarkedTriple k) (σ : k →+* L) : (T.baseChange σ).IsBaseChangeOf T σ (CategoryTheory.Limits.pullback.fst (T.X.left ↘ AlgebraicGeometry.Spec ↧k) (AlgebraicGeometry.Spec.map (CommRingCat.ofHom σ)))

The base change of a marked triple carries the base-change data, with the same mark.

The base change of a smooth blow-up sequence of order m

theorem AlgebraicGeometry.Triple.IsBaseChangeOf.isOrderSeq_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} [CharZero k] (hp : T'.IsBaseChangeOf T σ p) {S : T.X.left.BlowUpSequence} {m : ℕ} (hS : S.IsOrderSeq (T.X.left ↘ Spec ↧k) T.I T.E m) : (S.pullback p).IsOrderSeq (T'.X.left ↘ Spec ↧L) T'.I T'.E m

The base change of a smooth blow-up sequence of order m starting with (X, I, E) is one starting with (X_{L,σ}, I_{L,σ}, E_{L,σ}) [Kol07, 34.2]; the analogue of IsOrderSeq.pullback_of_equidim for the base change: smoothness of the centers by isSmooth_pullback, simple normal crossings by hasSncWith_comap_of_isPullback_specMap and the order by ordAlongEq_comap_of_isPullback_specMap, both through the stage squares.

theorem AlgebraicGeometry.Triple.IsBaseChangeOf.induced_isBaseChangeOf {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} [CharZero k] [CharZero L] (hp : T'.IsBaseChangeOf T σ p) {S : T.X.left.BlowUpSequence} {m : ℕ} (hS : S.IsOrderSeq (T.X.left ↘ Spec ↧k) T.I T.E m) (hS' : (S.pullback p).IsOrderSeq (T'.X.left ↘ Spec ↧L) T'.I T'.E m) (i : Fin (S.length + 1)) : (T'.induced (S.pullback p) hS' (S.pullbackStageIdx p i)).IsBaseChangeOf (T.induced S hS i) σ (S.pullbackStageHom p i)

The triple induced at stage i of the base-changed sequence (Kol07, Definition 66, condition (1)) carries the base-change data of the triple induced at stage i of S, through the stage lift: the stage square, the weak-transform identity IsOrderSeq.weakTransformSeq_pullback_of_isPullback_specMap and totalTransformSeq_pullback.

The marked form

theorem Hironaka.MarkedTriple.IsBaseChangeOf.isOrderGeSeq_pullback {k : Type u} [Field k] {L : Type u} [Field L] {T : MarkedTriple k} {T' : MarkedTriple L} {σ : k →+* L} {p : T'.X.left ⟶ T.X.left} [CharZero k] (hp : T'.IsBaseChangeOf T σ p) {S : T.X.left.BlowUpSequence} (hS : S.IsOrderGeSeq (T.X.left ↘ AlgebraicGeometry.Spec ↧k) T.I T.m T.E) : (S.pullback p).IsOrderGeSeq (T'.X.left ↘ AlgebraicGeometry.Spec ↧L) T'.I T'.m T'.E

The base change of a smooth blow-up sequence of order ≥ m starting with (X, I, m, E) is one starting with (X_{L,σ}, I_{L,σ}, m, E_{L,σ}) ([Kol07, 34.2]; conditions (2′)–(4′) of [Kol07, Definition 66]): the ≥ m condition transports along the flat stage lifts (leOrdAlong_comap_of_flat), simple normal crossings by hasSncWith_comap_of_isPullback_specMap, the marked transforms by markedTransformSeq_pullback_mk_of_flat.

theorem Hironaka.MarkedTriple.IsBaseChangeOf.induced_isBaseChangeOf {k : Type u} [Field k] {L : Type u} [Field L] {T : MarkedTriple k} {T' : MarkedTriple L} {σ : k →+* L} {p : T'.X.left ⟶ T.X.left} [CharZero k] [CharZero L] (hp : T'.IsBaseChangeOf T σ p) {S : T.X.left.BlowUpSequence} (hS : S.IsOrderGeSeq (T.X.left ↘ AlgebraicGeometry.Spec ↧k) T.I T.m T.E) (hS' : (S.pullback p).IsOrderGeSeq (T'.X.left ↘ AlgebraicGeometry.Spec ↧L) T'.I T'.m T'.E) (i : Fin (S.length + 1)) : (T'.induced (S.pullback p) hS' (S.pullbackStageIdx p i)).IsBaseChangeOf (T.induced S hS i) σ (S.pullbackStageHom p i)

The marked triple induced at stage i of the base-changed sequence (Kol07, Definition 66, condition (1′)) carries the base-change data, with the same mark, of the one induced at stage i of S, through the stage lift.

The induced triple of a pulled-back sequence carries the pullback data

The analogues of induced_isBaseChangeOf above for the pullback along a smooth morphism, beside inducedTriple_pullback of Hironaka/Scheme/BlowUpSequence/PullbackInduced.lean.

theorem AlgebraicGeometry.Triple.IsPullbackOf.induced_isPullbackOf {k : Type u} [Field k] [CharZero k] {T T' : Triple k} {h : T'.X.left ⟶ T.X.left} [Smooth h] (hp : T'.IsPullbackOf T h) {S : T.X.left.BlowUpSequence} {m : ℕ} (hS : S.IsOrderSeq (T.X.left ↘ Spec ↧k) T.I T.E m) (hS' : (S.pullback h).IsOrderSeq (T'.X.left ↘ Spec ↧k) T'.I T'.E m) (i : Fin (S.length + 1)) : (T'.induced (S.pullback h) hS' (S.pullbackStageIdx h i)).IsPullbackOf (T.induced S hS i) (S.pullbackStageHom h i)

The triple induced at stage i of the pulled-back sequence carries the pullback data of the triple induced at stage i, along the stage lift (inducedTriple_pullback as an IsPullbackOf).

theorem AlgebraicGeometry.Triple.isPullbackOf_induced_of_eq_idx {k : Type u} [Field k] [CharZero k] {T' : Triple k} {S' : T'.X.left.BlowUpSequence} {m : ℕ} {hS' : S'.IsOrderSeq (T'.X.left ↘ Spec ↧k) T'.I T'.E m} {i j : Fin (S'.length + 1)} (e : i = j) {R : Triple k} {q : S'.stage i ⟶ R.X.left} (hq : (T'.induced S' hS' i).IsPullbackOf R q) : (T'.induced S' hS' j).IsPullbackOf R (CategoryTheory.CategoryStruct.comp (CategoryTheory.eqToHom ⋯) q)

Transport of pullback data of an induced triple along an equality of stage indices: the eqToHom of the stage identification is absorbed.

theorem AlgebraicGeometry.Triple.isBaseChangeOf_induced_of_eq_idx {k : Type u} [Field k] {L : Type u} [Field L] [CharZero L] {T' : Triple L} {S' : T'.X.left.BlowUpSequence} {m : ℕ} {hS' : S'.IsOrderSeq (T'.X.left ↘ Spec ↧L) T'.I T'.E m} {i j : Fin (S'.length + 1)} (e : i = j) {R : Triple k} {σ : k →+* L} {q : S'.stage i ⟶ R.X.left} (hq : (T'.induced S' hS' i).IsBaseChangeOf R σ q) : (T'.induced S' hS' j).IsBaseChangeOf R σ (CategoryTheory.CategoryStruct.comp (CategoryTheory.eqToHom ⋯) q)

Transport of base-change data of an induced triple along an equality of stage indices.