From c64e5003d4dbaa2ac634919931892d4e01cafb78 Mon Sep 17 00:00:00 2001 From: Justus Springer Date: Fri, 22 May 2026 15:30:09 +0100 Subject: [PATCH 1/3] fix namespace issue --- Mathlib/RingTheory/Smooth/Basic.lean | 4 +++- Mathlib/RingTheory/Smooth/Quotient.lean | 4 ++-- 2 files changed, 5 insertions(+), 3 deletions(-) diff --git a/Mathlib/RingTheory/Smooth/Basic.lean b/Mathlib/RingTheory/Smooth/Basic.lean index c3fbf0a1423383..14ba94d44efd2e 100644 --- a/Mathlib/RingTheory/Smooth/Basic.lean +++ b/Mathlib/RingTheory/Smooth/Basic.lean @@ -108,7 +108,7 @@ lemma FormallySmooth.comp_surjective [FormallySmooth R A] (I : Ideal B) (hI : I 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 +instance FormallySmooth.mvPolynomial (σ : Type*) : FormallySmooth R (MvPolynomial σ R) := by let P : Generators R (MvPolynomial σ R) σ := .ofSurjective X (by simp [aeval_X_left, Function.Surjective]) have : Subsingleton ↥P.toExtension.ker := @@ -118,6 +118,8 @@ instance mvPolynomial (σ : Type*) : FormallySmooth R (MvPolynomial σ R) := by have := P.toExtension.h1Cotangentι_injective.subsingleton exact ⟨inferInstance, P.equivH1Cotangent.symm.subsingleton⟩ +@[deprecated (since := "2026-05-22")] 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) From a6adcfed6a62fdd9405dc8eaa94f22c6300fef85 Mon Sep 17 00:00:00 2001 From: Justus Springer <50165510+justus-springer@users.noreply.github.com> Date: Mon, 25 May 2026 18:25:43 +0100 Subject: [PATCH 2/3] Apply suggestion from @ocfnash Co-authored-by: Oliver Nash <7734364+ocfnash@users.noreply.github.com> --- Mathlib/RingTheory/Smooth/Basic.lean | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/Mathlib/RingTheory/Smooth/Basic.lean b/Mathlib/RingTheory/Smooth/Basic.lean index 14ba94d44efd2e..8d478555a02c8b 100644 --- a/Mathlib/RingTheory/Smooth/Basic.lean +++ b/Mathlib/RingTheory/Smooth/Basic.lean @@ -108,7 +108,7 @@ lemma FormallySmooth.comp_surjective [FormallySmooth R A] (I : Ideal B) (hI : I 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 FormallySmooth.mvPolynomial (σ : Type*) : FormallySmooth R (MvPolynomial σ R) := by +instance instFormallySmoothMvPolynomial (σ : Type*) : FormallySmooth R (MvPolynomial σ R) := by let P : Generators R (MvPolynomial σ R) σ := .ofSurjective X (by simp [aeval_X_left, Function.Surjective]) have : Subsingleton ↥P.toExtension.ker := From 5da6d340caa57165346a2ba4ec95a56f4a7f732c Mon Sep 17 00:00:00 2001 From: Justus Springer Date: Mon, 25 May 2026 18:26:49 +0100 Subject: [PATCH 3/3] update deprecation --- Mathlib/RingTheory/Smooth/Basic.lean | 2 +- Mathlib/RingTheory/Smooth/Quotient.lean | 4 ++-- 2 files changed, 3 insertions(+), 3 deletions(-) diff --git a/Mathlib/RingTheory/Smooth/Basic.lean b/Mathlib/RingTheory/Smooth/Basic.lean index 8d478555a02c8b..f0fd4687f0867c 100644 --- a/Mathlib/RingTheory/Smooth/Basic.lean +++ b/Mathlib/RingTheory/Smooth/Basic.lean @@ -118,7 +118,7 @@ instance instFormallySmoothMvPolynomial (σ : Type*) : FormallySmooth R (MvPolyn have := P.toExtension.h1Cotangentι_injective.subsingleton exact ⟨inferInstance, P.equivH1Cotangent.symm.subsingleton⟩ -@[deprecated (since := "2026-05-22")] alias mvPolynomial := FormallySmooth.mvPolynomial +@[deprecated (since := "2026-05-22")] alias mvPolynomial := instFormallySmoothMvPolynomial end diff --git a/Mathlib/RingTheory/Smooth/Quotient.lean b/Mathlib/RingTheory/Smooth/Quotient.lean index cdfccc38b37eda..1ec859b7b3ccc9 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.FormallySmooth.mvPolynomial S + let : Algebra.FormallySmooth R P.Ring := instFormallySmoothMvPolynomial 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.FormallySmooth.mvPolynomial S + let : Algebra.FormallySmooth R' P'.Ring := instFormallySmoothMvPolynomial 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)