The disjoined triple commutes with smooth pullback and base change

The functoriality of the principalization functor, clauses (4) and (5) of [Kol07, Theorem 35], "follow[s] from the corresponding functoriality properties in (69) and from (71.2)" [Kol07, 72]; for this the disjoined triple Hironaka.disjoinedTriple T = (X', π^* I, ∑ E^i) must carry the pullback data of disjoinedTriple T' along the lift of a smooth g : X' ⟶ X ([Kol07, 34.1]) and the base-change data along the lift of the projection X_{L,σ} ⟶ X ([Kol07, 34.2]). disjoin_functorial (Hironaka/Resolution/Algebraic/Kol07/Thm35/Disjoin/Functorial.lean) gives disjoinSeq (E.comap g) = (disjoinSeq E).pullback g, an equality of sequences, so the last stages agree only up to an eqToHom, and pullbackLastHom (Hironaka/Scheme/BlowUpSequence/ConcatPullback.lean) is the lift of g to the last stages. This module assembles the two into

• Triple.disjoinedMap g e : (disjoinedTriple T').X.left ⟶ (disjoinedTriple T).X.left, the lift of g across the identification e of the disjoining sequences;
• disjoinedTriple_isPullbackOf: disjoinedTriple T' is the pullback of disjoinedTriple T along it whenever T' is the pullback of T along a flat g ([Kol07, 34.1] for the disjoined triples);
• disjoinedTriple_isBaseChangeOf: the same for the base change along σ : k →+* L ([Kol07, 34.2]), the pulled-back square being the stage square of Hironaka/Scheme/BlowUpSequence/BaseChange.lean at the last stage pasted on the eqToHom.

The one non-formal point is the ordered family ∑ E^i (collapsedFamily): it is the total transform at the end of the disjoining sequence with the birational transforms of the original members collapsed into E^0 (DivisorFamily.collapse), and collapsing commutes with inverse images, componentwise, the collapsed member being a product (collapse_comap, comap_finset_prod), while the total transform and the marking of the original members commute with flat pullback by totalTransformSeq_pullback and the transport of originalIdx, in the recursive form of subfamily_originalIdx_pullback (collapse_originalIdx_pullback). The collapse is defined at the end of an arbitrary sequence S, so that the eqToHom of disjoin_functorial can be absorbed along an equality of sequences (collapsedFamily_congr). The decidability instance of the collapsed predicate is carried explicitly through the recursion (collapse_congr_inst: the collapse does not depend on it), since the constructive instance found for · ∈ Set.range f on a finite type and the classical one are not definitionally equal.

One general fact about sequences is placed here beside its use: Triple.IsBaseChangeOf.isPullback_pullbackLastHom, the last-stage lift of a base change is again a base change (the stage square Triple.IsBaseChangeOf.isPullback_pullbackStageHom at the last index across the identification pullbackStageIdx_last). This module is the first that imports pullbackStageIdx_last (EraseEmptyInduced.lean), pullbackLastHom (ConcatPullback.lean) and isPullback_pullbackStageHom (BaseChange.lean) together.

Collapsing commutes with inverse images

theorem Hironaka.Sequence.collapse_congr_inst {X : AlgebraicGeometry.Scheme} (F : X.DivisorFamily) (p : F.ι → Prop) (i₁ i₂ : DecidablePred p) : F.collapse p = F.collapse p

The collapse does not depend on the decidability instance of the collapsed predicate.

theorem Hironaka.Sequence.collapse_comap {X Y : AlgebraicGeometry.Scheme} (F : X.DivisorFamily) (p : F.ι → Prop) [hp : DecidablePred p] (φ : Y ⟶ X) : (F.collapse p).comap φ = (F.comap φ).collapse p

Collapsing a set of members commutes with the inverse image along any morphism: the collapsed member is a product, and inverse images of ideal sheaves are multiplicative (comap_finset_prod); the other members are unchanged. (The index type of F.comap φ is that of F only by unfolding, so the decidability instance is passed by hand.)

theorem Hironaka.Sequence.collapse_totalTransformSeq_eq_idx {X : AlgebraicGeometry.Scheme} (S : X.BlowUpSequence) (E : X.DivisorFamily) {i j : Fin (S.length + 1)} (e : i = j) (P : (i : Fin (S.length + 1)) → (S.totalTransformSeq E i).ι → Prop) (iP : (i : Fin (S.length + 1)) → DecidablePred (P i)) : (S.totalTransformSeq E j).collapse (P j) = ((S.totalTransformSeq E i).collapse (P i)).comap (CategoryTheory.eqToHom ⋯)

Transport of a collapse of the total transform along an equality of stage indices: the eqToHom of the stage identification is absorbed (the analogue for collapse of subfamily_totalTransformSeq_eq_idx).

theorem Hironaka.Sequence.collapse_originalIdx_congr {X : AlgebraicGeometry.Scheme} (S : X.BlowUpSequence) (F₁ F₂ : X.DivisorFamily) (e : F₁ = F₂) (i : Fin (S.length + 1)) {T : Type u} (x₁ : T → F₁.ι) (x₂ : T → F₂.ι) (hx : x₁ ≍ x₂) (i₁ : DecidablePred fun (b : (S.totalTransformSeq F₁ i).ι) => b ∈ Set.range fun (t : T) => S.originalIdx F₁ i (x₁ t)) (i₂ : DecidablePred fun (b : (S.totalTransformSeq F₂ i).ι) => b ∈ Set.range fun (t : T) => S.originalIdx F₂ i (x₂ t)) : ((S.totalTransformSeq F₁ i).collapse fun (b : (S.totalTransformSeq F₁ i).ι) => b ∈ Set.range fun (t : T) => S.originalIdx F₁ i (x₁ t)) = (S.totalTransformSeq F₂ i).collapse fun (b : (S.totalTransformSeq F₂ i).ι) => b ∈ Set.range fun (t : T) => S.originalIdx F₂ i (x₂ t)

Congruence of the collapse of the total transform along the marked original members, along an equality of the starting families (the analogue for collapse of subfamily_originalIdx_congr).

theorem Hironaka.Sequence.collapse_originalIdx_pullback {X : AlgebraicGeometry.Scheme} (S : X.BlowUpSequence) {Y : AlgebraicGeometry.Scheme} (g : Y ⟶ X) [AlgebraicGeometry.Flat g] (E : X.DivisorFamily) (j : ℕ) (hj : j < S.length + 1) {T : Type u} (x : T → E.ι) (i₁ : DecidablePred fun (b : ((S.pullback g).totalTransformSeq (E.comap g) (S.pullbackStageIdx g ⟨j, hj⟩)).ι) => b ∈ Set.range fun (t : T) => (S.pullback g).originalIdx (E.comap g) (S.pullbackStageIdx g ⟨j, hj⟩) (x t)) (i₂ : DecidablePred fun (b : (S.totalTransformSeq E ⟨j, hj⟩).ι) => b ∈ Set.range fun (t : T) => S.originalIdx E ⟨j, hj⟩ (x t)) : (((S.pullback g).totalTransformSeq (E.comap g) (S.pullbackStageIdx g ⟨j, hj⟩)).collapse fun (b : ((S.pullback g).totalTransformSeq (E.comap g) (S.pullbackStageIdx g ⟨j, hj⟩)).ι) => b ∈ Set.range fun (t : T) => (S.pullback g).originalIdx (E.comap g) (S.pullbackStageIdx g ⟨j, hj⟩) (x t)) = ((S.totalTransformSeq E ⟨j, hj⟩).collapse fun (b : (S.totalTransformSeq E ⟨j, hj⟩).ι) => b ∈ Set.range fun (t : T) => S.originalIdx E ⟨j, hj⟩ (x t)).comap (S.pullbackStageHom g ⟨j, hj⟩)

Along a flat g, the total transform at stage ⟨j, hj⟩ with the birational transforms of the marked original members x t collapsed pulls back to the corresponding collapse of the pulled-back sequence (totalTransformSeq_pullback, subfamily_originalIdx_pullback): by recursion on the sequence, the marked members carried through the first blow-up as toLex (Sum.inl (x t)); at the base the collapse commutes with the inverse image (collapse_comap).

The collapsed family at the end of a sequence

theorem Hironaka.Sequence.collapsedFamily_congr {X : AlgebraicGeometry.Scheme} {S S' : X.BlowUpSequence} (e : S = S') (E : X.DivisorFamily) : collapsedFamily S E = (collapsedFamily S' E).comap (CategoryTheory.eqToHom ⋯)

The collapsed family along an equality of sequences: the eqToHom of the last stages is absorbed.

theorem Hironaka.Sequence.collapsedFamily_pullback {X Y : AlgebraicGeometry.Scheme} (S : X.BlowUpSequence) (g : Y ⟶ X) [AlgebraicGeometry.Flat g] (E : X.DivisorFamily) : collapsedFamily (S.pullback g) (E.comap g) = (collapsedFamily S E).comap (S.pullbackLastHom g)

The collapsed family of the pulled-back sequence is the inverse image of the collapsed family along the last-stage lift (collapse_originalIdx_pullback at the last index, across pullbackStageIdx_last).

A general fact about sequences

theorem AlgebraicGeometry.Triple.IsBaseChangeOf.isPullback_pullbackLastHom {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) : CategoryTheory.IsPullback (S.pullbackLastHom p) (CategoryTheory.CategoryStruct.comp (S.pullback p).composite (T'.X.left ↘ Spec ↧L)) (CategoryTheory.CategoryStruct.comp S.composite (T.X.left ↘ Spec ↧k)) (Spec.map (CommRingCat.ofHom σ))

The last-stage lift of the projection of a base change is again a base change ([Kol07, 34.2] at the last stage): the stage square isPullback_pullbackStageHom at the last index across the identification pullbackStageIdx_last.

The lift to the disjoined triples

noncomputable def AlgebraicGeometry.Triple.disjoinedMap {k : Type u} [Field k] {L : Type u} [Field L] [CharZero k] [CharZero L] {T : Triple k} {T' : Triple L} (g : T'.X.left ⟶ T.X.left) (e : Hironaka.Sequence.disjoinSeq T'.E = (Hironaka.Sequence.disjoinSeq T.E).pullback g) : (Hironaka.disjoinedTriple T').X.left ⟶ (Hironaka.disjoinedTriple T).X.left

The lift of g : T'.X.left ⟶ T.X.left to the disjoined triples (over possibly different base fields), across the identification e of the disjoining sequence of T'.E with the pullback of that of T.E (disjoin_functorial) and the last-stage lift pullbackLastHom.

Equations

• AlgebraicGeometry.Triple.disjoinedMap g e = CategoryTheory.CategoryStruct.comp (CategoryTheory.eqToHom ⋯) ((Hironaka.Sequence.disjoinSeq T.E).pullbackLastHom g)

theorem AlgebraicGeometry.Triple.IsPullbackOf.disjoinSeq_eq {k : Type u} [Field k] {T T' : Triple k} {g : T'.X.left ⟶ T.X.left} [Flat g] (h : T'.IsPullbackOf T g) : Hironaka.Sequence.disjoinSeq T'.E = (Hironaka.Sequence.disjoinSeq T.E).pullback g

The disjoining sequence of the pullback data is the pullback of the disjoining sequence (disjoinSeq_comap_of_flat read through IsPullbackOf).

theorem AlgebraicGeometry.Triple.IsBaseChangeOf.disjoinSeq_eq {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} (h : T'.IsBaseChangeOf T σ p) : Hironaka.Sequence.disjoinSeq T'.E = (Hironaka.Sequence.disjoinSeq T.E).pullback p

The disjoining sequence of the base-change data is the pullback of the disjoining sequence (disjoinSeq_comap_of_flat, the projection being flat).

theorem AlgebraicGeometry.Triple.disjoinedTriple_isPullbackOf {k : Type u} [Field k] [CharZero k] {T T' : Triple k} (g : T'.X.left ⟶ T.X.left) [Flat g] (h : T'.IsPullbackOf T g) : (Hironaka.disjoinedTriple T').IsPullbackOf (Hironaka.disjoinedTriple T) (disjoinedMap g ⋯)

If T' carries the pullback data of T along a flat g, the disjoined triple of T' carries the pullback data of the disjoined triple of T along the lift disjoinedMap ([Kol07, 72 and 34.1]): the structure morphism and the ideal by pullbackLastHom_comp_composite, the ordered family by collapsedFamily_pullback.

theorem AlgebraicGeometry.Triple.disjoinedTriple_isBaseChangeOf {k : Type u} [Field k] {L : Type u} [Field L] [CharZero k] [CharZero L] {T : Triple k} {T' : Triple L} (σ : k →+* L) (p : T'.X.left ⟶ T.X.left) (h : T'.IsBaseChangeOf T σ p) : (Hironaka.disjoinedTriple T').IsBaseChangeOf (Hironaka.disjoinedTriple T) σ (disjoinedMap p ⋯)

If T' carries the base-change data of T along σ through p, the disjoined triple of T' carries the base-change data of the disjoined triple of T through the lift disjoinedMap ([Kol07, 72 and 34.2]): the cartesian square by IsBaseChangeOf.isPullback_pullbackLastHom pasted on the eqToHom, the ideal and the ordered family as for the pullback data.