The ideal of maximal contacts and MC-invariance

For m ≥ 1 the maximal contact ideal is MC_m(I) = D^(m-1) I [Kol07, 51 and Definition 79]; I is MC-invariant with respect to m if MC_m(I) · D(I) ⊂ I [Kol07, 53, (53.1)]. Kollár's note to Definition 79 — MC(I) has order 1 where ord I = m and order 0 where ord I < m, so cosupp MC(I) = cosupp (I, m) — is the order statement of [Kol07, Lemma 74(3)]. The local construction of maximal contact [Kol07, 51.2]: if ord I = m there is h ∈ MC_m(I) of order 1, and h is the first member of a system of coordinates, with ∂'₁ h = 1 (exists_maximalContact). Two examples: ⟨xᵢ^m⟩ is MC-invariant and ⟨xᵢ xⱼ⟩ is not MC-invariant with respect to 2.

The coordinate half of the construction needs a system of coordinates containing a given h ∈ 𝔪 ∖ 𝔪²: h = ∑ aⱼ xⱼ with some aᵢ a unit (else h ∈ 𝔪²), so x with xᵢ replaced by h still generates 𝔪 (exists_span_update), and the change of coordinates of Hironaka/Algebra/Local/Coords.lean applies under the standing hypothesis that the ∂ᵢ span the derivations (as in changeCoordsOfSpans); reindex moves h to the first position.

Reindexing and replacing a coordinate

def IsLocalRing.RegularCoords.reindex {R : Type u_1} [CommRing R] [IsRegularLocalRing R] [Algebra ℚ R] {n : ℕ} (c : RegularCoords R n) (σ : Equiv.Perm (Fin n)) : RegularCoords R n

Reindexing a coordinate structure along a permutation of the indices.

Equations

• c.reindex σ = { x := c.x ∘ ⇑σ, pderiv := c.pderiv ∘ ⇑σ, span_x := ⋯, card := ⋯, pderiv_x := ⋯, pderiv_comm := ⋯ }

@[simp]

theorem IsLocalRing.RegularCoords.reindex_x {R : Type u_1} [CommRing R] [IsRegularLocalRing R] [Algebra ℚ R] {n : ℕ} (c : RegularCoords R n) (σ : Equiv.Perm (Fin n)) (i : Fin n) : (c.reindex σ).x i = c.x (σ i)

@[simp]

theorem IsLocalRing.RegularCoords.reindex_pderiv {R : Type u_1} [CommRing R] [IsRegularLocalRing R] [Algebra ℚ R] {n : ℕ} (c : RegularCoords R n) (σ : Equiv.Perm (Fin n)) (i : Fin n) : (c.reindex σ).pderiv i = c.pderiv (σ i)

