CP3: re-basing the flag and transferring the strata

The second ring-level part of the statement CP3 of the embedded desingularization (Hironaka.Resolution.Algebraic.Wlo05.EmbeddedChainRelative): re-basing the flag of a K-shape or an un-isolated form to an element x of the ideal of order 1 whose hypersurface has simple normal crossings with the members — the hypersurface of maximal contact chosen in Step 2.2 of the proof of [Kol07, Theorem 103] — by replacing a flag member of the block of trivial monomials by x, the ideal and the exponents unchanged (exists_update_chainKIdeal_eq, exists_update_chainIdeal_eq); and the transfer of admissible, terminal-normal and absorbing strata from the re-based coordinate system back to the given one (stratumIn_of_stratumIn_update_chainKIdeal, stratumIn_of_stratumIn_update_chainIdeal, terminalIn_of_terminalIn_update). The mechanism is the coefficient argument: writing x = ∑ c_i g_i over the generators, outside (z_C) + 𝔪² some coefficient in the trivial block is a unit (exists_unit_coeff_of_notMem), and conversely a unit coefficient is what the regularity of the updated system forces (isUnit_coeff_of_update_rsp). Not in the literature; used by Hironaka.Resolution.Algebraic.Wlo05.EmbeddedCP3Chain.

theorem Hironaka.Resolution.notMem_span_compl_sup_sq {R : Type u_1} [CommRing R] [IsRegularLocalRing R] {n : ℕ} {w : Fin n → R} (hw : IsLocalRing.IsRegularSystemOfParameters w) (j : Fin n) : w j ∉ Ideal.span (w '' {k : Fin n | k ≠ j}) ⊔ IsLocalRing.maximalIdeal R ^ 2

A coordinate of a regular system lies outside the span of the others plus 𝔪².

theorem Hironaka.Resolution.monomialOf_update_of_apply_eq_zero {R : Type u_1} [CommRing R] {n : ℕ} (z : Fin n → R) (k₀ : Fin n) (x : R) (a : Fin n → ℕ) (ha : a k₀ = 0) : monomialOf (Function.update z k₀ x) a = monomialOf z a

A monomial not involving z k₀ is unchanged when z k₀ is replaced.

theorem Hironaka.Resolution.monomialOf_mem_span_singleton {R : Type u_1} [CommRing R] {n : ℕ} (z : Fin n → R) (a : Fin n → ℕ) {k : Fin n} (hk : a k ≠ 0) : monomialOf z a ∈ Ideal.span {z k}

A monomial with a positive exponent at k lies in (z k).

theorem Hironaka.Resolution.exists_unit_coeff_of_notMem {R : Type u_1} [CommRing R] [IsLocalRing R] {ι : Type u_2} [Fintype ι] {n : ℕ} {z : Fin n → R} (hzm : ∀ (k : Fin n), z k ∈ IsLocalRing.maximalIdeal R) (C : Set (Fin n)) (f : ι → Fin n) (g : ι → R) (P : ι → Prop) (hg1 : ∀ (i : ι), P i → g i = z (f i)) (hg2 : ∀ (i : ι), ¬P i → g i ∈ Ideal.span (z '' C)) (c : ι → R) {x : R} (hc : ∑ i : ι, c i • g i = x) (hx2 : x ∉ Ideal.span (z '' C) ⊔ IsLocalRing.maximalIdeal R ^ 2) : ∃ (i : ι), P i ∧ IsUnit (c i)

The core of the re-basing: for generators g agreeing with coordinates on a block P and lying in (z_C) off it, an element ∑ c i • g i outside (z_C) + 𝔪² has a unit coefficient in the block.

