Skip to content

Commit 82b142b

Browse files
chrisflavchrisflav
committed
fix
1 parent e7aca66 commit 82b142b

File tree

5 files changed

+270
-3
lines changed

5 files changed

+270
-3
lines changed

‎Mathlib.lean‎

Lines changed: 1 addition & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -6136,6 +6136,7 @@ public import Mathlib.RingTheory.Smooth.Basic
61366136
public import Mathlib.RingTheory.Smooth.Kaehler
61376137
public import Mathlib.RingTheory.Smooth.Local
61386138
public import Mathlib.RingTheory.Smooth.Locus
6139+
public import Mathlib.RingTheory.Smooth.NoetherianDescent
61396140
public import Mathlib.RingTheory.Smooth.Pi
61406141
public import Mathlib.RingTheory.Smooth.StandardSmooth
61416142
public import Mathlib.RingTheory.Smooth.StandardSmoothCotangent

‎Mathlib/Algebra/MvPolynomial/Eval.lean‎

Lines changed: 20 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -372,6 +372,14 @@ theorem map_eval₂ (f : R →+* S₁) (g : S₂ → MvPolynomial S₃ R) (p : M
372372
rw [eval₂_mul, (map f).map_mul, hp, (map f).map_mul, map_X, eval₂_mul, eval₂_X, eval₂_X,
373373
comp_apply]
374374

375+
lemma eval₂_map_comp_C {ι : Type*} (f : R →+* S₁) (h : ι → MvPolynomial σ S₁)
376+
(p : MvPolynomial ι R) : eval₂ ((map f).comp C) h p = eval₂ C h (map f p) := by
377+
induction p using MvPolynomial.induction_on <;> simp_all
378+
379+
lemma map_eval {S₂ : Type*} [CommSemiring S₂] (q : S₁ →+* S₂) (g : σ → S₁) (p : MvPolynomial σ S₁) :
380+
q (eval g p) = eval (q ∘ g) (map q p) := by
381+
rw [← eval₂_eq_eval_map, ← eval₂_id, eval₂_comp_right, map_id]
382+
375383
theorem coeff_map (p : MvPolynomial σ R) : ∀ m : σ →₀ ℕ, coeff m (map f p) = f (coeff m p) := by
376384
classical
377385
apply MvPolynomial.induction_on p <;> clear p
@@ -515,6 +523,18 @@ lemma mem_range_map_iff_coeffs_subset {f : R →+* S₁} {x : MvPolynomial σ S
515523
obtain ⟨u, hu⟩ := hp hx.2
516524
exact ⟨q + u, by simp [hq, hu]⟩
517525

526+
/-- If the coefficients of `p` are in the range of `f`, this is a preimage of
527+
`p` under `MvPolynomial.map f`. -/
528+
noncomputable def preimageOfCoeffsSubsetRange {f : R →+* S₁} {p : MvPolynomial σ S₁}
529+
(hp : (p.coeffs : Set S₁) ⊆ Set.range f) : MvPolynomial σ R :=
530+
(MvPolynomial.mem_range_map_iff_coeffs_subset.mpr hp).choose
531+
532+
@[simp]
533+
lemma map_preimageOfCoeffsSubsetRange {f : R →+* S₁} {p : MvPolynomial σ S₁}
534+
(hp : (p.coeffs : Set S₁) ⊆ Set.range f) :
535+
(p.preimageOfCoeffsSubsetRange hp).map f = p :=
536+
(MvPolynomial.mem_range_map_iff_coeffs_subset.mpr hp).choose_spec
537+
518538
/-- If `f : S₁ →ₐ[R] S₂` is a morphism of `R`-algebras, then so is `MvPolynomial.map f`. -/
519539
@[simps!]
520540
def mapAlgHom [CommSemiring S₂] [Algebra R S₁] [Algebra R S₂] (f : S₁ →ₐ[R] S₂) :

‎Mathlib/RingTheory/Ideal/Cotangent.lean‎

Lines changed: 4 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -172,6 +172,10 @@ def _root_.AlgHom.kerSquareLift (f : A →ₐ[R] B) : A ⧸ RingHom.ker f.toRing
172172
Ideal.Quotient.lift_mk]
173173
exact f.map_algebraMap r
174174

175+
@[simp]
176+
lemma _root_.AlgHom.kerSquareLift_mk (f : A →ₐ[R] B) (x : A) : f.kerSquareLift x = f x :=
177+
rfl
178+
175179
theorem _root_.AlgHom.ker_kerSquareLift (f : A →ₐ[R] B) :
176180
RingHom.ker f.kerSquareLift.toRingHom = (RingHom.ker f.toRingHom).cotangentIdeal := by
177181
apply le_antisymm

‎Mathlib/RingTheory/MvPolynomial/Homogeneous.lean‎

Lines changed: 56 additions & 3 deletions
Original file line numberDiff line numberDiff line change
@@ -5,12 +5,11 @@ Authors: Johan Commelin, Eric Wieser
55
-/
66
module
77

8-
public import Mathlib.Algebra.DirectSum.Internal
9-
public import Mathlib.Algebra.GradedMonoid
108
public import Mathlib.Algebra.MvPolynomial.CommRing
119
public import Mathlib.Algebra.MvPolynomial.Equiv
12-
public import Mathlib.Algebra.MvPolynomial.Variables
1310
public import Mathlib.Algebra.Polynomial.Roots
11+
public import Mathlib.RingTheory.Ideal.BigOperators
12+
public import Mathlib.RingTheory.Ideal.Operations
1413
public import Mathlib.RingTheory.MvPolynomial.WeightedHomogeneous
1514
public import Mathlib.SetTheory.Cardinal.Basic
1615

@@ -225,6 +224,10 @@ lemma eval₂ (hφ : φ.IsHomogeneous m) (f : R →+* MvPolynomial τ S) (g : σ
225224
lemma map (hφ : φ.IsHomogeneous n) (f : R →+* S) : (map f φ).IsHomogeneous n := by
226225
simpa only [one_mul] using hφ.eval₂ _ _ (fun r ↦ isHomogeneous_C _ (f r)) (isHomogeneous_X _)
227226

227+
lemma of_map {f : R →+* S} (hf : Function.Injective f)
228+
(h : (MvPolynomial.map f φ).IsHomogeneous n) : φ.IsHomogeneous n :=
229+
fun u hu ↦ h (coeff_map f φ u ▸ map_zero f ▸ hf.ne hu)
230+
228231
lemma aeval [Algebra R S] (hφ : φ.IsHomogeneous m)
229232
(g : σ → MvPolynomial τ S) (hg : ∀ i, (g i).IsHomogeneous n) :
230233
(aeval g φ).IsHomogeneous (n * m) :=
@@ -545,3 +548,53 @@ theorem decomposition.decompose'_eq :
545548
end GradedAlgebra
546549

547550
end MvPolynomial
551+
552+
/-- Try to use the universal property of the span (e.g., `Submodule.span_induction`) instead of
553+
this. -/
554+
lemma Ideal.exists_isHomogeneous_of_mem_span {ι R : Type*} [CommSemiring R]
555+
(x : ι → R) (y : R) (hy : y ∈ Ideal.span (.range x)) :
556+
∃ (p : MvPolynomial ι R), p.IsHomogeneous 1 ∧ p.eval x = y := by
557+
induction hy using Submodule.span_induction with
558+
| mem s hs =>
559+
obtain ⟨i, rfl⟩ := hs
560+
exact ⟨MvPolynomial.X i, MvPolynomial.isHomogeneous_X _ _, by simp⟩
561+
| zero => exact ⟨0, MvPolynomial.isHomogeneous_zero _ _ _, by simp⟩
562+
| add x y _ _ hx hy =>
563+
obtain ⟨px, hpxhom, rfl⟩ := hx
564+
obtain ⟨py, hpyhom, rfl⟩ := hy
565+
exact ⟨px + py, MvPolynomial.IsHomogeneous.add hpxhom hpyhom, by simp⟩
566+
| smul a x _ hx =>
567+
obtain ⟨px, hpxhom, rfl⟩ := hx
568+
exact ⟨MvPolynomial.C a * px, MvPolynomial.IsHomogeneous.C_mul hpxhom a, by simp⟩
569+
570+
/-- Try to use the universal property of the span (e.g., `Submodule.span_induction`) instead of
571+
this. -/
572+
lemma Ideal.mem_span_pow_iff {ι R : Type*} [CommSemiring R] {n : ℕ} (x : ι → R) (y : R) :
573+
y ∈ (Ideal.span <| Set.range x) ^ n ↔
574+
∃ (p : MvPolynomial ι R), p.IsHomogeneous n ∧ p.eval x = y := by
575+
refine ⟨?_, ?_⟩
576+
· induction n using Nat.case_strong_induction_on generalizing y with
577+
| hz => exact fun _ ↦ ⟨MvPolynomial.C y, MvPolynomial.isHomogeneous_C _ _, by simp⟩
578+
| hi n ih =>
579+
refine fun h ↦ Submodule.smul_induction_on h (fun r hr t ht ↦ ?_) ?_
580+
· obtain ⟨pr, hprhom, rfl⟩ := ih n (by omega) r hr
581+
obtain ⟨pt, hpthom, rfl⟩ := Ideal.exists_isHomogeneous_of_mem_span x t ht
582+
exact ⟨pr * pt, MvPolynomial.IsHomogeneous.mul hprhom hpthom, by simp⟩
583+
· rintro x y ⟨px, hpxhom, rfl⟩ ⟨py, hpyhom, rfl⟩
584+
exact ⟨px + py, MvPolynomial.IsHomogeneous.add hpxhom hpyhom, by simp⟩
585+
· rintro ⟨p, hp, rfl⟩
586+
rw [← p.sum_single, map_finsuppSum, Finsupp.sum]
587+
refine Ideal.sum_mem _ fun c hc ↦ ?_
588+
simp_rw [MvPolynomial.single_eq_monomial, MvPolynomial.eval_monomial]
589+
apply Ideal.mul_mem_left
590+
have : Finsupp.degree = Finsupp.weight 1 := Finsupp.degree_eq_weight_one (σ := ι) (R := ℕ)
591+
rw [← @hp c (by simpa using hc), ← this, Finsupp.degree, ← Finset.prod_pow_eq_pow_sum,
592+
Finsupp.prod]
593+
exact Ideal.prod_mem_prod fun _ _ ↦ Ideal.pow_mem_pow (Ideal.subset_span (by simp)) _
594+
595+
/-- Try to use the universal property of the span (e.g., `Submodule.span_induction`) instead of
596+
this. -/
597+
lemma Ideal.mem_span_iff {ι R : Type*} [CommSemiring R] (x : ι → R) (y : R) :
598+
y ∈ Ideal.span (.range x) ↔
599+
∃ (p : MvPolynomial ι R), p.IsHomogeneous 1 ∧ p.eval x = y := by
600+
rw [← pow_one (span <| .range x), mem_span_pow_iff]

‎Mathlib/RingTheory/Smooth/NoetherianDescent.lean‎

Lines changed: 189 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,189 @@
1+
/-
2+
Copyright (c) 2025 Judith Ludwig, Christian Merten. All rights reserved.
3+
Released under Apache 2.0 license as described in the file LICENSE.
4+
Authors: Judith Ludwig, Christian Merten
5+
-/
6+
module
7+
8+
public import Mathlib.RingTheory.Extension.Presentation.Core
9+
public import Mathlib.RingTheory.MvPolynomial.Homogeneous
10+
public import Mathlib.RingTheory.Smooth.Basic
11+
public import Mathlib.Tactic.DepRewrite
12+
13+
/-!
14+
# Smooth algebras have Noetherian models
15+
16+
In this file, we show if `S` is a smooth `R`-algebra, there exists a `ℤ`-subalgebra of finite type
17+
`R₀` and a smooth `R₀`-algebra `S₀` such that `S ≃ₐ R ⊗[R₀] S₀`.
18+
-/
19+
20+
universe u
21+
22+
open TensorProduct MvPolynomial
23+
24+
namespace Algebra.Smooth
25+
26+
variable {R : Type u} {S : Type*} [CommRing R] [CommRing S] [Algebra R S]
27+
28+
variable (R S) in
29+
/-- (Implementation detail): If `S` is an `R`-algebra with presentation `P`
30+
and section `σ` of the projection `R[Xᵢ] ⧸ I^2 → S`, then a
31+
`DescentAux` structure contains the data necessary to reconstruct `σ`. -/
32+
structure DescentAux where
33+
vars : Type
34+
rels : Type
35+
P : Presentation R S vars rels
36+
σ : S →ₐ[R] MvPolynomial vars R ⧸ P.ker ^ 2
37+
h : vars → MvPolynomial vars R
38+
p : rels → MvPolynomial rels (MvPolynomial vars R)
39+
hphom : ∀ (j : rels), (p j).IsHomogeneous 2
40+
hp : ∀ (j : rels), (eval P.relation) (p j) = (aeval h) (P.relation j)
41+
q : vars → MvPolynomial rels P.Ring
42+
hqhom : ∀ (i : vars), (q i).IsHomogeneous 1
43+
hq : ∀ (i : vars), (eval P.relation) (q i) = h i - X i
44+
45+
namespace DescentAux
46+
47+
variable (A : DescentAux R S)
48+
49+
/-- (Implementation detail): The finite type `ℤ`-algebra. -/
50+
def R₀ (A : DescentAux R S) : Type _ :=
51+
Algebra.adjoin A.P.Core
52+
((⋃ i, (A.h i).coeffs) ∪
53+
(⋃ i, ⋃ x ∈ (A.q i).coeffs, x.coeffs) ∪
54+
(⋃ i, ⋃ x ∈ (A.p i).coeffs, x.coeffs) : Set R)
55+
56+
instance : CommRing A.R₀ := inferInstanceAs <| CommRing (Algebra.adjoin _ _)
57+
instance algebra : Algebra A.R₀ R := inferInstanceAs <| Algebra (Algebra.adjoin _ _) R
58+
instance : Algebra A.R₀ S := inferInstanceAs <| Algebra (Algebra.adjoin _ _) S
59+
instance : IsScalarTower A.R₀ R S :=
60+
inferInstanceAs <| IsScalarTower (Algebra.adjoin _ _) _ _
61+
instance : FaithfulSMul A.R₀ R := inferInstanceAs <| FaithfulSMul (Algebra.adjoin _ _) _
62+
63+
instance [Finite A.vars] [Finite A.rels] : Algebra.FiniteType ℤ A.R₀ := by
64+
dsimp only [R₀]
65+
refine Algebra.FiniteType.trans (S := A.P.Core) inferInstance <| .adjoin_of_finite ?_
66+
refine Set.Finite.union (Set.Finite.union ?_ ?_) ?_
67+
· refine Set.finite_iUnion fun i ↦ Finset.finite_toSet _
68+
· refine Set.finite_iUnion fun i ↦ ?_
69+
exact Set.Finite.biUnion (Finset.finite_toSet _) (fun i hi ↦ Finset.finite_toSet _)
70+
· refine Set.finite_iUnion fun i ↦ ?_
71+
exact Set.Finite.biUnion (Finset.finite_toSet _) (fun i hi ↦ Finset.finite_toSet _)
72+
73+
instance hasCoeffs : A.P.HasCoeffs A.R₀ := by dsimp [R₀]; infer_instance
74+
75+
set_option quotPrecheck false in
76+
local notation "f₀" =>
77+
Ideal.Quotient.mkₐ A.R₀ (Ideal.span <| .range <| A.P.relationOfHasCoeffs A.R₀)
78+
79+
lemma subset_range_algebraMap :
80+
((⋃ i, (A.h i).coeffs) ∪
81+
(⋃ i, ⋃ x ∈ (A.q i).coeffs, x.coeffs) ∪
82+
(⋃ i, ⋃ x ∈ (A.p i).coeffs, x.coeffs) : Set R) ⊆ Set.range ⇑(algebraMap A.R₀ R) := by
83+
simp only [R₀, Subalgebra.setRange_algebraMap, Algebra.subset_adjoin]
84+
85+
lemma coeffs_h_subset (i) : ((A.h i).coeffs : Set R) ⊆ Set.range ⇑(algebraMap A.R₀ R) := by
86+
trans ⋃ i, ↑(A.h i).coeffs
87+
· exact Set.subset_iUnion_of_subset i subset_rfl
88+
· exact subset_trans (subset_trans Set.subset_union_left Set.subset_union_left)
89+
A.subset_range_algebraMap
90+
91+
lemma coeffs_p_subset (i) :
92+
((A.p i).coeffs : Set _) ⊆ .range (MvPolynomial.map (σ := A.vars) (algebraMap A.R₀ R)) := by
93+
intro p hp
94+
rw [MvPolynomial.mem_range_map_iff_coeffs_subset]
95+
refine subset_trans ?_ A.subset_range_algebraMap
96+
refine subset_trans ?_ Set.subset_union_right
97+
exact Set.subset_iUnion_of_subset i (Set.subset_iUnion₂_of_subset p hp subset_rfl)
98+
99+
lemma coeffs_q_subset (i) :
100+
((A.q i).coeffs : Set _) ⊆ .range (MvPolynomial.map (σ := A.vars) (algebraMap A.R₀ R)) := by
101+
intro q hq
102+
rw [MvPolynomial.mem_range_map_iff_coeffs_subset]
103+
refine subset_trans ?_ A.subset_range_algebraMap
104+
refine subset_trans ?_ Set.subset_union_left
105+
refine subset_trans ?_ Set.subset_union_right
106+
exact Set.subset_iUnion_of_subset i (Set.subset_iUnion₂_of_subset q hq subset_rfl)
107+
108+
noncomputable def σ₀ :
109+
A.P.ModelOfHasCoeffs A.R₀ →ₐ[A.R₀] MvPolynomial A.vars A.R₀ ⧸ (RingHom.ker f₀ ^ 2) :=
110+
Ideal.Quotient.liftₐ _ ((Ideal.Quotient.mkₐ _ _).comp <| aeval fun i ↦
111+
((A.h i).preimageOfCoeffsSubsetRange (A.coeffs_h_subset i))) <| by
112+
simp_rw [← RingHom.mem_ker, ← SetLike.le_def, Ideal.span_le, Set.range_subset_iff]
113+
intro i
114+
simp only [← AlgHom.comap_ker, Ideal.coe_comap,
115+
Set.mem_preimage, SetLike.mem_coe]
116+
rw [← RingHom.ker_coe_toRingHom, Ideal.Quotient.mkₐ_ker,
117+
← RingHom.ker_coe_toRingHom, Ideal.Quotient.mkₐ_ker]
118+
have hinj : Function.Injective (MvPolynomial.map (σ := A.vars) (algebraMap A.R₀ R)) :=
119+
map_injective _ (FaithfulSMul.algebraMap_injective A.R₀ R)
120+
rw [Ideal.mem_span_pow_iff]
121+
refine ⟨(A.p i).preimageOfCoeffsSubsetRange (A.coeffs_p_subset i), .of_map hinj ?_, hinj ?_⟩
122+
· rw [map_preimageOfCoeffsSubsetRange]
123+
exact A.hphom i
124+
· simp_rw [map_eval, Function.comp_def, Presentation.map_relationOfHasCoeffs,
125+
map_preimageOfCoeffsSubsetRange, A.hp, MvPolynomial.map_aeval]
126+
simp [MvPolynomial.eval₂_map_comp_C, Presentation.map_relationOfHasCoeffs, aeval_def]
127+
128+
lemma kerSquareLift_comp_σ₀ :
129+
(AlgHom.kerSquareLift f₀).comp A.σ₀ = .id A.R₀ (Presentation.ModelOfHasCoeffs A.R₀) := by
130+
have hf₀ : Function.Surjective f₀ := Ideal.Quotient.mk_surjective
131+
rw [← AlgHom.cancel_right hf₀]
132+
refine MvPolynomial.algHom_ext fun i ↦ ?_
133+
suffices h : ∃ p, p.IsHomogeneous 1 ∧ (eval (A.P.relationOfHasCoeffs A.R₀)) p =
134+
preimageOfCoeffsSubsetRange (A.coeffs_h_subset i) - X i by
135+
-- Reducible def-eq issues caused by `RingHom.ker f.toRingHom` dicsrepancies
136+
apply (Ideal.Quotient.mk_eq_mk_iff_sub_mem _ _).mpr
137+
simpa [Ideal.mem_span_iff]
138+
have hinj : Function.Injective (MvPolynomial.map (σ := A.vars) (algebraMap A.R₀ R)) :=
139+
map_injective _ (FaithfulSMul.algebraMap_injective A.R₀ R)
140+
refine ⟨(A.q i).preimageOfCoeffsSubsetRange (A.coeffs_q_subset i), .of_map hinj ?_, hinj ?_⟩
141+
· rw [map_preimageOfCoeffsSubsetRange]
142+
exact A.hqhom i
143+
· simp [MvPolynomial.map_eval, map_preimageOfCoeffsSubsetRange, Function.comp_def,
144+
Presentation.map_relationOfHasCoeffs, hq]
145+
146+
end DescentAux
147+
148+
/-- If `S` is a smooth `R`-algebra, there exists a `ℤ`-subalgebra of finite type
149+
`R₀` and a smooth `R₀`-algebra `S₀` such that `S ≃ₐ R ⊗[R₀] S₀`. -/
150+
@[stacks 00TP]
151+
public theorem exists_finiteType [Smooth R S] :
152+
∃ (R₀ : Type u) (S₀ : Type u) (_ : CommRing R₀) (_ : CommRing S₀)
153+
(_ : Algebra R₀ R) (_ : Algebra R₀ S₀),
154+
FiniteType ℤ R₀ ∧ Smooth R₀ S₀ ∧ Nonempty (S ≃ₐ[R] R ⊗[R₀] S₀) := by
155+
let P := Presentation.ofFinitePresentation R S
156+
let f : P.Ring →ₐ[R] S := IsScalarTower.toAlgHom _ _ _
157+
have hkerf : RingHom.ker f = Ideal.span (.range P.relation) :=
158+
P.span_range_relation_eq_ker.symm
159+
obtain ⟨(σ : S →ₐ[R] MvPolynomial _ R ⧸ RingHom.ker f ^ 2), hsig⟩ :=
160+
(FormallySmooth.iff_split_surjection f P.algebraMap_surjective).mp inferInstance
161+
have (i : _) := Ideal.Quotient.mk_surjective (σ <| P.val i)
162+
choose h hh using this
163+
have hdiag : (Ideal.Quotient.mkₐ _ _).comp (aeval h) = σ.comp (aeval P.val) :=
164+
algHom_ext (by simp [hh])
165+
have (j : _) : Ideal.Quotient.mk (RingHom.ker f ^ 2) (aeval h (P.relation j)) = 0 := by
166+
suffices ho : σ (aeval P.val (P.relation j)) = 0 by
167+
convert ho
168+
exact congr($hdiag _)
169+
simp
170+
simp_rw [Ideal.Quotient.eq_zero_iff_mem, hkerf, Ideal.mem_span_pow_iff] at this
171+
choose p homog hp using this
172+
have hsig (i : _) : f (h i) = P.val i := by
173+
rw [← AlgHom.kerSquareLift_mk]
174+
-- Reducible def-eq issues caused by `RingHom.ker f.toRingHom` dicsrepancies
175+
exact hh i ▸ congr($hsig (P.val i))
176+
have (i : Fin (Presentation.ofFinitePresentationVars R S)) :
177+
h i - X i ∈ Ideal.span (.range P.relation) := by
178+
simpa [P.span_range_relation_eq_ker, sub_eq_zero, f] using hsig i
179+
simp_rw [Ideal.mem_span_iff] at this
180+
choose q hqhom hq using this
181+
let A : DescentAux R S :=
182+
{ vars := _, rels := _, P := P, σ := σ, p := p, h := h, hphom := homog, hp := hp,
183+
q := q, hqhom := hqhom, hq := hq }
184+
have : P.HasCoeffs A.R₀ := A.hasCoeffs
185+
exact ⟨A.R₀, P.ModelOfHasCoeffs A.R₀, inferInstance, inferInstance, inferInstance, inferInstance,
186+
inferInstance, ⟨.of_split _ A.σ₀ A.kerSquareLift_comp_σ₀, inferInstance⟩,
187+
⟨(P.tensorModelOfHasCoeffsEquiv A.R₀).symm⟩⟩
188+
189+
end Algebra.Smooth

0 commit comments

Comments
 (0)