theorem IsLocalRing.RegularCoords.exists_span_update {R : Type u_1} [CommRing R] [IsRegularLocalRing R] [Algebra ℚ R] {n : ℕ} (c : RegularCoords R n) {h : R} (hh : h ∈ maximalIdeal R) (hh' : h ∉ maximalIdeal R ^ 2) : ∃ (i : Fin n), maximalIdeal R = Ideal.span (Set.range (Function.update c.x i h))

An element h ∈ 𝔪 ∖ 𝔪² can replace one of the coordinates as a generator of 𝔪 (the coordinate step of the local construction of maximal contact, [Kol07, 51.2]).

theorem IsLocalRing.RegularCoords.exists_coords_x_eq {R : Type u_1} [CommRing R] [IsRegularLocalRing R] [Algebra ℚ R] {n : ℕ} (c : RegularCoords R n) (hs : c.SpansDerivations ℚ) {h : R} (hh : ordElem h = 1) : ∃ (c' : RegularCoords R n) (i : Fin n), c'.x i = h

An element of order 1 is a member of some system of coordinates, given that the ∂ᵢ span the derivations (the coordinate half of [Kol07, 51.2]).

theorem IsLocalRing.RegularCoords.exists_coords_x_zero_eq {R : Type u_1} [CommRing R] [IsRegularLocalRing R] [Algebra ℚ R] {n : ℕ} (c : RegularCoords R n) (hs : c.SpansDerivations ℚ) {h : R} (hh : ordElem h = 1) : ∃ (hn : 0 < n) (c' : RegularCoords R n), c'.x ⟨0, hn⟩ = h ∧ (c'.pderiv ⟨0, hn⟩) h = 1

An element h of order 1 is the first coordinate of some system of coordinates x', with ∂'₁ h = 1.

The maximal contact ideal

def IsLocalRing.RegularCoords.MC {R : Type u_1} [CommRing R] [IsRegularLocalRing R] [Algebra ℚ R] {n : ℕ} (c : RegularCoords R n) (I : Ideal R) (m : ℕ) : Ideal R

The maximal contact ideal MC_m(I) = D^(m-1) I [Kol07, 51 and Definition 79].

Equations

• c.MC I m = c.Dpow (m - 1) I

def IsLocalRing.RegularCoords.IsMCInvariant {R : Type u_1} [CommRing R] [IsRegularLocalRing R] [Algebra ℚ R] {n : ℕ} (c : RegularCoords R n) (I : Ideal R) (m : ℕ) : Prop

I is MC-invariant with respect to m if MC_m(I) · D(I) ≤ I [Kol07, 53, (53.1)].

Equations

• c.IsMCInvariant I m = (c.MC I m * c.D I ≤ I)

theorem IsLocalRing.RegularCoords.ord_MC_of_ord_eq {R : Type u_1} [CommRing R] [IsRegularLocalRing R] [Algebra ℚ R] {n : ℕ} (c : RegularCoords R n) {I : Ideal R} {m : ℕ} (hm : 1 ≤ m) (hI : ord I = ↑m) : ord (c.MC I m) = 1

MC(I) has order 1 where ord I = m (the note to [Kol07, Definition 79]).

theorem IsLocalRing.RegularCoords.MC_eq_top_of_ord_lt {R : Type u_1} [CommRing R] [IsRegularLocalRing R] [Algebra ℚ R] {n : ℕ} (c : RegularCoords R n) {I : Ideal R} {m : ℕ} (hm : 1 ≤ m) (hI : ord I < ↑m) : c.MC I m = ⊤

MC(I) has order 0 where ord I < m (the note to [Kol07, Definition 79]).

theorem IsLocalRing.RegularCoords.exists_mem_MC_ordElem_eq_one {R : Type u_1} [CommRing R] [IsRegularLocalRing R] [Algebra ℚ R] {n : ℕ} (c : RegularCoords R n) {I : Ideal R} {m : ℕ} (hm : 1 ≤ m) (hI : ord I = ↑m) : ∃ h ∈ c.MC I m, ordElem h = 1

If ord I = m ≥ 1 there is h ∈ MC_m(I) of order 1 ([Kol07, 51.2]; "pick x₁ ∈ MC(I) that has order 1 at p" in the proof of [Kol07, Proposition 99]).

theorem IsLocalRing.RegularCoords.exists_maximalContact {R : Type u_1} [CommRing R] [IsRegularLocalRing R] [Algebra ℚ R] {n : ℕ} (c : RegularCoords R n) (hs : c.SpansDerivations ℚ) {I : Ideal R} {m : ℕ} (hm : 1 ≤ m) (hI : ord I = ↑m) : ∃ h ∈ c.MC I m, ordElem h = 1 ∧ ∃ (hn : 0 < n) (c' : RegularCoords R n), c'.x ⟨0, hn⟩ = h ∧ (c'.pderiv ⟨0, hn⟩) h = 1

The local construction of maximal contact [Kol07, 51.2]: if ord I = m ≥ 1 then some h ∈ MC_m(I) has order 1 and is the first coordinate of a system of coordinates x' with ∂'₁ h = 1 (given that the ∂ᵢ span the derivations).

Examples

theorem IsLocalRing.RegularCoords.MC_span_singleton_x_pow {R : Type u_1} [CommRing R] [IsRegularLocalRing R] [Algebra ℚ R] {n : ℕ} (c : RegularCoords R n) (i : Fin n) {m : ℕ} (hm : 1 ≤ m) : c.MC (Ideal.span {c.x i ^ m}) m = Ideal.span {c.x i}

MC_m ⟨xᵢ^m⟩ = ⟨xᵢ⟩ for m ≥ 1.

theorem IsLocalRing.RegularCoords.isMCInvariant_span_singleton_x_pow {R : Type u_1} [CommRing R] [IsRegularLocalRing R] [Algebra ℚ R] {n : ℕ} (c : RegularCoords R n) (i : Fin n) {m : ℕ} (hm : 1 ≤ m) : c.IsMCInvariant (Ideal.span {c.x i ^ m}) m

⟨xᵢ^m⟩ is MC-invariant with respect to m ≥ 1 (MC = ⟨xᵢ⟩, D ⟨xᵢ^m⟩ = ⟨xᵢ^(m-1)⟩).

theorem IsLocalRing.RegularCoords.not_isMCInvariant_span_singleton_x_mul_x {R : Type u_1} [CommRing R] [IsRegularLocalRing R] [Algebra ℚ R] {n : ℕ} (c : RegularCoords R n) {i j : Fin n} (hij : i ≠ j) (h : c.x i ^ 2 ∉ Ideal.span {c.x i * c.x j}) : ¬c.IsMCInvariant (Ideal.span {c.x i * c.x j}) 2

⟨xᵢ xⱼ⟩ is not MC-invariant with respect to 2 as soon as xᵢ² ∉ ⟨xᵢ xⱼ⟩ (which holds in ℚ⟦x₁, x₂⟧, X_sq_notMem_span_X_mul_X), since MC₂ ⟨xᵢ xⱼ⟩ = D ⟨xᵢ xⱼ⟩ = ⟨xᵢ, xⱼ⟩.