From de528bedc7ede4d0626e70137a2c779640d3dc58 Mon Sep 17 00:00:00 2001 From: Justus Springer Date: Fri, 22 May 2026 15:39:31 +0100 Subject: [PATCH] MvPolynomial is standard smooth --- Mathlib/RingTheory/Extension/Generators.lean | 12 ++++++++++++ .../Extension/Presentation/Basic.lean | 14 ++++++++++++++ .../Extension/Presentation/Submersive.lean | 19 +++++++++++++++++++ Mathlib/RingTheory/Smooth/Basic.lean | 11 +++++------ Mathlib/RingTheory/Smooth/Quotient.lean | 4 ++-- Mathlib/RingTheory/Smooth/StandardSmooth.lean | 14 ++++++++++++++ 6 files changed, 66 insertions(+), 8 deletions(-) diff --git a/Mathlib/RingTheory/Extension/Generators.lean b/Mathlib/RingTheory/Extension/Generators.lean index 5ea6b2b1bdedfd..0e050b3801dce8 100644 --- a/Mathlib/RingTheory/Extension/Generators.lean +++ b/Mathlib/RingTheory/Extension/Generators.lean @@ -139,6 +139,15 @@ noncomputable def id : Generators R R PEmpty.{w + 1} := ofSurjectiveAlgebraMap < rw [algebraMap_self] exact RingHomSurjective.is_surjective +variable (R ι) in +/-- The canonical `R`-generators of the polynomial algebra `MvPolynomial ι R`, +indexed by `ι` via the variables `X`. -/ +@[simps σ, simps -fullyApplied val] +noncomputable def mvPolynomial : Generators R (MvPolynomial ι R) ι where + val := X + σ' f := f + aeval_val_σ' := aeval_X_left_apply + /-- Construct `Generators` from an assignment `I → S` such that `R[X] → S` is surjective. -/ noncomputable def ofAlgHom {I : Type*} (f : MvPolynomial I R →ₐ[R] S) (h : Function.Surjective f) : @@ -606,6 +615,9 @@ lemma ker_eq_ker_aeval_val : P.ker = RingHom.ker (aeval P.val) := by simp only [ker, Extension.ker, toExtension_Ring, algebraMap_eq] rfl +lemma ker_mvPolynomial : (mvPolynomial R ι).ker = ⊥ := by + simp [ker_eq_ker_aeval_val, SetLike.ext_iff, aeval_X_left] + variable {P} in lemma aeval_val_eq_zero {x} (hx : x ∈ P.ker) : aeval P.val x = 0 := by rwa [← algebraMap_apply] diff --git a/Mathlib/RingTheory/Extension/Presentation/Basic.lean b/Mathlib/RingTheory/Extension/Presentation/Basic.lean index 6aba6035755878..adcb529cdeeda6 100644 --- a/Mathlib/RingTheory/Extension/Presentation/Basic.lean +++ b/Mathlib/RingTheory/Extension/Presentation/Basic.lean @@ -198,6 +198,20 @@ noncomputable def id : Presentation R R PEmpty.{w + 1} PEmpty.{t + 1} := lemma id_dimension : (Presentation.id R).dimension = 0 := ofBijectiveAlgebraMap_dimension (R := R) Function.bijective_id +variable (R ι) in +/-- The canonical `R`-presentation of the polynomial algebra `MvPolynomial ι R`, +with generators `X` indexed by `ι` and no relations. -/ +@[simps -fullyApplied relation] +noncomputable def mvPolynomial : Presentation R (MvPolynomial ι R) ι PEmpty.{t + 1} where + relation := PEmpty.elim + span_range_relation_eq_ker := by + simpa only [Generators.ker_mvPolynomial, Set.range_eq_empty] using Ideal.span_empty + __ := Generators.mvPolynomial R ι + +@[simp] +lemma dimension_mvPolynomial : (mvPolynomial R ι).dimension = Nat.card ι := by + simp [dimension] + section Localization variable (r : R) [IsLocalization.Away r S] diff --git a/Mathlib/RingTheory/Extension/Presentation/Submersive.lean b/Mathlib/RingTheory/Extension/Presentation/Submersive.lean index 715b28ed3779e1..a395f989515b38 100644 --- a/Mathlib/RingTheory/Extension/Presentation/Submersive.lean +++ b/Mathlib/RingTheory/Extension/Presentation/Submersive.lean @@ -223,6 +223,20 @@ lemma ofBijectiveAlgebraMap_jacobian (h : Function.Bijective (algebraMap R S)) : contradiction rw [jacobian_eq_jacobiMatrix_det, RingHom.map_det, this, Matrix.det_one] +variable (R ι) in +/-- The canonical pre-submersive `R`-presentation of the polynomial algebra `MvPolynomial ι R`, +with generators `X` indexed by `ι` and no relations. -/ +@[simps -fullyApplied map] +noncomputable def mvPolynomial : + PreSubmersivePresentation R (MvPolynomial ι R) ι PEmpty.{t + 1} where + map := PEmpty.elim + map_inj := PEmpty.elim.injective_of_subsingleton + __ := Presentation.mvPolynomial R ι + +@[simp] +lemma jacobian_mvPolynomial : (mvPolynomial R ι).jacobian = 1 := by + rw [jacobian_eq_jacobiMatrix_det, Matrix.det_isEmpty, map_one] + section Localization variable (r : R) [IsLocalization.Away r S] @@ -529,6 +543,11 @@ noncomputable def ofBijectiveAlgebraMap (h : Function.Bijective (algebraMap R S) noncomputable def id : SubmersivePresentation R R PEmpty.{w + 1} PEmpty.{t + 1} := ofBijectiveAlgebraMap Function.bijective_id +/-- The canonical submersive `R`-presentation of the polynomial algebra `MvPolynomial ι R`. -/ +noncomputable def mvPolynomial : SubmersivePresentation R (MvPolynomial ι R) ι PEmpty.{t + 1} where + __ := PreSubmersivePresentation.mvPolynomial R ι + jacobian_isUnit := by simp + section Composition variable {R S ι σ} variable {T ι' σ' : Type*} [CommRing T] [Algebra R T] [Algebra S T] [IsScalarTower R S T] diff --git a/Mathlib/RingTheory/Smooth/Basic.lean b/Mathlib/RingTheory/Smooth/Basic.lean index c3fbf0a1423383..984a80eda4d11e 100644 --- a/Mathlib/RingTheory/Smooth/Basic.lean +++ b/Mathlib/RingTheory/Smooth/Basic.lean @@ -107,17 +107,16 @@ lemma FormallySmooth.comp_surjective [FormallySmooth R A] (I : Ideal B) (hI : I simpa using (Function.surjInv_eq _ _).symm exact ⟨l.comp g, by rw [← AlgHom.comp_assoc, ← this, AlgHom.comp_assoc, hg, AlgHom.comp_id]⟩ -set_option backward.isDefEq.respectTransparency false in -instance mvPolynomial (σ : Type*) : FormallySmooth R (MvPolynomial σ R) := by - let P : Generators R (MvPolynomial σ R) σ := - .ofSurjective X (by simp [aeval_X_left, Function.Surjective]) +instance FormallySmooth.mvPolynomial (σ : Type*) : FormallySmooth R (MvPolynomial σ R) := by + let P := Generators.mvPolynomial R σ have : Subsingleton ↥P.toExtension.ker := - Submodule.subsingleton_iff_eq_bot.mpr <| by - simp [SetLike.ext_iff, P, Generators.ofSurjective, aeval_X_left] + Submodule.subsingleton_iff_eq_bot.mpr (Generators.ker_mvPolynomial) have : Subsingleton P.toExtension.Cotangent := Cotangent.mk_surjective.subsingleton have := P.toExtension.h1Cotangentι_injective.subsingleton exact ⟨inferInstance, P.equivH1Cotangent.symm.subsingleton⟩ +@[deprecated (since := "2026-05_20")] alias mvPolynomial := FormallySmooth.mvPolynomial + end namespace FormallySmooth diff --git a/Mathlib/RingTheory/Smooth/Quotient.lean b/Mathlib/RingTheory/Smooth/Quotient.lean index 039c9fdb9e1a5d..cdfccc38b37eda 100644 --- a/Mathlib/RingTheory/Smooth/Quotient.lean +++ b/Mathlib/RingTheory/Smooth/Quotient.lean @@ -104,14 +104,14 @@ lemma Algebra.FormallySmooth.of_surjective_of_ker_eq_map_of_flat [Module.Flat R (sq0 : (RingHom.ker (algebraMap R R')) ^ 2 = ⊥) (smoothq : Algebra.FormallySmooth R' S') : Algebra.FormallySmooth R S := by let P := (Algebra.Generators.self R S).toExtension - let : Algebra.FormallySmooth R P.Ring := Algebra.mvPolynomial S + let : Algebra.FormallySmooth R P.Ring := Algebra.FormallySmooth.mvPolynomial S let IP := (RingHom.ker (algebraMap R R')).map (algebraMap R P.Ring) let Gen : Algebra.Generators R' S' S := { val := algebraMap S S' σ' := fun s' ↦ MvPolynomial.X (Classical.choose (surjS s')) aeval_val_σ' s' := by simp [Classical.choose_spec (surjS s')] } let P' := Gen.toExtension - let : Algebra.FormallySmooth R' P'.Ring := Algebra.mvPolynomial S + let : Algebra.FormallySmooth R' P'.Ring := Algebra.FormallySmooth.mvPolynomial S let : Algebra P.Ring P'.Ring := MvPolynomial.algebraMvPolynomial let : IsScalarTower R P.Ring P'.Ring := IsScalarTower.of_algebraMap_eq (fun x ↦ (MvPolynomial.map_C _ x).symm) diff --git a/Mathlib/RingTheory/Smooth/StandardSmooth.lean b/Mathlib/RingTheory/Smooth/StandardSmooth.lean index ad083a3e38272d..a29b13bc6adad9 100644 --- a/Mathlib/RingTheory/Smooth/StandardSmooth.lean +++ b/Mathlib/RingTheory/Smooth/StandardSmooth.lean @@ -115,6 +115,20 @@ instance IsStandardSmoothOfRelativeDimension.id : IsStandardSmoothOfRelativeDimension 0 R R := IsStandardSmoothOfRelativeDimension.of_algebraMap_bijective Function.bijective_id +variable (R) in +/-- The polynomial algebra `MvPolynomial ι R` is standard smooth over `R` of relative +dimension `Nat.card ι`. -/ +lemma IsStandardSmoothOfRelativeDimension.mvPolynomial [Finite ι] : + IsStandardSmoothOfRelativeDimension (Nat.card ι) R (MvPolynomial ι R) := + (SubmersivePresentation.mvPolynomial.{0} R ι).isStandardSmoothOfRelativeDimension + (Presentation.dimension_mvPolynomial) + +/-- The polynomial algebra `MvPolynomial (Fin n) R` is standard smooth over `R` of relative +dimension `n`. -/ +instance IsStandardSmoothOfRelativeDimension.mvPolynomial_fin {n : ℕ} : + IsStandardSmoothOfRelativeDimension n R (MvPolynomial (Fin n) R) := by + simpa using IsStandardSmoothOfRelativeDimension.mvPolynomial R (Fin n) + instance (priority := 100) IsStandardSmooth.finitePresentation [IsStandardSmooth R S] : FinitePresentation R S := by obtain ⟨_, _, _, _, ⟨P⟩⟩ := ‹IsStandardSmooth R S›