theorem Hironaka.Resolution.isRegularSystemOfParameters_update_of_unit {R : Type u_1} [CommRing R] [IsRegularLocalRing R] {n : ℕ} {z : Fin n → R} (hz : IsLocalRing.IsRegularSystemOfParameters z) (j : Fin n) {x : R} (hxm : x ∈ IsLocalRing.maximalIdeal R) {ι : Type u_2} [Fintype ι] (g c : ι → R) (t : ι) (hc : ∑ i : ι, c i • g i = x) (hgt : g t = z j) (hu : IsUnit (c t)) (hg : ∀ (i : ι), i ≠ t → g i ∈ Ideal.span (z '' {k : Fin n | k ≠ j})) : IsLocalRing.IsRegularSystemOfParameters (Function.update z j x)

Replacing the coordinate z j by an element x = ∑ c i • g i with g t = z j, c t a unit and the other g i in the span of the other coordinates gives a regular system of parameters.

theorem Hironaka.Resolution.span_range_update_eq_of_unit {R : Type u_1} [CommRing R] {ι : Type u_2} [Fintype ι] [DecidableEq ι] (g c : ι → R) (t : ι) {x : R} (hc : ∑ i : ι, c i • g i = x) (hu : IsUnit (c t)) : Ideal.span (Set.range (Function.update g t x)) = Ideal.span (Set.range g)

The span of the generators is unchanged when a generator with a unit coefficient in x = ∑ c i • g i is replaced by x.

theorem Hironaka.Resolution.isUnit_coeff_of_update_rsp {R : Type u_1} [CommRing R] [IsRegularLocalRing R] {n : ℕ} {z : Fin n → R} (hz : IsLocalRing.IsRegularSystemOfParameters z) (j : Fin n) {x : R} (hupd : IsLocalRing.IsRegularSystemOfParameters (Function.update z j x)) {ι : Type u_2} [Fintype ι] (g c : ι → R) (t : ι) (hc : ∑ i : ι, c i • g i = x) (hgt : g t = z j) (hg : ∀ (i : ι), i ≠ t → g i ∈ Ideal.span (z '' {k : Fin n | k ≠ j})) : IsUnit (c t)

The unit coefficient from the regularity of the updated system: if update z j x is a regular system, x = ∑ c i • g i with g t = z j and the other g i in the span of the other coordinates, then c t is a unit.

def Hironaka.Resolution.kGen {R : Type u_1} [CommRing R] {n : ℕ} (z : Fin n → R) {r : ℕ} (σ : Fin (r + 1) → Fin n) (a : Fin (r + 1) → Fin n → ℕ) (i : Fin (r + 1)) : R

The generators of the K-shape.

Equations

