The hypersurface x₁ = 0 as a coordinate ring

Kollár picks local coordinates x₁, …, xₙ with S = (x₁ = 0) and notes that ∂f/∂xᵢ |_S = ∂(f|_S)/∂xᵢ for i > 1, "but ∂(f|_S)/∂x₁ does not even make sense" [Kol07, 87]. In the local model: R̄ := R/⟨x₁⟩ is a regular local ring (isRegularLocalRing_quotient_span_image_lt of Hironaka/Algebra/Local/RegularSystem.lean) with coordinates x̄₂, …, x̄ₙ and derivations ∂̄ⱼ (j ≥ 2) induced by ∂ⱼ, which preserve ⟨x₁⟩ because ∂ⱼ x₁ = 0; ∂̄ⱼ x̄ₗ = δⱼₗ; so R̄ carries a RegularCoords structure on n − 1 coordinates, and (∂ⱼ f)‾ = ∂̄ⱼ f̄.

Kollár's x₁ is any coordinate x_{i₀}; the other coordinates are enumerated by Fin.succAbove i₀. The general descent of a derivation to a quotient by an invariant ideal is Derivation.quotientOfMapLE. The structure quotientCoords is the setting of the restriction (87.1) in Hironaka/Algebra/Local/LogDeriv.lean.

noncomputable def Derivation.quotientLinear {k : Type u_1} {R : Type u_2} [CommRing k] [CommRing R] [Algebra k R] (D : Derivation k R R) (J : Ideal R) (hJ : ∀ f ∈ J, D f ∈ J) : R ⧸ J →ₗ[k] R ⧸ J

The k-linear map R/J → R/J induced by a derivation D with D(J) ⊆ J.

Equations

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

theorem Derivation.quotientLinear_mk {k : Type u_1} {R : Type u_2} [CommRing k] [CommRing R] [Algebra k R] (D : Derivation k R R) (J : Ideal R) (hJ : ∀ f ∈ J, D f ∈ J) (f : R) : (D.quotientLinear J hJ) ((Ideal.Quotient.mk J) f) = (Ideal.Quotient.mk J) (D f)

noncomputable def Derivation.quotientOfMapLE {k : Type u_1} {R : Type u_2} [CommRing k] [CommRing R] [Algebra k R] (D : Derivation k R R) (J : Ideal R) (hJ : ∀ f ∈ J, D f ∈ J) : Derivation k (R ⧸ J) (R ⧸ J)

A derivation D of R with D(J) ⊆ J descends to a derivation D̄ of R/J with D̄ (f̄) = (D f)‾.

Equations

• D.quotientOfMapLE J hJ = Derivation.mk' (D.quotientLinear J hJ) ⋯

@[simp]

theorem Derivation.quotientOfMapLE_mk {k : Type u_1} {R : Type u_2} [CommRing k] [CommRing R] [Algebra k R] (D : Derivation k R R) (J : Ideal R) (hJ : ∀ f ∈ J, D f ∈ J) (f : R) : (D.quotientOfMapLE J hJ) ((Ideal.Quotient.mk J) f) = (Ideal.Quotient.mk J) (D f)

theorem IsLocalRing.RegularCoords.pderiv_mem_span_x_of_ne {R : Type u_1} [CommRing R] [IsRegularLocalRing R] [Algebra ℚ R] {k : ℕ} (c : RegularCoords R (k + 1)) (i₀ : Fin (k + 1)) {j : Fin (k + 1)} (hj : j ≠ i₀) {f : R} (hf : f ∈ Ideal.span {c.x i₀}) : (c.pderiv j) f ∈ Ideal.span {c.x i₀}

∂ⱼ preserves ⟨x_{i₀}⟩ for j ≠ i₀, because ∂ⱼ x_{i₀} = 0.

noncomputable def IsLocalRing.RegularCoords.quotientPderiv {R : Type u_1} [CommRing R] [IsRegularLocalRing R] [Algebra ℚ R] {k : ℕ} (c : RegularCoords R (k + 1)) (i₀ : Fin (k + 1)) (j : Fin k) : Derivation ℚ (R ⧸ Ideal.span {c.x i₀}) (R ⧸ Ideal.span {c.x i₀})

The induced derivation ∂̄ⱼ of R̄ = R/⟨x_{i₀}⟩, from ∂_{σ j} with σ = Fin.succAbove i₀.

Equations

• c.quotientPderiv i₀ j = (c.pderiv (i₀.succAbove j)).quotientOfMapLE (Ideal.span {c.x i₀}) ⋯

@[simp]

theorem IsLocalRing.RegularCoords.quotientPderiv_mk {R : Type u_1} [CommRing R] [IsRegularLocalRing R] [Algebra ℚ R] {k : ℕ} (c : RegularCoords R (k + 1)) (i₀ : Fin (k + 1)) (j : Fin k) (f : R) : (c.quotientPderiv i₀ j) ((Ideal.Quotient.mk (Ideal.span {c.x i₀})) f) = (Ideal.Quotient.mk (Ideal.span {c.x i₀})) ((c.pderiv (i₀.succAbove j)) f)

(∂_{σ j} f)‾ = ∂̄ⱼ f̄: Kollár's ∂f/∂xᵢ |_S = ∂(f|_S)/∂xᵢ for i > 1 [Kol07, 87].

def IsLocalRing.RegularCoords.shiftPerm {k : ℕ} (i₀ : Fin (k + 1)) : Equiv.Perm (Fin (k + 1))

The permutation of the coordinates putting x_{i₀} first: 0 ↦ i₀, j.succ ↦ i₀.succAbove j.

Equations

