The algebra of CP3: strata in given coordinates, images of chain forms, lifts

The ring-level part of the statement CP3 of the embedded desingularization (Hironaka.Resolution.Algebraic.Wlo05.EmbeddedChainRelative: the centres of a run on a protected state are chain-relative strata). It provides: the predicates StratumIn and TerminalIn — admissible and terminal-normal strata (Hironaka.Resolution.Algebraic.Wlo05.EmbeddedAdmissibleStratum) IN given chain coordinates; the images of the chain forms under ring homomorphisms; the truncation of the chain at the first level whose monomial vanishes; the ideal identities for the restriction to a member of the boundary (two cases: no level carries the killed coordinate, or a first level does and truncates the chain) and for the descent to a chain hypersurface (the flag shortened, the monomials shifted, M₀ the new top monomial); the regular system of parameters of the member's stalk; and the lifts of strata along the surjection to the member or to the hypersurface (the killed coordinate adjoined; the absorption (f̄) lifting to a stratum one level up, or to the terminal-normal stratum (f, z_{k₀})).

The hypersurface of maximal contact and the restriction of the ideal to it are those of [Kol07, Lemma 62] and the proof of [Kol07, Lemma 102]. These identities are not in the literature. They are used by the CP3 modules Hironaka.Resolution.Algebraic.Wlo05.EmbeddedCP3Predicates, Hironaka.Resolution.Algebraic.Wlo05.EmbeddedCP3Rebase, Hironaka.Resolution.Algebraic.Wlo05.EmbeddedCP3Pass, Hironaka.Resolution.Algebraic.Wlo05.EmbeddedCP3Chain, Hironaka.Resolution.Algebraic.Wlo05.EmbeddedCP3Restrict and Hironaka.Resolution.Algebraic.Wlo05.EmbeddedCP3Transport.

def Hironaka.Resolution.StratumIn {R : Type u_1} [CommRing R] {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) : Prop

Z is an admissible chain stratum IN the coordinates (z, σ, a, b) with member coordinates C: Z = (f₀, …, f_{l−1}, z_s), l ≤ r, s ⊆ C, and (★) at the stratum's own level.

Equations

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

def Hironaka.Resolution.TerminalIn {R : Type u_1} [CommRing R] {n : ℕ} (z : Fin n → R) (C : Set (Fin n)) {r : ℕ} (σ : Fin (r + 1) → Fin n) (Z : Ideal R) : Prop

Z is a terminal-normal stratum IN the coordinates (z, σ): all chain equations plus a nonempty set of member coordinates.

Equations

• Hironaka.Resolution.TerminalIn z C σ Z = ∃ (s : Finset (Fin n)), ↑s ⊆ C ∧ s.Nonempty ∧ Z = Ideal.span (Set.range (z ∘ σ)) ⊔ Ideal.span (z '' ↑s)

theorem Hironaka.Resolution.map_monomialOf {R : Type u_1} [CommRing R] {S : Type u_2} [CommRing S] (φ : R →+* S) {n : ℕ} (z : Fin n → R) (a : Fin n → ℕ) : φ (monomialOf z a) = monomialOf (⇑φ ∘ z) a

The image of a monomial under a ring homomorphism is the monomial of the images.

theorem Hironaka.Resolution.map_chainIdeal {R : Type u_1} [CommRing R] {S : Type u_2} [CommRing S] (φ : R →+* S) {r : ℕ} (f M : Fin r → R) : Ideal.map φ (chainIdeal f M) = chainIdeal (⇑φ ∘ f) (⇑φ ∘ M)

The image of the un-isolated chain form is the chain form of the images.

theorem Hironaka.Resolution.map_chainKIdeal {R : Type u_1} [CommRing R] {S : Type u_2} [CommRing S] (φ : R →+* S) {r : ℕ} (f M : Fin (r + 1) → R) : Ideal.map φ (chainKIdeal f M) = chainKIdeal (⇑φ ∘ f) (⇑φ ∘ M)

The image of the K-shape is the K-shape of the images.

theorem Hironaka.Resolution.prod_filter_lt_castLE {R : Type u_1} [CommRing R] {r l₀ : ℕ} (h : l₀ + 1 ≤ r + 1) (M : Fin (r + 1) → R) (j : Fin (l₀ + 1)) : ∏ i' : Fin (r + 1) with i' < Fin.castLE h j, M i' = ∏ j' : Fin (l₀ + 1) with j' < j, M (Fin.castLE h j')

