Smoothness of the model blow-up

The point blow-up of 𝔸ⁿ is non-singular [Hau14, Example 4.55]; for a general coordinate subspace L, B_L 𝔸ⁿ_A is smooth over A of relative dimension n. Smoothness of relative dimension n is Zariski-local on the source (Mathlib's HasRingHomProperty for SmoothOfRelativeDimension n), the charts U_j = Spec A[x] are open immersions covering B (Hironaka.Scheme.BlowUp.CoordinateSubspace.Charts), and over the base each chart is Spec (π_j) with π_j an A-algebra endomorphism of A[x], so U_j → B → Spec A is Spec (A → A[x]), which is standard smooth of relative dimension n: the polynomial algebra has the submersive presentation with the n variables as generators and no relations (Mathlib's PreSubmersivePresentation.naive with an empty relation index; the Jacobian is the determinant of the endomorphism of the zero module, 1). Mathlib at the pinned version has no instance IsStandardSmoothOfRelativeDimension n R (MvPolynomial (Fin n) R); mvPolynomial_isStandardSmoothOfRelativeDimension supplies it, transported from the quotient by the zero ideal along RespectsIso. The smoothness of affine space and of the model blow-up is used wherever the model is compared with a blow-up of a smooth centre (Hironaka.Scheme.Smooth.BlowUpSmoothChart, Hironaka.Resolution.Algebraic.Kol07.Thm36.AffineSpace, Hironaka.Scheme.IdealSheaf.Order.AffineSpace).

theorem AlgebraicGeometry.CoordinateSubspace.isStandardSmoothOfRelativeDimension_algebraMap_of_algEquiv {A : Type u} [CommRing A] {S : Type v} {T : Type w} [CommRing S] [CommRing T] [Algebra A S] [Algebra A T] (e : S ≃ₐ[A] T) {m : ℕ} (h : RingHom.IsStandardSmoothOfRelativeDimension m (algebraMap A S)) : RingHom.IsStandardSmoothOfRelativeDimension m (algebraMap A T)

Standard smoothness of relative dimension m over A transports along an A-algebra isomorphism (the ring-hom form, so that the universes of S and T may differ).

noncomputable def AlgebraicGeometry.CoordinateSubspace.mvPolynomialPreSubmersivePresentation (A : Type u) [CommRing A] (σ : Type v) : Algebra.PreSubmersivePresentation A (MvPolynomial σ A ⧸ Ideal.span (Set.range Empty.elim)) σ Empty

The pre-submersive presentation of A[x_i : i ∈ σ] (as the quotient by the zero ideal) with the variables as generators and no relations.

Equations

• AlgebraicGeometry.CoordinateSubspace.mvPolynomialPreSubmersivePresentation A σ = Algebra.PreSubmersivePresentation.naive Empty.elim ⋯ (Function.surjInv ⋯) ⋯

noncomputable def AlgebraicGeometry.CoordinateSubspace.mvPolynomialSubmersivePresentation (A : Type u) [CommRing A] (σ : Type v) : Algebra.SubmersivePresentation A (MvPolynomial σ A ⧸ Ideal.span (Set.range Empty.elim)) σ Empty

The ring-level input: the empty-relation presentation is submersive — its Jacobian is the determinant of the endomorphism of the zero module.

Equations

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

theorem AlgebraicGeometry.CoordinateSubspace.isStandardSmoothOfRelativeDimension_mvPolynomial_quotient (A : Type u) [CommRing A] (σ : Type v) [Finite σ] : Algebra.IsStandardSmoothOfRelativeDimension (Nat.card σ) A (MvPolynomial σ A ⧸ Ideal.span (Set.range Empty.elim))

theorem AlgebraicGeometry.CoordinateSubspace.ringHom_isStandardSmoothOfRelativeDimension_algebraMap_mvPolynomial (A : Type u) [CommRing A] (σ : Type v) [Finite σ] : RingHom.IsStandardSmoothOfRelativeDimension (Nat.card σ) (algebraMap A (MvPolynomial σ A))

The ring-level input (absent from Mathlib at the pinned version): A → A[x_i : i ∈ σ] is standard smooth of relative dimension |σ|.

instance AlgebraicGeometry.CoordinateSubspace.mvPolynomial_isStandardSmoothOfRelativeDimension (A : Type u) [CommRing A] (σ : Type v) [Finite σ] : Algebra.IsStandardSmoothOfRelativeDimension (Nat.card σ) A (MvPolynomial σ A)

A[x_i : i ∈ σ] is standard smooth of relative dimension |σ| over A.

theorem AlgebraicGeometry.CoordinateSubspace.smoothOfRelativeDimension_Spec_map_algebraMap_mvPolynomial (A : Type u) [CommRing A] (n : ℕ) : SmoothOfRelativeDimension n (Spec.map (CommRingCat.ofHom (algebraMap A (MvPolynomial (Fin n) A))))

𝔸ⁿ_A → Spec A is smooth of relative dimension n.

theorem AlgebraicGeometry.CoordinateSubspace.smoothOfRelativeDimension_modelBlowUp (A : Type u) [CommRing A] (n r : ℕ) : SmoothOfRelativeDimension n (CategoryTheory.CategoryStruct.comp (affineBlowUp.π (centerIdeal A n r)) (Spec.map (CommRingCat.ofHom (algebraMap A (MvPolynomial (Fin n) A)))))

The model blow-up is smooth ([Hau14, Example 4.55] for a point; here for any coordinate subspace): B_L 𝔸ⁿ_A is smooth over A of relative dimension n — Zariski-local on the source, and on the chart U_j the map to Spec A is Spec (A → A[x]).