The transport lemmas of CP3, part 1

The statement CP3 of the embedded desingularization (Hironaka.Resolution.Algebraic.Wlo05.EmbeddedChainRelative) is proved in the form universal over the chain-coordinate systems at a point (CenterClassifiedAt, CP3For of Hironaka.Resolution.Algebraic.Wlo05.EmbeddedCP3Predicates). Like the predicate CP1For of CP1, it must travel with the bookkeeping of the algorithm: along a morphism that is an isomorphism on the stalk (charts, the pull-backs of covers, the deletion of empty blow-ups), between two divisor families whose members through the point correspond, and along a concatenation of runs. This module holds those transports:

• centerClassifiedAt_of_comap_of_isIso_stalkMap and its converse centerClassifiedAt_comap_of_isIso_stalkMap — the stalk isomorphism carries chain coordinates, monomials and chain ideals both ways (isRegularSystemOfParameters_comp_ringEquiv, monomialOf_map, chainIdeal_comp, chainKIdeal_comp), and the strata and terminal strata as well (stratumIn_map_ringEquiv, terminalIn_map_ringEquiv);
• centerClassifiedAt_iff_of_embeds — the classification sees the family only through its members through the point;
• cp3For_concat — CP3For along S.concat T from CP3For on S and on T for the data induced at the end of S (the concatenation of [Kol07, Definition 29]), by the stage, centre and transform identities of Hironaka.Scheme.BlowUpSequence.ConcatIndex (forall_centerClassifiedAt_of_heq carries the pointwise statement across the casts);
• the order bounds ord_le_one_of_stalkIdeal_eq_chainKIdeal and ord_le_one_of_stalkIdeal_eq_chainIdeal — the K-shape and the un-isolated form have order at most one at the point (they contain a parameter or are the unit ideal). This is the observation that makes CP3 hold trivially along the rounds of order ≥ 2 of Step 1 (Hironaka.Resolution.Algebraic.Wlo05.EmbeddedCP3Step1).

These transports are not in the literature. Used in Hironaka.Resolution.Algebraic.Wlo05.EmbeddedCP3EraseEmpty, Hironaka.Resolution.Algebraic.Wlo05.EmbeddedCP3Step21, Hironaka.Resolution.Algebraic.Wlo05.EmbeddedCP3Step22 and Hironaka.Resolution.Algebraic.Wlo05.EmbeddedCP3Tower.

theorem Hironaka.Resolution.stratumIn_map_ringEquiv {R : Type u_1} [CommRing R] {S : Type u_2} [CommRing S] (e : R ≃+* S) {n : ℕ} {z : Fin n → R} {C : Set (Fin n)} {r : ℕ} {σ : Fin (r + 1) → Fin n} {a : Fin (r + 1) → Fin n → ℕ} {b : Fin n → ℕ} {Z : Ideal R} (h : StratumIn z C σ a b Z) : StratumIn (fun (i : Fin n) => e (z i)) C σ a b (Ideal.map (↑e) Z)

A stratum in given coordinates transports along a ring equivalence.

theorem Hironaka.Resolution.terminalIn_map_ringEquiv {R : Type u_1} [CommRing R] {S : Type u_2} [CommRing S] (e : R ≃+* S) {n : ℕ} {z : Fin n → R} {C : Set (Fin n)} {r : ℕ} {σ : Fin (r + 1) → Fin n} {Z : Ideal R} (h : TerminalIn z C σ Z) : TerminalIn (fun (i : Fin n) => e (z i)) C σ (Ideal.map (↑e) Z)

A terminal stratum in given coordinates transports along a ring equivalence.

theorem Hironaka.Resolution.map_span_range_comp {R : Type u_1} [CommRing R] {S : Type u_2} [CommRing S] (e : R ≃+* S) {n : ℕ} (z : Fin n → R) {r : ℕ} (σ : Fin (r + 1) → Fin n) : Ideal.map (↑e) (Ideal.span (Set.range (z ∘ σ))) = Ideal.span (Set.range ((fun (i : Fin n) => e (z i)) ∘ σ))

The image of the span of the range of a composite along a ring equivalence.