The product over the indices below castLE j reindexed through castLE.

theorem Hironaka.Resolution.prod_filter_lt_eq_zero {R : Type u_1} [CommRing R] {r : ℕ} (M : Fin r → R) {l₀ : Fin r} (h0 : M l₀ = 0) {i : Fin r} (hi : l₀ < i) : ∏ i' : Fin r with i' < i, M i' = 0

A generator whose product contains a vanishing monomial is zero.

theorem Hironaka.Resolution.chainIdeal_eq_chainIdeal_castLE {R : Type u_1} [CommRing R] {r : ℕ} (f M : Fin r → R) {l₀ : ℕ} (hl : l₀ < r) (h0 : M ⟨l₀, hl⟩ = 0) : chainIdeal f M = chainIdeal (fun (i : Fin (l₀ + 1)) => f (Fin.castLE hl i)) fun (i : Fin (l₀ + 1)) => M (Fin.castLE hl i)

The truncation of the chain, un-isolated form: a vanishing monomial at level l₀ < r truncates the chain at l₀.

theorem Hironaka.Resolution.chainKIdeal_eq_chainIdeal_castLE {R : Type u_1} [CommRing R] {r : ℕ} (f M : Fin (r + 1) → R) {l₀ : ℕ} (hl : l₀ < r) (h0 : M ⟨l₀, ⋯⟩ = 0) : chainKIdeal f M = chainIdeal (fun (i : Fin (l₀ + 1)) => f (Fin.castLE ⋯ i)) fun (i : Fin (l₀ + 1)) => M (Fin.castLE ⋯ i)

The truncation of the chain, K-shape: a vanishing monomial at level l₀ < r turns the K-shape into the un-isolated form of the chain truncated at l₀ (g := f_{l₀}).

theorem Hironaka.Resolution.map_monomialOf_of_apply_eq_zero {R : Type u_1} [CommRing R] {S : Type u_2} [CommRing S] {n : ℕ} (z : Fin (n + 1) → R) (k₀ : Fin (n + 1)) (φ : R →+* S) (a : Fin (n + 1) → ℕ) (ha : a k₀ = 0) : φ (monomialOf z a) = monomialOf (fun (i : Fin n) => φ (z (k₀.succAbove i))) (a ∘ k₀.succAbove)

A monomial with exponent 0 at the killed coordinate maps to the monomial of the remaining coordinates.

theorem Hironaka.Resolution.map_monomialOf_of_apply_ne_zero {R : Type u_1} [CommRing R] {S : Type u_2} [CommRing S] {n : ℕ} (z : Fin (n + 1) → R) (k₀ : Fin (n + 1)) (φ : R →+* S) (hk : φ (z k₀) = 0) (a : Fin (n + 1) → ℕ) (ha : a k₀ ≠ 0) : φ (monomialOf z a) = 0

A monomial with a positive exponent at the killed coordinate maps to 0.

def Hironaka.Resolution.natExt {R : Type u_1} [CommRing R] {m : ℕ} (M : Fin m → R) (k : ℕ) : R

The chain monomials as an ℕ-indexed family (1 beyond the range).

Equations

• Hironaka.Resolution.natExt M k = if h : k < m then M ⟨k, h⟩ else 1

theorem Hironaka.Resolution.natExt_val {R : Type u_1} [CommRing R] {m : ℕ} (M : Fin m → R) (i : Fin m) : natExt M ↑i = M i

natExt agrees with M on the range.

theorem Hironaka.Resolution.natExt_zero {R : Type u_1} [CommRing R] {m : ℕ} (M : Fin (m + 1) → R) : natExt M 0 = M 0

natExt at 0.

theorem Hironaka.Resolution.natExt_comp_succ {R : Type u_1} [CommRing R] {m : ℕ} (M : Fin (m + 1) → R) (k : ℕ) : natExt (M ∘ Fin.succ) k = natExt M (k + 1)

natExt of the shifted family.

theorem Hironaka.Resolution.natExt_eq_one_of_lt {R : Type u_1} [CommRing R] {m : ℕ} (M : Fin m → R) {t : Fin m} (ht : ∀ (i : Fin m), ↑i < ↑t → M i = 1) {k : ℕ} (hk : k < ↑t) : natExt M k = 1

natExt is 1 below a trivial block's end.

