The coordinate ring of 𝔸ⁿ as a polynomial ring over 𝒪(L)

For the coordinate subspace L = V(x_0, …, x_{r-1}) ⊆ 𝔸ⁿ_A (r ≤ n), A[x] ≅ 𝒪(L)[u_0, …, u_{r-1}] with 𝒪(L) = A[x]/I ≅ A[x_r, …, x_{n-1}] (quotientCenterAlgEquiv of Hironaka.Scheme.BlowUp.CoordinateSubspace.Exceptional), x_i ↦ u_i for i < r and x_i ↦ x̄_i for i ≥ r (centerSplitEquiv). Under it the centre ideal I is the ideal (u_0, …, u_{r-1}) of the polynomial ring, and I^k is the ideal of polynomials all of whose monomials have degree ≥ k (mem_span_range_X_pow_iff); the degree-k homogeneous component of such a polynomial is its initial form, and initial forms multiply (homogeneousComponent_mul_of_mem). This is [Mat89, Theorem 16.2] (the associated graded ring of an ideal generated by a regular sequence is the polynomial ring) for the coordinate ideal, by degree counting — the algebraic input for the identification of the exceptional divisor with ℙ^{r-1}_L (Hironaka.Scheme.BlowUp.CoordinateSubspace.ReesInitial).

theorem AlgebraicGeometry.CoordinateSubspace.prod_pow_mem_pow {σ : Type u_1} {S : Type u_2} [CommRing S] (J : Ideal S) (s : Finset σ) (e : σ → ℕ) (x : σ → S) (hx : ∀ (i : σ), x i ∈ J) : ∏ i ∈ s, x i ^ e i ∈ J ^ ∑ i ∈ s, e i

Products of powers of elements of an ideal lie in the corresponding power of the ideal.

theorem AlgebraicGeometry.CoordinateSubspace.mem_span_range_X_pow_of_forall {σ : Type u_1} {S : Type u_2} [CommRing S] {k : ℕ} {p : MvPolynomial σ S} (h : ∀ d ∈ p.support, k ≤ Finsupp.degree d) : p ∈ Ideal.span (Set.range MvPolynomial.X) ^ k

A polynomial all of whose monomials have degree ≥ k lies in (X_i)^k.

theorem AlgebraicGeometry.CoordinateSubspace.forall_degree_of_mem_span_range_X_pow {σ : Type u_1} {S : Type u_2} [CommRing S] {k : ℕ} {p : MvPolynomial σ S} (hp : p ∈ Ideal.span (Set.range MvPolynomial.X) ^ k) (d : σ →₀ ℕ) : d ∈ p.support → k ≤ Finsupp.degree d

Every monomial of an element of (X_i)^k has degree ≥ k.

theorem AlgebraicGeometry.CoordinateSubspace.mem_span_range_X_pow_iff {σ : Type u_1} {S : Type u_2} [CommRing S] {k : ℕ} {p : MvPolynomial σ S} : p ∈ Ideal.span (Set.range MvPolynomial.X) ^ k ↔ ∀ d ∈ p.support, k ≤ Finsupp.degree d

(X_i)^k is the ideal of polynomials all of whose monomials have degree ≥ k.

theorem AlgebraicGeometry.CoordinateSubspace.homogeneousComponent_mem_span_range_X_pow {σ : Type u_1} {S : Type u_2} [CommRing S] (k : ℕ) (p : MvPolynomial σ S) : (MvPolynomial.homogeneousComponent k) p ∈ Ideal.span (Set.range MvPolynomial.X) ^ k

The homogeneous component of degree k lies in (X_i)^k.

theorem AlgebraicGeometry.CoordinateSubspace.sub_homogeneousComponent_mem {σ : Type u_1} {S : Type u_2} [CommRing S] {k : ℕ} {p : MvPolynomial σ S} (hp : p ∈ Ideal.span (Set.range MvPolynomial.X) ^ k) : p - (MvPolynomial.homogeneousComponent k) p ∈ Ideal.span (Set.range MvPolynomial.X) ^ (k + 1)

For p ∈ (X_i)^k, p minus its initial form lies in (X_i)^(k+1).

theorem AlgebraicGeometry.CoordinateSubspace.homogeneousComponent_eq_zero_iff_mem_succ {σ : Type u_1} {S : Type u_2} [CommRing S] {k : ℕ} {p : MvPolynomial σ S} (hp : p ∈ Ideal.span (Set.range MvPolynomial.X) ^ k) : (MvPolynomial.homogeneousComponent k) p = 0 ↔ p ∈ Ideal.span (Set.range MvPolynomial.X) ^ (k + 1)

