Clause (2) of marked order reduction: change of fields

Clause (2) of [Kol07, Theorem 107] with [Kol07, 34.2]: for a field extension σ : k → L and the base-changed marked triple (X_L, I_L, m, E_L) along the projection p : X_L → X, BMO_{n,m}(X_L, I_L, m, E_L) = p^* BMO_{n,m}(X, I, m, E); no blow-up is deleted, the projection being surjective on points. The proof is the change-of-fields form of the argument for smooth surjections (Hironaka/Resolution/Algebraic/MarkedOrderReduction/LoopFunctorial.lean, Step3Functorial.lean, Functoriality.lean): the round parameters are preserved (roundOrder_of_isBaseChangeOf, sepOrder_of_isBaseChangeOf), each round commutes by the second half of clause (2) of [Kol07, Theorem 103] (BOData.commutesWithBaseChange) on the base-changed round triple, the marked triple induced at the end of the base-changed round carries the base-change data of the one induced at the end of the round along the last-stage lift (MarkedTriple.isBaseChangeOf_induced_last), the loops follow by induction over the well-founded recursions, and Step 3 is realize_pullback_of_isBaseChangeOf (Hironaka/Resolution/Algebraic/Monomial/Geometric/BaseChangeRealize.lean) on the refining family refinesAlong_ofDivisorFamily in its flat form; the exponents agree at the generic points because the order is preserved pointwise by a change of fields (ord_comap_of_isBaseChangeOf).