theorem Hironaka.Resolution.prod_filter_lt_eq_prod_range {R : Type u_1} [CommRing R] {m : ℕ} (M : Fin m → R) (i : Fin m) : ∏ i' : Fin m with i' < i, M i' = ∏ k ∈ Finset.range ↑i, natExt M k

The chain product below i as a product over range i.

theorem Hironaka.Resolution.descent_generator_eq {R : Type u_1} [CommRing R] {r : ℕ} (M : Fin (r + 1) → R) (t : Fin (r + 1)) (ht : ∀ (i : Fin (r + 1)), ↑i < ↑t → M i = 1) (j : Fin r) (x : R) : M 0 * ((∏ j' : Fin r with j' < j, (M ∘ Fin.succ) j') * x) = (∏ i' : Fin (r + 1) with i' < t.succAbove j, M i') * x

The generator identity of the descent: with the monomials before t trivial, the generator of the shortened chain at j, times M₀, is the generator of the full chain at t.succAbove j.

theorem Hironaka.Resolution.chainIdeal_eq_span_mul_chainIdeal_succAbove {R : Type u_1} [CommRing R] {r : ℕ} (f M : Fin (r + 1) → R) (t : Fin (r + 1)) (ht : ∀ (i : Fin (r + 1)), ↑i < ↑t → M i = 1) (h0 : f t = 0) : chainIdeal f M = Ideal.span {M 0} * chainIdeal (f ∘ t.succAbove) (M ∘ Fin.succ)

The descent to a chain hypersurface, un-isolated form: killing the chain coordinate f_t (the monomials before t trivial) gives M₀ · I(f without t; M shifted).

theorem Hironaka.Resolution.chainKIdeal_eq_span_mul_chainKIdeal_succAbove {R : Type u_1} [CommRing R] {r : ℕ} (f M : Fin (r + 2) → R) (t : Fin (r + 2)) (ht : ∀ (i : Fin (r + 2)), ↑i < ↑t → M i = 1) (h0 : f t = 0) : chainKIdeal f M = Ideal.span {M 0} * chainKIdeal (f ∘ t.succAbove) (M ∘ Fin.succ)

The K-shape version: the K-last generator is handled through update; when t is the last chain coordinate every monomial is trivial and both sides are the unit ideal.

theorem Hironaka.Resolution.chainKIdeal_congr_of_lt {R : Type u_1} [CommRing R] {r : ℕ} (f : Fin (r + 1) → R) {M M' : Fin (r + 1) → R} (h : ∀ (i : Fin (r + 1)), ↑i < r → M i = M' i) : chainKIdeal f M = chainKIdeal f M'

The K-shape ignores the last monomial: agreement below r suffices.

theorem Hironaka.Resolution.chainIdeal_congr_of_lt {R : Type u_1} [CommRing R] {r : ℕ} (f : Fin r → R) {M M' : Fin r → R} (h : ∀ (i : Fin r), ↑i + 1 < r → M i = M' i) : chainIdeal f M = chainIdeal f M'

The un-isolated form ignores the last monomial.

theorem Hironaka.Resolution.map_span_mul_chainKIdeal_of_forall {R : Type u_1} [CommRing R] {S : Type u_2} [CommRing S] {n : ℕ} (z : Fin (n + 1) → R) (k₀ : Fin (n + 1)) (φ : R →+* S) {r : ℕ} (σ : Fin (r + 1) → Fin (n + 1)) (σ' : Fin (r + 1) → Fin n) (hσ : ∀ (i : Fin (r + 1)), k₀.succAbove (σ' i) = σ i) (a : Fin (r + 1) → Fin (n + 1) → ℕ) (b : Fin (n + 1) → ℕ) (hb : b k₀ = 0) (ha : ∀ (i : Fin (r + 1)), ↑i < r → a i k₀ = 0) : Ideal.map φ (Ideal.span {monomialOf z b} * chainKIdeal (z ∘ σ) fun (i : Fin (r + 1)) => monomialOf z (a i)) = Ideal.span {monomialOf (fun (i : Fin n) => φ (z (k₀.succAbove i))) (b ∘ k₀.succAbove)} * chainKIdeal ((fun (i : Fin n) => φ (z (k₀.succAbove i))) ∘ σ') fun (i : Fin (r + 1)) => monomialOf (fun (i : Fin n) => φ (z (k₀.succAbove i))) (a i ∘ k₀.succAbove)

The restriction to a member, K-shape, when no level < r carries the killed coordinate: the image is the K-shape of the restricted data.

theorem Hironaka.Resolution.map_span_mul_chainIdeal_of_forall {R : Type u_1} [CommRing R] {S : Type u_2} [CommRing S] {n : ℕ} (z : Fin (n + 1) → R) (k₀ : Fin (n + 1)) (φ : R →+* S) {r : ℕ} (σ : Fin (r + 1) → Fin (n + 1)) (σ' : Fin (r + 1) → Fin n) (hσ : ∀ (i : Fin (r + 1)), k₀.succAbove (σ' i) = σ i) (a : Fin (r + 1) → Fin (n + 1) → ℕ) (b : Fin (n + 1) → ℕ) (hb : b k₀ = 0) (ha : ∀ (i : Fin (r + 1)), ↑i < r → a i k₀ = 0) : Ideal.map φ (Ideal.span {monomialOf z b} * chainIdeal (z ∘ σ) fun (i : Fin (r + 1)) => monomialOf z (a i)) = Ideal.span {monomialOf (fun (i : Fin n) => φ (z (k₀.succAbove i))) (b ∘ k₀.succAbove)} * chainIdeal ((fun (i : Fin n) => φ (z (k₀.succAbove i))) ∘ σ') fun (i : Fin (r + 1)) => monomialOf (fun (i : Fin n) => φ (z (k₀.succAbove i))) (a i ∘ k₀.succAbove)

The restriction to a member for the un-isolated form, when no level carries the killed coordinate.

theorem Hironaka.Resolution.map_span_mul_chainKIdeal_of_lt {R : Type u_1} [CommRing R] {S : Type u_2} [CommRing S] {n : ℕ} (z : Fin (n + 1) → R) (k₀ : Fin (n + 1)) (φ : R →+* S) (hk : φ (z k₀) = 0) {r : ℕ} (σ : Fin (r + 1) → Fin (n + 1)) (σ' : Fin (r + 1) → Fin n) (hσ : ∀ (i : Fin (r + 1)), k₀.succAbove (σ' i) = σ i) (a : Fin (r + 1) → Fin (n + 1) → ℕ) (b : Fin (n + 1) → ℕ) (hb : b k₀ = 0) {l₀ : ℕ} (hl : l₀ < r) (h0 : a ⟨l₀, ⋯⟩ k₀ ≠ 0) (hlt : ∀ (i : Fin (r + 1)), ↑i < l₀ → a i k₀ = 0) : Ideal.map φ (Ideal.span {monomialOf z b} * chainKIdeal (z ∘ σ) fun (i : Fin (r + 1)) => monomialOf z (a i)) = Ideal.span {monomialOf (fun (i : Fin n) => φ (z (k₀.succAbove i))) (b ∘ k₀.succAbove)} * chainIdeal (fun (i : Fin (l₀ + 1)) => φ (z (k₀.succAbove (σ' (Fin.castLE ⋯ i))))) fun (i : Fin (l₀ + 1)) => monomialOf (fun (i : Fin n) => φ (z (k₀.succAbove i))) (a (Fin.castLE ⋯ i) ∘ k₀.succAbove)

The restriction to a member, K-shape, when a first level l₀ < r carries the killed coordinate: it truncates the chain — the image is the un-isolated form of f₀, …, f_{l₀}.

theorem Hironaka.Resolution.map_span_mul_chainIdeal_of_lt {R : Type u_1} [CommRing R] {S : Type u_2} [CommRing S] {n : ℕ} (z : Fin (n + 1) → R) (k₀ : Fin (n + 1)) (φ : R →+* S) (hk : φ (z k₀) = 0) {r : ℕ} (σ : Fin (r + 1) → Fin (n + 1)) (σ' : Fin (r + 1) → Fin n) (hσ : ∀ (i : Fin (r + 1)), k₀.succAbove (σ' i) = σ i) (a : Fin (r + 1) → Fin (n + 1) → ℕ) (b : Fin (n + 1) → ℕ) (hb : b k₀ = 0) {l₀ : ℕ} (hl : l₀ < r) (h0 : a ⟨l₀, ⋯⟩ k₀ ≠ 0) (hlt : ∀ (i : Fin (r + 1)), ↑i < l₀ → a i k₀ = 0) : Ideal.map φ (Ideal.span {monomialOf z b} * chainIdeal (z ∘ σ) fun (i : Fin (r + 1)) => monomialOf z (a i)) = Ideal.span {monomialOf (fun (i : Fin n) => φ (z (k₀.succAbove i))) (b ∘ k₀.succAbove)} * chainIdeal (fun (i : Fin (l₀ + 1)) => φ (z (k₀.succAbove (σ' (Fin.castLE ⋯ i))))) fun (i : Fin (l₀ + 1)) => monomialOf (fun (i : Fin n) => φ (z (k₀.succAbove i))) (a (Fin.castLE ⋯ i) ∘ k₀.succAbove)

The restriction to a member for the un-isolated form, when a first level carries the killed coordinate.

theorem Hironaka.Resolution.map_chainKIdeal_succAbove_of_trivial {R : Type u_1} [CommRing R] {S : Type u_2} [CommRing S] {n : ℕ} (z : Fin (n + 1) → R) (k₀ : Fin (n + 1)) (φ : R →+* S) (hk : φ (z k₀) = 0) {r : ℕ} (σ : Fin (r + 2) → Fin (n + 1)) (t : Fin (r + 2)) (hk₀ : σ t = k₀) (σ' : Fin (r + 1) → Fin n) (hσ : ∀ (i : Fin (r + 1)), k₀.succAbove (σ' i) = σ (t.succAbove i)) (a : Fin (r + 2) → Fin (n + 1) → ℕ) (ha : ∀ (i : Fin (r + 2)) (κ : Fin (n + 1)), a i κ ≠ 0 → κ ≠ k₀) (ht : ∀ (i : Fin (r + 2)), ↑i < ↑t → a i = 0) : Ideal.map φ (chainKIdeal (z ∘ σ) fun (i : Fin (r + 1 + 1)) => monomialOf z (a i)) = Ideal.span {monomialOf (fun (i : Fin n) => φ (z (k₀.succAbove i))) (a 0 ∘ k₀.succAbove)} * chainKIdeal ((fun (i : Fin n) => φ (z (k₀.succAbove i))) ∘ σ') fun (i : Fin (r + 1)) => monomialOf (fun (i : Fin n) => φ (z (k₀.succAbove i))) (a i.succ ∘ k₀.succAbove)

The descent to a chain hypersurface at the ring level, K-shape: killing the chain coordinate f_t after a trivial block gives M₀ · K(f without t; M shifted).

theorem Hironaka.Resolution.map_chainIdeal_succAbove_of_trivial {R : Type u_1} [CommRing R] {S : Type u_2} [CommRing S] {n : ℕ} (z : Fin (n + 1) → R) (k₀ : Fin (n + 1)) (φ : R →+* S) (hk : φ (z k₀) = 0) {r : ℕ} (σ : Fin (r + 1) → Fin (n + 1)) (t : Fin (r + 1)) (hk₀ : σ t = k₀) (σ' : Fin r → Fin n) (hσ : ∀ (i : Fin r), k₀.succAbove (σ' i) = σ (t.succAbove i)) (a : Fin (r + 1) → Fin (n + 1) → ℕ) (ha : ∀ (i : Fin (r + 1)) (κ : Fin (n + 1)), a i κ ≠ 0 → κ ≠ k₀) (ht : ∀ (i : Fin (r + 1)), ↑i < ↑t → a i = 0) : Ideal.map φ (chainIdeal (z ∘ σ) fun (i : Fin (r + 1)) => monomialOf z (a i)) = Ideal.span {monomialOf (fun (i : Fin n) => φ (z (k₀.succAbove i))) (a 0 ∘ k₀.succAbove)} * chainIdeal ((fun (i : Fin n) => φ (z (k₀.succAbove i))) ∘ σ') fun (i : Fin r) => monomialOf (fun (i : Fin n) => φ (z (k₀.succAbove i))) (a i.succ ∘ k₀.succAbove)

The same descent for the un-isolated form.

theorem Hironaka.Resolution.comap_map_eq_sup_span {R : Type u_1} [CommRing R] {S : Type u_2} [CommRing S] {n : ℕ} {z : Fin (n + 1) → R} {k₀ : Fin (n + 1)} {φ : R →+* S} (hφ : Function.Surjective ⇑φ) (hker : RingHom.ker φ = Ideal.span {z k₀}) (J : Ideal R) : Ideal.comap φ (Ideal.map φ J) = J ⊔ Ideal.span {z k₀}

comap ∘ map along a surjection with kernel (z k₀).

theorem Hironaka.Resolution.apply_eq_zero_of_ker {R : Type u_1} [CommRing R] {S : Type u_2} [CommRing S] {n : ℕ} {z : Fin (n + 1) → R} {k₀ : Fin (n + 1)} {φ : R →+* S} (hker : RingHom.ker φ = Ideal.span {z k₀}) : φ (z k₀) = 0

The killed coordinate maps to 0.

theorem Hironaka.Resolution.isRegularSystemOfParameters_comp_succAbove {R : Type u_1} [CommRing R] {S : Type u_2} [CommRing S] [IsRegularLocalRing R] [IsLocalRing S] {n : ℕ} {z : Fin (n + 1) → R} (hz : IsLocalRing.IsRegularSystemOfParameters z) (k₀ : Fin (n + 1)) (φ : R →+* S) (hφ : Function.Surjective ⇑φ) (hker : RingHom.ker φ = Ideal.span {z k₀}) : IsLocalRing.IsRegularSystemOfParameters fun (i : Fin n) => φ (z (k₀.succAbove i))

The images of a regular system of parameters under a surjection killing exactly one of them form a regular system of parameters of the target.

theorem Hironaka.Resolution.stratumIn_comap_of_stratumIn {R : Type u_1} [CommRing R] {S : Type u_2} [CommRing S] {n : ℕ} {z : Fin (n + 1) → R} {k₀ : Fin (n + 1)} {φ : R →+* S} (hφ : Function.Surjective ⇑φ) (hker : RingHom.ker φ = Ideal.span {z k₀}) {C : Set (Fin (n + 1))} (hk₀ : k₀ ∈ C) {C' : Set (Fin n)} (hC : ∀ k ∈ C', k₀.succAbove k ∈ C) {r : ℕ} {σ : Fin (r + 1) → Fin (n + 1)} {σ' : Fin (r + 1) → Fin n} (hσ : ∀ (i : Fin (r + 1)), k₀.succAbove (σ' i) = σ i) {a : Fin (r + 1) → Fin (n + 1) → ℕ} {b : Fin (n + 1) → ℕ} {Z' : Ideal S} (h : StratumIn (fun (i : Fin n) => φ (z (k₀.succAbove i))) C' σ' (fun (i : Fin (r + 1)) => a i ∘ k₀.succAbove) (b ∘ k₀.succAbove) Z') : StratumIn z C σ a b (Ideal.comap φ Z')

The lift of a stratum along the surjection: the preimage of a stratum in the restricted coordinates is a stratum in the original ones, the killed coordinate adjoined.

theorem Hironaka.Resolution.terminalIn_comap_of_terminalIn {R : Type u_1} [CommRing R] {S : Type u_2} [CommRing S] {n : ℕ} {z : Fin (n + 1) → R} {k₀ : Fin (n + 1)} {φ : R →+* S} (hφ : Function.Surjective ⇑φ) (hker : RingHom.ker φ = Ideal.span {z k₀}) {C : Set (Fin (n + 1))} (hk₀ : k₀ ∈ C) {C' : Set (Fin n)} (hC : ∀ k ∈ C', k₀.succAbove k ∈ C) {r : ℕ} {σ : Fin (r + 1) → Fin (n + 1)} {σ' : Fin (r + 1) → Fin n} (hσ : ∀ (i : Fin (r + 1)), k₀.succAbove (σ' i) = σ i) {Z' : Ideal S} (h : TerminalIn (fun (i : Fin n) => φ (z (k₀.succAbove i))) C' σ' Z') : TerminalIn z C σ (Ideal.comap φ Z')

The lift of a terminal-normal stratum.

theorem Hironaka.Resolution.terminalIn_comap_of_eq_span {R : Type u_1} [CommRing R] {S : Type u_2} [CommRing S] {n : ℕ} {z : Fin (n + 1) → R} {k₀ : Fin (n + 1)} {φ : R →+* S} (hφ : Function.Surjective ⇑φ) (hker : RingHom.ker φ = Ideal.span {z k₀}) {C : Set (Fin (n + 1))} (hk₀ : k₀ ∈ C) {r : ℕ} {σ : Fin (r + 1) → Fin (n + 1)} {σ' : Fin (r + 1) → Fin n} (hσ : ∀ (i : Fin (r + 1)), k₀.succAbove (σ' i) = σ i) {Z' : Ideal S} (h : Z' = Ideal.span (Set.range ((fun (i : Fin n) => φ (z (k₀.succAbove i))) ∘ σ'))) : TerminalIn z C σ (Ideal.comap φ Z')

The lift of the absorption Z' = (f̄): the preimage is the terminal-normal stratum (f, z_{k₀}).

theorem Hironaka.Resolution.image_castLE_lt_eq {R : Type u_1} {r l₀ : ℕ} (h : l₀ + 1 ≤ r + 1) {F : Fin (r + 1) → R} {l : ℕ} (hl : l ≤ l₀ + 1) : (fun (i : Fin (l₀ + 1)) => F (Fin.castLE h i)) '' {i : Fin (l₀ + 1) | ↑i < l} = F '' {i : Fin (r + 1) | ↑i < l}

Truncated images: the image of the indices below l ≤ l₀ through castLE is the image of the indices below l.

theorem Hironaka.Resolution.range_castLE_eq {R : Type u_1} {r l₀ : ℕ} (h : l₀ + 1 ≤ r + 1) (F : Fin (r + 1) → R) : (Set.range fun (i : Fin (l₀ + 1)) => F (Fin.castLE h i)) = F '' {i : Fin (r + 1) | ↑i < l₀ + 1}

The range of the truncated family is the image of the indices below l₀ + 1.

theorem Hironaka.Resolution.image_succAbove_lt_union {r l : ℕ} (t : Fin (r + 2)) (hl : ↑t ≤ l) : t.succAbove '' {i : Fin (r + 1) | ↑i < l} ∪ {t} = {i : Fin (r + 2) | ↑i < l + 1}

The indices below l + 1 are the succAbove t-images of the indices below l together with t, when t ≤ l.

theorem Hironaka.Resolution.span_image_succAbove_sup {R : Type u_1} [CommRing R] {r l : ℕ} (F : Fin (r + 2) → R) (t : Fin (r + 2)) (hl : ↑t ≤ l) : Ideal.span (F ∘ t.succAbove '' {i : Fin (r + 1) | ↑i < l}) ⊔ Ideal.span {F t} = Ideal.span (F '' {i : Fin (r + 2) | ↑i < l + 1})

The flag span of the shortened chain, with the killed coordinate adjoined, is the flag span of the full chain (t ≤ l).

theorem Hironaka.Resolution.span_range_comp_succAbove_sup {R : Type u_1} [CommRing R] {r : ℕ} (F : Fin (r + 2) → R) (t : Fin (r + 2)) : Ideal.span (Set.range (F ∘ t.succAbove)) ⊔ Ideal.span {F t} = Ideal.span (Set.range F)

The chain span of the shortened chain, with the killed coordinate adjoined, is the full chain span.

theorem Hironaka.Resolution.stratumIn_comap_of_stratumIn_castLE {R : Type u_1} [CommRing R] {S : Type u_2} [CommRing S] {n : ℕ} {z : Fin (n + 1) → R} {k₀ : Fin (n + 1)} {φ : R →+* S} (hφ : Function.Surjective ⇑φ) (hker : RingHom.ker φ = Ideal.span {z k₀}) {C : Set (Fin (n + 1))} (hk₀ : k₀ ∈ C) {C' : Set (Fin n)} (hC : ∀ k ∈ C', k₀.succAbove k ∈ C) {r : ℕ} {σ : Fin (r + 1) → Fin (n + 1)} {σ' : Fin (r + 1) → Fin n} (hσ : ∀ (i : Fin (r + 1)), k₀.succAbove (σ' i) = σ i) {a : Fin (r + 1) → Fin (n + 1) → ℕ} {b : Fin (n + 1) → ℕ} {l₀ : ℕ} (hl : l₀ < r) (ha : a ⟨l₀, ⋯⟩ k₀ ≠ 0) {Z' : Ideal S} (h : StratumIn (fun (i : Fin n) => φ (z (k₀.succAbove i))) C' (fun (i : Fin (l₀ + 1)) => σ' (Fin.castLE ⋯ i)) (fun (i : Fin (l₀ + 1)) => a (Fin.castLE ⋯ i) ∘ k₀.succAbove) (b ∘ k₀.succAbove) Z' ∨ TerminalIn (fun (i : Fin n) => φ (z (k₀.succAbove i))) C' (fun (i : Fin (l₀ + 1)) => σ' (Fin.castLE ⋯ i)) Z' ∨ Z' = Ideal.span (Set.range ((fun (i : Fin n) => φ (z (k₀.succAbove i))) ∘ fun (i : Fin (l₀ + 1)) => σ' (Fin.castLE ⋯ i)))) : StratumIn z C σ a b (Ideal.comap φ Z')

The lift of a stratum of the TRUNCATED chain (the restriction to a member with a first level carrying the killed coordinate): a stratum at level l ≤ l₀ of the truncated chain, or its absorption, lifts to a stratum of the full chain; the absorption lifts to level l₀ + 1 with s = {k₀}, admissible by a l₀ k₀ ≠ 0.

theorem Hironaka.Resolution.stratumIn_comap_of_stratumIn_succAbove {R : Type u_1} [CommRing R] {S : Type u_2} [CommRing S] {n : ℕ} {z : Fin (n + 1) → R} {k₀ : Fin (n + 1)} {φ : R →+* S} (hφ : Function.Surjective ⇑φ) (hker : RingHom.ker φ = Ideal.span {z k₀}) {C : Set (Fin (n + 1))} {C' : Set (Fin n)} (hC : ∀ k ∈ C', k₀.succAbove k ∈ C) {r : ℕ} {σ : Fin (r + 2) → Fin (n + 1)} {t : Fin (r + 2)} (hk₀ : σ t = k₀) {σ' : Fin (r + 1) → Fin n} (hσ : ∀ (i : Fin (r + 1)), k₀.succAbove (σ' i) = σ (t.succAbove i)) {a : Fin (r + 2) → Fin (n + 1) → ℕ} (ht : ∀ (i : Fin (r + 2)), ↑i < ↑t → a i = 0) {b : Fin (n + 1) → ℕ} {Z' : Ideal S} (h : StratumIn (fun (i : Fin n) => φ (z (k₀.succAbove i))) C' σ' (fun (i : Fin (r + 1)) => a i.succ ∘ k₀.succAbove) (a 0 ∘ k₀.succAbove) Z') : StratumIn z C σ a b (Ideal.comap φ Z')

The lift along the descent to a chain hypersurface (k₀ = σ t, the flag shortened, the monomials shifted): a stratum of the shortened chain lifts to a stratum of the full chain.

theorem Hironaka.Resolution.terminalIn_comap_of_terminalIn_succAbove {R : Type u_1} [CommRing R] {S : Type u_2} [CommRing S] {n : ℕ} {z : Fin (n + 1) → R} {k₀ : Fin (n + 1)} {φ : R →+* S} (hφ : Function.Surjective ⇑φ) (hker : RingHom.ker φ = Ideal.span {z k₀}) {C : Set (Fin (n + 1))} {C' : Set (Fin n)} (hC : ∀ k ∈ C', k₀.succAbove k ∈ C) {r : ℕ} {σ : Fin (r + 2) → Fin (n + 1)} {t : Fin (r + 2)} (hk₀ : σ t = k₀) {σ' : Fin (r + 1) → Fin n} (hσ : ∀ (i : Fin (r + 1)), k₀.succAbove (σ' i) = σ (t.succAbove i)) {Z' : Ideal S} (h : TerminalIn (fun (i : Fin n) => φ (z (k₀.succAbove i))) C' σ' Z') : TerminalIn z C σ (Ideal.comap φ Z')

The descent lift for a terminal-normal stratum of the shortened chain: adjoining the killed chain coordinate restores the full chain.

theorem Hironaka.Resolution.comap_eq_span_range_of_eq_span_range_succAbove {R : Type u_1} [CommRing R] {S : Type u_2} [CommRing S] {n : ℕ} {z : Fin (n + 1) → R} {k₀ : Fin (n + 1)} {φ : R →+* S} (hφ : Function.Surjective ⇑φ) (hker : RingHom.ker φ = Ideal.span {z k₀}) {r : ℕ} {σ : Fin (r + 2) → Fin (n + 1)} {t : Fin (r + 2)} (hk₀ : σ t = k₀) {σ' : Fin (r + 1) → Fin n} (hσ : ∀ (i : Fin (r + 1)), k₀.succAbove (σ' i) = σ (t.succAbove i)) {Z' : Ideal S} (h : Z' = Ideal.span (Set.range ((fun (i : Fin n) => φ (z (k₀.succAbove i))) ∘ σ'))) : Ideal.comap φ Z' = Ideal.span (Set.range (z ∘ σ))

The descent lift for the absorption of the shortened chain: the preimage is the full chain.