For p ∈ (X_i)^k, the initial form vanishes iff p ∈ (X_i)^(k+1).

theorem AlgebraicGeometry.CoordinateSubspace.homogeneousComponent_mul_of_mem {σ : Type u_1} {S : Type u_2} [CommRing S] {k l : ℕ} {a b : MvPolynomial σ S} (ha : a ∈ Ideal.span (Set.range MvPolynomial.X) ^ k) (hb : b ∈ Ideal.span (Set.range MvPolynomial.X) ^ l) : (MvPolynomial.homogeneousComponent (k + l)) (a * b) = (MvPolynomial.homogeneousComponent k) a * (MvPolynomial.homogeneousComponent l) b

Initial forms multiply: for a ∈ (X_i)^k, b ∈ (X_i)^l, the degree-(k + l) component of a * b is the product of the degree-k component of a and the degree-l component of b.

def AlgebraicGeometry.CoordinateSubspace.splitFin (n r : ℕ) (hrn : r ≤ n) : Fin n ≃ Fin r ⊕ { i : Fin n // ¬↑i < r }

The variables of 𝔸ⁿ split into the r center variables (Fin r) and the rest.

Equations

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

theorem AlgebraicGeometry.CoordinateSubspace.splitFin_apply_of_lt (n r : ℕ) (hrn : r ≤ n) {i : Fin n} (h : ↑i < r) : (splitFin n r hrn) i = Sum.inl ⟨↑i, h⟩

theorem AlgebraicGeometry.CoordinateSubspace.splitFin_apply_of_not_lt (n r : ℕ) (hrn : r ≤ n) {i : Fin n} (h : ¬↑i < r) : (splitFin n r hrn) i = Sum.inr ⟨i, h⟩

noncomputable def AlgebraicGeometry.CoordinateSubspace.centerSplitEquiv (A : Type u) [CommRing A] (n r : ℕ) (hrn : r ≤ n) : MvPolynomial (Fin n) A ≃ₐ[A] MvPolynomial (Fin r) (MvPolynomial (Fin n) A ⧸ centerIdeal A n r)

A[x_0, …, x_{n-1}] ≃ₐ[A] (A[x]/I)[u_0, …, u_{r-1}], x_i ↦ u_i for i < r and x_i ↦ x̄_i for i ≥ r, through A[x]/I ≃ A[x_i : r ≤ i] (quotientCenterAlgEquiv).

Equations

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

theorem AlgebraicGeometry.CoordinateSubspace.centerSplitEquiv_X_of_lt (A : Type u) [CommRing A] (n r : ℕ) (hrn : r ≤ n) {i : Fin n} (h : ↑i < r) : (centerSplitEquiv A n r hrn) (MvPolynomial.X i) = MvPolynomial.X ⟨↑i, h⟩

theorem AlgebraicGeometry.CoordinateSubspace.centerSplitEquiv_X_of_not_lt (A : Type u) [CommRing A] (n r : ℕ) (hrn : r ≤ n) {i : Fin n} (h : ¬↑i < r) : (centerSplitEquiv A n r hrn) (MvPolynomial.X i) = MvPolynomial.C ((Ideal.Quotient.mk (centerIdeal A n r)) (MvPolynomial.X i))

theorem AlgebraicGeometry.CoordinateSubspace.constantCoeff_comp_centerSplitEquiv (A : Type u) [CommRing A] (n r : ℕ) (hrn : r ≤ n) : MvPolynomial.constantCoeff.comp ↑(centerSplitEquiv A n r hrn) = Ideal.Quotient.mk (centerIdeal A n r)

The constant term of centerSplitEquiv p is the class of p in A[x]/I.

theorem AlgebraicGeometry.CoordinateSubspace.map_centerIdeal_centerSplitEquiv (A : Type u) [CommRing A] (n r : ℕ) (hrn : r ≤ n) : Ideal.map (↑(centerSplitEquiv A n r hrn)) (centerIdeal A n r) = Ideal.span (Set.range MvPolynomial.X)

Under centerSplitEquiv the center ideal is the ideal (u_0, …, u_{r-1}).

theorem AlgebraicGeometry.CoordinateSubspace.mem_pow_iff_centerSplitEquiv_mem (A : Type u) [CommRing A] (n r : ℕ) (hrn : r ≤ n) {k : ℕ} {c : MvPolynomial (Fin n) A} : c ∈ centerIdeal A n r ^ k ↔ (centerSplitEquiv A n r hrn) c ∈ Ideal.span (Set.range MvPolynomial.X) ^ k

p ∈ I^k iff its image under centerSplitEquiv lies in (u_0, …, u_{r-1})^k.