theorem Hironaka.Resolution.centerClassifiedAt_of_comap_of_isIso_stalkMap {X Y : AlgebraicGeometry.Scheme} (φ : Y ⟶ X) {E : X.DivisorFamily} {K Z : X.IdealSheafData} {q' : ↥Y} [CategoryTheory.IsIso (AlgebraicGeometry.Scheme.Hom.stalkMap φ q')] (h : CenterClassifiedAt E K Z (φ q')) : CenterClassifiedAt (E.comap φ) (K.comap φ) (Z.comap φ) q'

The classification transports along a morphism inducing an isomorphism on the stalk at the point: the pulled-back data at q' classify when the data at φ q' do (the counterpart of chainRelativeAt_of_comap_of_isIso_stalkMap for the universal predicate).

theorem Hironaka.Resolution.centerClassifiedAt_iff_of_embeds {X : AlgebraicGeometry.Scheme} {E₁ E₂ : X.DivisorFamily} (e : E₁.ι → E₂.ι) (he : Function.Injective e) (hcomp : ∀ (a : E₁.ι), E₂.component (e a) = E₁.component a) {K Z : X.IdealSheafData} {q : ↥X} (hmiss : ∀ b ∉ Set.range e, q ∉ (E₂.component b).support) : CenterClassifiedAt E₁ K Z q ↔ CenterClassifiedAt E₂ K Z q

The classification depends on the family only through its members through q: two families whose members through q correspond classify alike (chainRelativeAt_iff_of_embeds for the universal predicate).

theorem Hironaka.Resolution.ord_le_one_of_stalkIdeal_eq_chainKIdeal {X : AlgebraicGeometry.Scheme} {N : X.IdealSheafData} {p : ↥X} [IsRegularLocalRing ↑(X.presheaf.stalk p)] {n : ℕ} {z : Fin n → ↑(X.presheaf.stalk p)} (hz : IsLocalRing.IsRegularSystemOfParameters z) {r : ℕ} {σ : Fin (r + 1) → Fin n} (M : Fin (r + 1) → ↑(X.presheaf.stalk p)) (hN : N.stalkIdeal p = chainKIdeal (z ∘ σ) M) : N.ord p ≤ 1

The K-shape has order ≤ 1: it contains the parameter f₀, or is the unit ideal.

theorem Hironaka.Resolution.ord_le_one_of_stalkIdeal_eq_chainIdeal {X : AlgebraicGeometry.Scheme} {N : X.IdealSheafData} {p : ↥X} [IsRegularLocalRing ↑(X.presheaf.stalk p)] {n : ℕ} {z : Fin n → ↑(X.presheaf.stalk p)} (hz : IsLocalRing.IsRegularSystemOfParameters z) {r : ℕ} {σ : Fin (r + 1) → Fin n} (M : Fin (r + 1) → ↑(X.presheaf.stalk p)) (hN : N.stalkIdeal p = chainIdeal (z ∘ σ) M) : N.ord p ≤ 1

The un-isolated form has order ≤ 1: it contains the parameter f₀.

theorem Hironaka.Resolution.forall_centerClassifiedAt_of_heq {Y₁ Y₂ : AlgebraicGeometry.Scheme} (e : Y₁ = Y₂) {E₁ : Y₁.DivisorFamily} {E₂ : Y₂.DivisorFamily} (hE : E₁ ≍ E₂) {K₁ Z₁ : Y₁.IdealSheafData} {K₂ Z₂ : Y₂.IdealSheafData} (hK : K₁ ≍ K₂) (hZ : Z₁ ≍ Z₂) (h : ∀ q ∈ Z₁.support, CenterClassifiedAt E₁ K₁ Z₁ q) (q : ↥Y₂) : q ∈ Z₂.support → CenterClassifiedAt E₂ K₂ Z₂ q

The pointwise classification along a stage transports across equal schemes with heterogeneously equal data.

theorem Hironaka.Resolution.cp3For_concat {X : AlgebraicGeometry.Scheme} (S : X.BlowUpSequence) (T : S.last.BlowUpSequence) (I : X.IdealSheafData) (E : X.DivisorFamily) (hS : CP3For S I E) (hT : CP3For T (S.markedTransformSeq I 1 (Fin.last S.length)) (S.totalTransformSeq E (Fin.last S.length))) : CP3For (S.concat T) I E

CP3For along a concatenation ([Kol07, Definition 29]) from CP3For on the two pieces, the second for the data induced at the end of the first (the stage, centre and transform identities of Hironaka.Scheme.BlowUpSequence.ConcatIndex).

theorem Hironaka.Resolution.centerClassifiedAt_comap_of_isIso_stalkMap {X Y : AlgebraicGeometry.Scheme} (φ : Y ⟶ X) {E : X.DivisorFamily} {K Z : X.IdealSheafData} {q' : ↥Y} [CategoryTheory.IsIso (AlgebraicGeometry.Scheme.Hom.stalkMap φ q')] (h : CenterClassifiedAt (E.comap φ) (K.comap φ) (Z.comap φ) q') : CenterClassifiedAt E K Z (φ q')

The converse of centerClassifiedAt_of_comap_of_isIso_stalkMap: the data at φ q' classify when the pulled-back data at q' do.