theorem Hironaka.MarkedTriple.isBaseChangeOf_induced_of_eq_idx {k : Type u} [Field k] {L : Type u} [Field L] [CharZero L] {T' : MarkedTriple L} {S' : T'.X.left.BlowUpSequence} {hS' : S'.IsOrderGeSeq (T'.X.left ↘ AlgebraicGeometry.Spec ↧L) T'.I T'.m T'.E} {i j : Fin (S'.length + 1)} (e : i = j) {R : MarkedTriple 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 marked triple along an equality of stage indices (the marked form of Triple.isBaseChangeOf_induced_of_eq_idx).

theorem Hironaka.MarkedTriple.isBaseChangeOf_induced_last {k : Type u} [Field k] {L : Type u} [Field L] [CharZero k] [CharZero L] {T : MarkedTriple k} {T' : MarkedTriple L} {σ : k →+* L} (p : T'.X.left ⟶ T.X.left) (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) : (T'.induced (S.pullback p) hS' (Fin.last (S.pullback p).length)).IsBaseChangeOf (T.induced S hS (Fin.last S.length)) σ (S.pullbackLastHom p)

The marked triple induced at the end of the base-changed sequence is the base change of the marked triple induced at the end of the sequence, along the last-stage lift ([Kol07, 34.2]; the marked form of isBaseChangeOf_induced_last).

theorem Hironaka.MarkedTriple.isBaseChangeOf_induced_of_eq_seq {k : Type u} [Field k] {L : Type u} [Field L] [CharZero L] {T' : MarkedTriple L} {S S' : T'.X.left.BlowUpSequence} (e : S = S') {hS : S.IsOrderGeSeq (T'.X.left ↘ AlgebraicGeometry.Spec ↧L) T'.I T'.m T'.E} {hS' : S'.IsOrderGeSeq (T'.X.left ↘ AlgebraicGeometry.Spec ↧L) T'.I T'.m T'.E} {R : MarkedTriple k} {σ : k →+* L} {q : S'.last ⟶ R.X.left} (hq : (T'.induced S' hS' (Fin.last S'.length)).IsBaseChangeOf R σ q) : (T'.induced S hS (Fin.last S.length)).IsBaseChangeOf R σ (CategoryTheory.CategoryStruct.comp (CategoryTheory.eqToHom ⋯) q)

Transport of base-change data of the last induced marked triple along an equality of sequences: the eqToHom of the last-stage identification is absorbed.

theorem Hironaka.BMO.nonmonomialTriple_isBaseChangeOf {k : Type u} [Field k] [CharZero k] {L : Type u} [Field L] [CharZero L] (T : MarkedTriple k) (T' : MarkedTriple L) (σ : k →+* L) (p : T'.X.left ⟶ T.X.left) (hbc : T'.IsBaseChangeOf T σ p) : (nonmonomialTriple T').IsBaseChangeOf (nonmonomialTriple T) σ p

The round triple (X, N(I), E) of the base-changed data is the base change of the round triple, since N(I_L) = p^* N(I).

theorem Hironaka.BMO.step1Round_baseChange {k : Type u} [Field k] [CharZero k] {L : Type u} [Field L] [CharZero L] {n m : ℕ} (bo : (d : ℕ) → BOData n d) (T : MarkedTriple k) (T' : MarkedTriple L) (σ : k →+* L) (p : T'.X.left ⟶ T.X.left) (hbc : T'.IsBaseChangeOf T σ p) (hT : MarkedTriple.BMOClass n m T) (hT' : MarkedTriple.BMOClass n m T') (hd : m ≤ roundOrder T) (hd' : m ≤ roundOrder T') : step1Round bo T' hT' hd' = (step1Round bo T hT hd).pullback p

A round of Step 1 commutes with a change of fields (clause (2) of [Kol07, Theorem 103] with [Kol07, 34.2], per round): the round order is preserved and BO_{n,d} commutes on the base-changed round triple.

theorem Hironaka.BMO.step1_baseChange_aux {k : Type u} [Field k] [CharZero k] {L : Type u} [Field L] [CharZero L] {n m : ℕ} (bo : (d : ℕ) → BOData n d) (σ : k →+* L) (l : ℕ) (T : MarkedTriple k) (T' : MarkedTriple L) (p : T'.X.left ⟶ T.X.left) : T'.IsBaseChangeOf T σ p → ∀ (hT : MarkedTriple.BMOClass n m T) (hT' : MarkedTriple.BMOClass n m T'), roundOrder T ≤ l → ↑(step1 bo T' hT') = (↑(step1 bo T hT)).pullback p

The induction behind step1_baseChange: on a bound l for the loop variable, following the recursion of step1.

theorem Hironaka.BMO.step1_baseChange {k : Type u} [Field k] [CharZero k] {L : Type u} [Field L] [CharZero L] {n m : ℕ} (bo : (d : ℕ) → BOData n d) (T : MarkedTriple k) (T' : MarkedTriple L) (σ : k →+* L) (p : T'.X.left ⟶ T.X.left) (hbc : T'.IsBaseChangeOf T σ p) (hT : MarkedTriple.BMOClass n m T) (hT' : MarkedTriple.BMOClass n m T') : ↑(step1 bo T' hT') = (↑(step1 bo T hT)).pullback p

Step 1 commutes with a change of fields ([Kol07, 34.2] for Step 1): round by round through the loop, by clause (2) of [Kol07, Theorem 103] on the base-changed round triples.

theorem Hironaka.BMO.sepTriple_isBaseChangeOf {k : Type u} [Field k] [CharZero k] {L : Type u} [Field L] [CharZero L] (T : MarkedTriple k) (T' : MarkedTriple L) (σ : k →+* L) (p : T'.X.left ⟶ T.X.left) (hbc : T'.IsBaseChangeOf T σ p) : (sepTriple T').IsBaseChangeOf (sepTriple T) σ p

The separating triple (X, N(I)^m + I^s, E) of the base-changed data is the base change of the separating triple: N(I_L) = p^* N(I), the separation order is preserved, and the inverse image commutes with sums and powers.

theorem Hironaka.BMO.step2Round_baseChange {k : Type u} [Field k] [CharZero k] {L : Type u} [Field L] [CharZero L] {n m : ℕ} (bo : (d : ℕ) → BOData n d) (T : MarkedTriple k) (T' : MarkedTriple L) (σ : k →+* L) (p : T'.X.left ⟶ T.X.left) (hbc : T'.IsBaseChangeOf T σ p) (hT : MarkedTriple.BMOClass n m T) (hT' : MarkedTriple.BMOClass n m T') (hpos : 0 < sepOrder T) (hpos' : 0 < sepOrder T') : step2Round bo T' hT' hpos' = (step2Round bo T hT hpos).pullback p

A round of Step 2 commutes with a change of fields (clause (2) of [Kol07, Theorem 103] with [Kol07, 34.2], per round): the separation order is preserved and BO_{n,ms} commutes on the base-changed separating triple.

theorem Hironaka.BMO.step2_baseChange_aux {k : Type u} [Field k] [CharZero k] {L : Type u} [Field L] [CharZero L] {n m : ℕ} (bo : (d : ℕ) → BOData n d) (σ : k →+* L) (l : ℕ) (T : MarkedTriple k) (T' : MarkedTriple L) (p : T'.X.left ⟶ T.X.left) : T'.IsBaseChangeOf T σ p → ∀ (hT : MarkedTriple.BMOClass n m T) (hT' : MarkedTriple.BMOClass n m T'), sepOrder T ≤ l → ↑(step2 bo T' hT') = (↑(step2 bo T hT)).pullback p

The induction behind step2_baseChange: on a bound l for the separation order, following the recursion of step2.

theorem Hironaka.BMO.step2_baseChange {k : Type u} [Field k] [CharZero k] {L : Type u} [Field L] [CharZero L] {n m : ℕ} (bo : (d : ℕ) → BOData n d) (T : MarkedTriple k) (T' : MarkedTriple L) (σ : k →+* L) (p : T'.X.left ⟶ T.X.left) (hbc : T'.IsBaseChangeOf T σ p) (hT : MarkedTriple.BMOClass n m T) (hT' : MarkedTriple.BMOClass n m T') : ↑(step2 bo T' hT') = (↑(step2 bo T hT)).pullback p

Step 2 commutes with a change of fields ([Kol07, 34.2] for Step 2): round by round through the loop, by clause (2) of [Kol07, Theorem 103] on the base-changed separating triples.

theorem Hironaka.BMO.step3Seq_baseChange {k : Type u} [Field k] [CharZero k] {L : Type u} [Field L] [CharZero L] {n m : ℕ} (T : MarkedTriple k) (T' : MarkedTriple L) (σ : k →+* L) (p : T'.X.left ⟶ T.X.left) (hbc : T'.IsBaseChangeOf T σ p) (hT : MarkedTriple.BMOClass n m T) (hT' : MarkedTriple.BMOClass n m T') : step3Seq T' hT' = (step3Seq T hT).pullback p

The geometric Step 3 of a marked triple commutes with a change of fields ([Kol07, 34.2] for Step 3; realize_pullback_of_isBaseChangeOf with refinesAlong_ofDivisorFamily in its flat form): Step 3's input family on X_L is the refining family up to the exponents, which agree at the generic points of the components since the projection is flat (it sends generic points to generic points) and preserves the order at every point (ord_comap_of_isBaseChangeOf); the enumeration σ' of the components of E_L is Step 3's own.

theorem Hironaka.BMO.tailAfterStep2_baseChange {k : Type u} [Field k] [CharZero k] {n m : ℕ} {L : Type u} [Field L] [CharZero L] (T : MarkedTriple k) (T' : MarkedTriple L) (σ : k →+* L) (p : T'.X.left ⟶ T.X.left) (hbc : T'.IsBaseChangeOf T σ p) (hT : MarkedTriple.BMOClass n m T) (hT' : MarkedTriple.BMOClass n m T') (τ : { R : T.X.left.BlowUpSequence // R.IsOrderGeSeq (T.X.left ↘ AlgebraicGeometry.Spec ↧k) T.I T.m T.E ∧ R.NoEmptyCenters }) (τ' : { R : T'.X.left.BlowUpSequence // R.IsOrderGeSeq (T'.X.left ↘ AlgebraicGeometry.Spec ↧L) T'.I T'.m T'.E ∧ R.NoEmptyCenters }) (e : ↑τ' = (↑τ).pullback p) : tailAfterStep2 T' hT' τ' = (tailAfterStep2 T hT τ).pullback p

The tail after Step 2 under a change of fields: the change-of-fields form of tailAfterStep2_pullback, Step 3 by step3Seq_baseChange on the marked triples induced after Step 2 along the last-stage lift.

theorem Hironaka.BMO.tailAfterStep1_baseChange {k : Type u} [Field k] [CharZero k] {n : ℕ} (bo : (d : ℕ) → BOData n d) {m : ℕ} {L : Type u} [Field L] [CharZero L] (T : MarkedTriple k) (T' : MarkedTriple L) (σ : k →+* L) (p : T'.X.left ⟶ T.X.left) (hbc : T'.IsBaseChangeOf T σ p) (hT : MarkedTriple.BMOClass n m T) (hT' : MarkedTriple.BMOClass n m T') (S : T.X.left.BlowUpSequence) (hS : S.IsOrderGeSeq (T.X.left ↘ AlgebraicGeometry.Spec ↧k) T.I T.m T.E ∧ S.NoEmptyCenters) (hS' : (S.pullback p).IsOrderGeSeq (T'.X.left ↘ AlgebraicGeometry.Spec ↧L) T'.I T'.m T'.E ∧ (S.pullback p).NoEmptyCenters) : tailAfterStep1 bo T' hT' ⟨S.pullback p, hS'⟩ = (tailAfterStep1 bo T hT ⟨S, hS⟩).pullback (S.pullbackLastHom p)

The tail after Step 1 under a change of fields: the change-of-fields form of tailAfterStep1_pullback.

theorem Hironaka.BMO.concat_tailAfterStep1_baseChange {k : Type u} [Field k] [CharZero k] {n : ℕ} (bo : (d : ℕ) → BOData n d) {m : ℕ} {L : Type u} [Field L] [CharZero L] (T : MarkedTriple k) (T' : MarkedTriple L) (σ : k →+* L) (p : T'.X.left ⟶ T.X.left) (hbc : T'.IsBaseChangeOf T σ p) (hT : MarkedTriple.BMOClass n m T) (hT' : MarkedTriple.BMOClass n m T') (σ₁ : { S : T.X.left.BlowUpSequence // S.IsOrderGeSeq (T.X.left ↘ AlgebraicGeometry.Spec ↧k) T.I T.m T.E ∧ S.NoEmptyCenters }) (σ₁' : { S : T'.X.left.BlowUpSequence // S.IsOrderGeSeq (T'.X.left ↘ AlgebraicGeometry.Spec ↧L) T'.I T'.m T'.E ∧ S.NoEmptyCenters }) (e : ↑σ₁' = (↑σ₁).pullback p) : (↑σ₁').concat (tailAfterStep1 bo T' hT' σ₁') = ((↑σ₁).concat (tailAfterStep1 bo T hT σ₁)).pullback p

The whole assembly under a change of fields: the change-of-fields form of concat_tailAfterStep1_pullback.

theorem Hironaka.BMO.commutesWithBaseChange {k : Type u} [Field k] [CharZero k] {n : ℕ} (bo : (d : ℕ) → BOData n d) {m : ℕ} {L : Type u} [Field L] [CharZero L] (σ : k →+* L) : (functor bo m).CommutesWithBaseChange (functor bo m) σ

BMO_{n,m} commutes with change of fields (clause (2) of [Kol07, Theorem 107] with [Kol07, 34.2]): the field commutesWithBaseChange of the order-reduction data on each round, with the parameters preserved (roundOrder_of_isBaseChangeOf, sepOrder_of_isBaseChangeOf), and step3Seq_baseChange for Step 3; no blow-up is deleted.