• IsLocalRing.RegularCoords.shiftPerm i₀ = (finSuccEquiv k).trans (finSuccEquiv' i₀).symm

@[simp]

theorem IsLocalRing.RegularCoords.shiftPerm_zero {k : ℕ} (i₀ : Fin (k + 1)) : (shiftPerm i₀) 0 = i₀

@[simp]

theorem IsLocalRing.RegularCoords.shiftPerm_succ {k : ℕ} (i₀ : Fin (k + 1)) (j : Fin k) : (shiftPerm i₀) j.succ = i₀.succAbove j

theorem IsLocalRing.RegularCoords.span_x_shiftPerm {R : Type u_1} [CommRing R] [IsRegularLocalRing R] [Algebra ℚ R] {k : ℕ} (c : RegularCoords R (k + 1)) (i₀ : Fin (k + 1)) : maximalIdeal R = Ideal.span (Set.range (c.x ∘ ⇑(shiftPerm i₀)))

theorem IsLocalRing.RegularCoords.span_image_lt_one {R : Type u_1} [CommRing R] [IsRegularLocalRing R] [Algebra ℚ R] {k : ℕ} (c : RegularCoords R (k + 1)) (i₀ : Fin (k + 1)) : Ideal.span (c.x ∘ ⇑(shiftPerm i₀) '' {j : Fin (k + 1) | ↑j < 1}) = Ideal.span {c.x i₀}

instance IsLocalRing.RegularCoords.isRegularLocalRing_quotient_span_x {R : Type u_1} [CommRing R] [IsRegularLocalRing R] [Algebra ℚ R] {k : ℕ} (c : RegularCoords R (k + 1)) (i₀ : Fin (k + 1)) : IsRegularLocalRing (R ⧸ Ideal.span {c.x i₀})

R̄ = R/⟨x_{i₀}⟩ is a regular local ring (the quotient by a member of a regular system of parameters).

theorem IsLocalRing.RegularCoords.ringKrullDim_quotient_span_x_add_one {R : Type u_1} [CommRing R] [IsRegularLocalRing R] [Algebra ℚ R] {k : ℕ} (c : RegularCoords R (k + 1)) (i₀ : Fin (k + 1)) : ringKrullDim (R ⧸ Ideal.span {c.x i₀}) + 1 = ringKrullDim R

theorem IsLocalRing.RegularCoords.withBot_eq_natCast_of_add_one_eq {d : WithBot ℕ∞} {m : ℕ} (h : d + 1 = ↑(m + 1)) : d = ↑m

theorem IsLocalRing.RegularCoords.card_quotient_span_x {R : Type u_1} [CommRing R] [IsRegularLocalRing R] [Algebra ℚ R] {k : ℕ} (c : RegularCoords R (k + 1)) (i₀ : Fin (k + 1)) : ↑k = ringKrullDim (R ⧸ Ideal.span {c.x i₀})

dim R̄ = n − 1.

theorem IsLocalRing.RegularCoords.maximalIdeal_quotient_span_x {R : Type u_1} [CommRing R] [IsRegularLocalRing R] [Algebra ℚ R] {k : ℕ} (c : RegularCoords R (k + 1)) (i₀ : Fin (k + 1)) : maximalIdeal (R ⧸ Ideal.span {c.x i₀}) = Ideal.span (Set.range fun (j : Fin k) => (Ideal.Quotient.mk (Ideal.span {c.x i₀})) (c.x (i₀.succAbove j)))

The classes x̄_{σ j} generate the maximal ideal of R̄.

noncomputable def IsLocalRing.RegularCoords.quotientCoords {R : Type u_1} [CommRing R] [IsRegularLocalRing R] [Algebra ℚ R] {k : ℕ} (c : RegularCoords R (k + 1)) (i₀ : Fin (k + 1)) : RegularCoords (R ⧸ Ideal.span {c.x i₀}) k

The coordinate structure on the hypersurface ring R̄ = R/⟨x_{i₀}⟩, with coordinates x̄_{σ j} and derivations ∂̄ⱼ, where σ = Fin.succAbove i₀ (Kollár's coordinates on S = (x₁ = 0), [Kol07, 87]).

Equations

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

@[simp]

theorem IsLocalRing.RegularCoords.quotientCoords_x {R : Type u_1} [CommRing R] [IsRegularLocalRing R] [Algebra ℚ R] {k : ℕ} (c : RegularCoords R (k + 1)) (i₀ : Fin (k + 1)) (j : Fin k) : (c.quotientCoords i₀).x j = (Ideal.Quotient.mk (Ideal.span {c.x i₀})) (c.x (i₀.succAbove j))

@[simp]

theorem IsLocalRing.RegularCoords.quotientCoords_pderiv {R : Type u_1} [CommRing R] [IsRegularLocalRing R] [Algebra ℚ R] {k : ℕ} (c : RegularCoords R (k + 1)) (i₀ : Fin (k + 1)) (j : Fin k) : (c.quotientCoords i₀).pderiv j = c.quotientPderiv i₀ j

theorem IsLocalRing.RegularCoords.quotientCoords_pderiv_mk {R : Type u_1} [CommRing R] [IsRegularLocalRing R] [Algebra ℚ R] {k : ℕ} (c : RegularCoords R (k + 1)) (i₀ : Fin (k + 1)) (j : Fin k) (f : R) : ((c.quotientCoords i₀).pderiv j) ((Ideal.Quotient.mk (Ideal.span {c.x i₀})) f) = (Ideal.Quotient.mk (Ideal.span {c.x i₀})) ((c.pderiv (i₀.succAbove j)) f)

The compatibility clause ∂̄ⱼ (f̄) = (∂_{σ j} f)‾, in the form the restriction of D-balanced ideals takes as a hypothesis.