• Hironaka.Resolution.kGen z σ a i = (∏ i' : Fin (r + 1) with i' < i, Hironaka.Resolution.monomialOf z (a i')) * Function.update (z ∘ σ) (Fin.last r) 1 i

theorem Hironaka.Resolution.chainKIdeal_eq_span_range_kGen {R : Type u_1} [CommRing R] {n : ℕ} (z : Fin n → R) {r : ℕ} (σ : Fin (r + 1) → Fin n) (a : Fin (r + 1) → Fin n → ℕ) : (chainKIdeal (z ∘ σ) fun (i : Fin (r + 1)) => monomialOf z (a i)) = Ideal.span (Set.range (kGen z σ a))

The K-shape is the span of its generators.

def Hironaka.Resolution.iGen {R : Type u_1} [CommRing R] {n : ℕ} (z : Fin n → R) {r : ℕ} (σ : Fin (r + 1) → Fin n) (a : Fin (r + 1) → Fin n → ℕ) (i : Fin (r + 1)) : R

The generators of the un-isolated form.

Equations

• Hironaka.Resolution.iGen z σ a i = (∏ i' : Fin (r + 1) with i' < i, Hironaka.Resolution.monomialOf z (a i')) * z (σ i)

theorem Hironaka.Resolution.chainIdeal_eq_span_range_iGen {R : Type u_1} [CommRing R] {n : ℕ} (z : Fin n → R) {r : ℕ} (σ : Fin (r + 1) → Fin n) (a : Fin (r + 1) → Fin n → ℕ) : (chainIdeal (z ∘ σ) fun (i : Fin (r + 1)) => monomialOf z (a i)) = Ideal.span (Set.range (iGen z σ a))

The un-isolated form is the span of its generators.

theorem Hironaka.Resolution.kGen_eq_of_le {R : Type u_1} [CommRing R] {n : ℕ} (z : Fin n → R) {r : ℕ} (σ : Fin (r + 1) → Fin n) (a : Fin (r + 1) → Fin n → ℕ) {t₀ : ℕ} (ht₀ : t₀ < r) (hmin : ∀ (i : Fin (r + 1)), ↑i < t₀ → a i = 0) {i : Fin (r + 1)} (hi : ↑i ≤ t₀) : kGen z σ a i = z (σ i)

Below the first level carrying a nontrivial monomial the K-generator is the chain coordinate.

theorem Hironaka.Resolution.iGen_eq_of_le {R : Type u_1} [CommRing R] {n : ℕ} (z : Fin n → R) {r : ℕ} (σ : Fin (r + 1) → Fin n) (a : Fin (r + 1) → Fin n → ℕ) {t₀ : ℕ} (hmin : ∀ (i : Fin (r + 1)), ↑i < t₀ → a i = 0) {i : Fin (r + 1)} (hi : ↑i ≤ t₀) : iGen z σ a i = z (σ i)

Below the first nontrivial level the generator of the un-isolated form is the chain coordinate.

theorem Hironaka.Resolution.prod_mem_span_of_lt {R : Type u_1} [CommRing R] {n : ℕ} (z : Fin n → R) {r : ℕ} (a : Fin (r + 1) → Fin n → ℕ) (C : Set (Fin n)) (ha : ∀ (i : Fin (r + 1)) (k : Fin n), a i k ≠ 0 → k ∈ C) {t₀ : Fin (r + 1)} (ha₀ : a t₀ ≠ 0) {i : Fin (r + 1)} (hi : t₀ < i) : ∏ i' : Fin (r + 1) with i' < i, monomialOf z (a i') ∈ Ideal.span (z '' C)

Beyond a level whose monomial is nontrivial the generators lie in (z_C).

theorem Hironaka.Resolution.kGen_mem_span_of_lt {R : Type u_1} [CommRing R] {n : ℕ} (z : Fin n → R) {r : ℕ} (σ : Fin (r + 1) → Fin n) (a : Fin (r + 1) → Fin n → ℕ) (C : Set (Fin n)) (ha : ∀ (i : Fin (r + 1)) (k : Fin n), a i k ≠ 0 → k ∈ C) {t₀ : Fin (r + 1)} (ha₀ : a t₀ ≠ 0) {i : Fin (r + 1)} (hi : t₀ < i) : kGen z σ a i ∈ Ideal.span (z '' C)

Beyond a nontrivial level the K-generators lie in (z_C).

theorem Hironaka.Resolution.iGen_mem_span_of_lt {R : Type u_1} [CommRing R] {n : ℕ} (z : Fin n → R) {r : ℕ} (σ : Fin (r + 1) → Fin n) (a : Fin (r + 1) → Fin n → ℕ) (C : Set (Fin n)) (ha : ∀ (i : Fin (r + 1)) (k : Fin n), a i k ≠ 0 → k ∈ C) {t₀ : Fin (r + 1)} (ha₀ : a t₀ ≠ 0) {i : Fin (r + 1)} (hi : t₀ < i) : iGen z σ a i ∈ Ideal.span (z '' C)

Beyond a nontrivial level the generators of the un-isolated form lie in (z_C).

theorem Hironaka.Resolution.exists_update_chainKIdeal_eq {R : Type u_1} [CommRing R] [IsRegularLocalRing R] {n : ℕ} {z : Fin n → R} (hz : IsLocalRing.IsRegularSystemOfParameters z) {r : ℕ} (σ : Fin (r + 1) → Fin n) (hσ : Function.Injective σ) (C : Set (Fin n)) (hCσ : ∀ k ∈ C, k ∉ Set.range σ) (a : Fin (r + 1) → Fin n → ℕ) (ha : ∀ (i : Fin (r + 1)) (k : Fin n), a i k ≠ 0 → k ∈ C) (hne : ∃ (i : Fin (r + 1)), ↑i < r ∧ a i ≠ 0) {x : R} (hx : x ∈ chainKIdeal (z ∘ σ) fun (i : Fin (r + 1)) => monomialOf z (a i)) (hx2 : x ∉ Ideal.span (z '' C) ⊔ IsLocalRing.maximalIdeal R ^ 2) : ∃ (t : Fin (r + 1)), ↑t < r ∧ (∀ (i : Fin (r + 1)), ↑i < ↑t → a i = 0) ∧ IsLocalRing.IsRegularSystemOfParameters (Function.update z (σ t) x) ∧ (chainKIdeal (z ∘ σ) fun (i : Fin (r + 1)) => monomialOf z (a i)) = chainKIdeal (Function.update z (σ t) x ∘ σ) fun (i : Fin (r + 1)) => monomialOf (Function.update z (σ t) x) (a i)

Re-basing the flag to an element x ∈ K of order 1 whose hypersurface has snc with the members.

theorem Hironaka.Resolution.prod_mem_span_singleton_of_lt {R : Type u_1} [CommRing R] {n : ℕ} (z : Fin n → R) {r : ℕ} (a : Fin (r + 1) → Fin n → ℕ) {t₀ : Fin (r + 1)} {k : Fin n} (hak : a t₀ k ≠ 0) {i : Fin (r + 1)} (hi : t₀ < i) : ∏ i' : Fin (r + 1) with i' < i, monomialOf z (a i') ∈ Ideal.span {z k}

A chain product beyond a level with a nontrivial exponent at k lies in (z k).

theorem Hironaka.Resolution.exists_update_chainIdeal_eq {R : Type u_1} [CommRing R] [IsRegularLocalRing R] {n : ℕ} {z : Fin n → R} (hz : IsLocalRing.IsRegularSystemOfParameters z) {r : ℕ} (σ : Fin (r + 1) → Fin n) (hσ : Function.Injective σ) (C : Set (Fin n)) (hCσ : ∀ k ∈ C, k ∉ Set.range σ) (a : Fin (r + 1) → Fin n → ℕ) (ha : ∀ (i : Fin (r + 1)) (k : Fin n), a i k ≠ 0 → k ∈ C) {x : R} (hx : x ∈ chainIdeal (z ∘ σ) fun (i : Fin (r + 1)) => monomialOf z (a i)) (hx2 : x ∉ Ideal.span (z '' C) ⊔ IsLocalRing.maximalIdeal R ^ 2) : ∃ (t : Fin (r + 1)), (∀ (i : Fin (r + 1)), ↑i < ↑t → a i = 0) ∧ IsLocalRing.IsRegularSystemOfParameters (Function.update z (σ t) x) ∧ (chainIdeal (z ∘ σ) fun (i : Fin (r + 1)) => monomialOf z (a i)) = chainIdeal (Function.update z (σ t) x ∘ σ) fun (i : Fin (r + 1)) => monomialOf (Function.update z (σ t) x) (a i)

Re-basing for the un-isolated form (t ≤ r; t = r is the normal parameter).

theorem Hironaka.Resolution.span_range_update_eq_of_mem_chainIdeal {R : Type u_1} [CommRing R] [IsRegularLocalRing R] {n : ℕ} {z : Fin n → R} (hz : IsLocalRing.IsRegularSystemOfParameters z) {r : ℕ} (σ : Fin (r + 1) → Fin n) (hσ : Function.Injective σ) (a : Fin (r + 1) → Fin n → ℕ) {x : R} (hx : x ∈ chainIdeal (z ∘ σ) fun (i : Fin (r + 1)) => monomialOf z (a i)) (t : Fin (r + 1)) (hupd : IsLocalRing.IsRegularSystemOfParameters (Function.update z (σ t) x)) : Ideal.span (Set.range (Function.update z (σ t) x ∘ σ)) = Ideal.span (Set.range (z ∘ σ))

The absorption transfer: with x in the un- isolated form and update z (σ t) x a regular system, the chain's span is unchanged.

theorem Hironaka.Resolution.stratumIn_of_stratumIn_update_chainKIdeal {R : Type u_1} [CommRing R] [IsRegularLocalRing R] {n : ℕ} {z : Fin n → R} (hz : IsLocalRing.IsRegularSystemOfParameters z) {r : ℕ} (σ : Fin (r + 1) → Fin n) (hσ : Function.Injective σ) (C : Set (Fin n)) (hCσ : ∀ k ∈ C, k ∉ Set.range σ) (a : Fin (r + 1) → Fin n → ℕ) (b : Fin n → ℕ) {x : R} (hx : x ∈ chainKIdeal (z ∘ σ) fun (i : Fin (r + 1)) => monomialOf z (a i)) (t : Fin (r + 1)) (ht : ∀ (i : Fin (r + 1)), ↑i < ↑t → a i = 0) (hupd : IsLocalRing.IsRegularSystemOfParameters (Function.update z (σ t) x)) {Z : Ideal R} (h : StratumIn (Function.update z (σ t) x) C σ a b Z) : StratumIn z C σ a b Z

The transfer back from the re-based system, K-shape: a stratum in the coordinates update z (σ t) x is a stratum in z.

theorem Hironaka.Resolution.stratumIn_of_stratumIn_update_chainIdeal {R : Type u_1} [CommRing R] [IsRegularLocalRing R] {n : ℕ} {z : Fin n → R} (hz : IsLocalRing.IsRegularSystemOfParameters z) {r : ℕ} (σ : Fin (r + 1) → Fin n) (hσ : Function.Injective σ) (C : Set (Fin n)) (hCσ : ∀ k ∈ C, k ∉ Set.range σ) (a : Fin (r + 1) → Fin n → ℕ) (b : Fin n → ℕ) {x : R} (hx : x ∈ chainIdeal (z ∘ σ) fun (i : Fin (r + 1)) => monomialOf z (a i)) (t : Fin (r + 1)) (ht : ∀ (i : Fin (r + 1)), ↑i < ↑t → a i = 0) (hupd : IsLocalRing.IsRegularSystemOfParameters (Function.update z (σ t) x)) {Z : Ideal R} (h : StratumIn (Function.update z (σ t) x) C σ a b Z) : StratumIn z C σ a b Z

The transfer for the un-isolated form.

theorem Hironaka.Resolution.terminalIn_of_terminalIn_update {R : Type u_1} [CommRing R] [IsRegularLocalRing R] {n : ℕ} {z : Fin n → R} (hz : IsLocalRing.IsRegularSystemOfParameters z) {r : ℕ} (σ : Fin (r + 1) → Fin n) (hσ : Function.Injective σ) (C : Set (Fin n)) (hCσ : ∀ k ∈ C, k ∉ Set.range σ) (a : Fin (r + 1) → Fin n → ℕ) {x : R} (hx : x ∈ chainIdeal (z ∘ σ) fun (i : Fin (r + 1)) => monomialOf z (a i)) (t : Fin (r + 1)) (hupd : IsLocalRing.IsRegularSystemOfParameters (Function.update z (σ t) x)) {Z : Ideal R} (h : TerminalIn (Function.update z (σ t) x) C σ Z) : TerminalIn z C σ Z

The transfer for a terminal-normal stratum.