Skip to content

Commit 6eec427

Browse files
chrisflavchrisflav
committed
feat(RingTheory/StandardSmooth): meta properties of standard smooth ring homomorphisms (#16868)
In particular we show that being standard smooth is stable under composition and base change. This contribution was created as part of the AIM workshop "Formalizing algebraic geometry" in June 2024.
1 parent 36c03bd commit 6eec427

5 files changed

Lines changed: 217 additions & 25 deletions

File tree

‎Mathlib.lean‎

Lines changed: 1 addition & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -4110,6 +4110,7 @@ import Mathlib.RingTheory.RingHom.FinitePresentation
41104110
import Mathlib.RingTheory.RingHom.FiniteType
41114111
import Mathlib.RingTheory.RingHom.Integral
41124112
import Mathlib.RingTheory.RingHom.Locally
4113+
import Mathlib.RingTheory.RingHom.StandardSmooth
41134114
import Mathlib.RingTheory.RingHom.Surjective
41144115
import Mathlib.RingTheory.RingHomProperties
41154116
import Mathlib.RingTheory.RingInvo

‎Mathlib/RingTheory/LocalProperties/Basic.lean‎

Lines changed: 38 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -4,6 +4,7 @@ Released under Apache 2.0 license as described in the file LICENSE.
44
Authors: Andrew Yang
55
-/
66
import Mathlib.RingTheory.Localization.AtPrime
7+
import Mathlib.RingTheory.Localization.BaseChange
78
import Mathlib.RingTheory.Localization.Submodule
89
import Mathlib.RingTheory.RingHomProperties
910

@@ -261,6 +262,43 @@ lemma RingHom.OfLocalizationSpanTarget.ofIsLocalization
261262
AlgEquiv.toRingEquiv_toRingHom, Localization.coe_algEquiv_symm, IsLocalization.map_comp,
262263
RingHom.comp_id]
263264

265+
section
266+
267+
variable (hP : RingHom.StableUnderBaseChange @P)
268+
variable {R S Rᵣ Sᵣ : Type u} [CommRing R] [CommRing S] [CommRing Rᵣ] [CommRing Sᵣ] [Algebra R Rᵣ]
269+
[Algebra S Sᵣ]
270+
271+
include hP
272+
273+
/-- Let `S` be an `R`-algebra and `Sᵣ` and `Rᵣ` be the respective localizations at a submonoid
274+
`M` of `R`. If `P` is stable under base change and `P` holds for `algebraMap R S`, then
275+
`P` holds for `algebraMap Rᵣ Sᵣ`. -/
276+
lemma RingHom.StableUnderBaseChange.of_isLocalization [Algebra R S] [Algebra R Sᵣ] [Algebra Rᵣ Sᵣ]
277+
[IsScalarTower R S Sᵣ] [IsScalarTower R Rᵣ Sᵣ]
278+
(M : Submonoid R) [IsLocalization M Rᵣ] [IsLocalization (Algebra.algebraMapSubmonoid S M) Sᵣ]
279+
(h : P (algebraMap R S)) : P (algebraMap Rᵣ Sᵣ) :=
280+
letI : Algebra.IsPushout R S Rᵣ Sᵣ := Algebra.isPushout_of_isLocalization M Rᵣ S Sᵣ
281+
hP R S Rᵣ Sᵣ h
282+
283+
/-- If `P` is stable under base change and holds for `f`, then `P` holds for `f` localized
284+
at any submonoid `M` of `R`. -/
285+
lemma RingHom.StableUnderBaseChange.isLocalization_map (M : Submonoid R) [IsLocalization M Rᵣ]
286+
(f : R →+* S) [IsLocalization (M.map f) Sᵣ] (hf : P f) :
287+
P (IsLocalization.map Sᵣ f M.le_comap_map : Rᵣ →+* Sᵣ) := by
288+
algebraize [f, IsLocalization.map (S := Rᵣ) Sᵣ f M.le_comap_map,
289+
(IsLocalization.map (S := Rᵣ) Sᵣ f M.le_comap_map).comp (algebraMap R Rᵣ)]
290+
haveI : IsScalarTower R S Sᵣ := IsScalarTower.of_algebraMap_eq'
291+
(IsLocalization.map_comp M.le_comap_map)
292+
haveI : IsLocalization (Algebra.algebraMapSubmonoid S M) Sᵣ :=
293+
inferInstanceAs <| IsLocalization (M.map f) Sᵣ
294+
apply hP.of_isLocalization M hf
295+
296+
lemma RingHom.StableUnderBaseChange.localizationPreserves : LocalizationPreserves P := by
297+
introv R hf
298+
exact hP.isLocalization_map _ _ hf
299+
300+
end
301+
264302
end RingHom
265303

266304
end Properties

‎Mathlib/RingTheory/Localization/BaseChange.lean‎

Lines changed: 9 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -47,3 +47,12 @@ theorem isLocalizedModule_iff_isBaseChange : IsLocalizedModule S f ↔ IsBaseCha
4747
rw [LinearMap.coe_comp, LinearEquiv.coe_coe, Function.comp_apply,
4848
LinearEquiv.restrictScalars_apply, LinearEquiv.trans_apply, IsBaseChange.equiv_symm_apply,
4949
IsBaseChange.equiv_tmul, one_smul]
50+
51+
variable (T B : Type*) [CommSemiring T] [CommSemiring B]
52+
[Algebra R T] [Algebra T B] [Algebra R B] [Algebra A B] [IsScalarTower R T B]
53+
[IsScalarTower R A B]
54+
55+
lemma Algebra.isPushout_of_isLocalization [IsLocalization (Algebra.algebraMapSubmonoid T S) B] :
56+
Algebra.IsPushout R T A B := by
57+
rw [Algebra.IsPushout.comm, Algebra.isPushout_iff]
58+
apply IsLocalizedModule.isBaseChange S

‎Mathlib/RingTheory/RingHom/StandardSmooth.lean‎

Lines changed: 168 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,168 @@
1+
/-
2+
Copyright (c) 2024 Christian Merten. All rights reserved.
3+
Released under Apache 2.0 license as described in the file LICENSE.
4+
Authors: Christian Merten
5+
-/
6+
import Mathlib.RingTheory.LocalProperties.Basic
7+
import Mathlib.RingTheory.Smooth.StandardSmooth
8+
import Mathlib.Tactic.Algebraize
9+
10+
/-!
11+
# Standard smooth ring homomorphisms
12+
13+
In this file we define standard smooth ring homomorphisms and show their
14+
meta properties.
15+
16+
## Notes
17+
18+
This contribution was created as part of the AIM workshop "Formalizing algebraic geometry"
19+
in June 2024.
20+
21+
-/
22+
23+
universe t t' w w' u v
24+
25+
variable (n m : ℕ)
26+
27+
open TensorProduct
28+
29+
namespace RingHom
30+
31+
variable {R : Type u} {S : Type v} [CommRing R] [CommRing S]
32+
33+
/-- A ring homomorphism `R →+* S` is standard smooth if `S` is standard smooth as `R`-algebra. -/
34+
def IsStandardSmooth (f : R →+* S) : Prop :=
35+
@Algebra.IsStandardSmooth.{t, w} _ _ _ _ f.toAlgebra
36+
37+
/-- A ring homomorphism `R →+* S` is standard smooth of relative dimension `n` if
38+
`S` is standard smooth of relative dimension `n` as `R`-algebra. -/
39+
def IsStandardSmoothOfRelativeDimension (f : R →+* S) : Prop :=
40+
@Algebra.IsStandardSmoothOfRelativeDimension.{t, w} n _ _ _ _ f.toAlgebra
41+
42+
lemma IsStandardSmoothOfRelativeDimension.isStandardSmooth (f : R →+* S)
43+
(hf : IsStandardSmoothOfRelativeDimension.{t, w} n f) :
44+
IsStandardSmooth.{t, w} f := by
45+
algebraize [f]
46+
letI : Algebra.IsStandardSmoothOfRelativeDimension.{t, w} n R S := hf
47+
exact Algebra.IsStandardSmoothOfRelativeDimension.isStandardSmooth n
48+
49+
variable {n m}
50+
51+
variable (R) in
52+
lemma IsStandardSmoothOfRelativeDimension.id :
53+
IsStandardSmoothOfRelativeDimension.{t, w} 0 (RingHom.id R) :=
54+
Algebra.IsStandardSmoothOfRelativeDimension.id R
55+
56+
lemma IsStandardSmoothOfRelativeDimension.equiv (e : R ≃+* S) :
57+
IsStandardSmoothOfRelativeDimension.{t, w} 0 (e : R →+* S) := by
58+
algebraize [e.toRingHom]
59+
exact Algebra.IsStandardSmoothOfRelativeDimension.of_algebraMap_bijective e.bijective
60+
61+
variable {T : Type*} [CommRing T]
62+
63+
lemma IsStandardSmooth.comp {g : S →+* T} {f : R →+* S}
64+
(hg : IsStandardSmooth.{t', w'} g) (hf : IsStandardSmooth.{t, w} f) :
65+
IsStandardSmooth.{max t t', max w w'} (g.comp f) := by
66+
rw [IsStandardSmooth]
67+
algebraize [f, g, (g.comp f)]
68+
letI : Algebra.IsStandardSmooth R S := hf
69+
letI : Algebra.IsStandardSmooth S T := hg
70+
exact Algebra.IsStandardSmooth.trans.{t, t', w, w'} R S T
71+
72+
lemma IsStandardSmoothOfRelativeDimension.comp {g : S →+* T} {f : R →+* S}
73+
(hg : IsStandardSmoothOfRelativeDimension.{t', w'} n g)
74+
(hf : IsStandardSmoothOfRelativeDimension.{t, w} m f) :
75+
IsStandardSmoothOfRelativeDimension.{max t t', max w w'} (n + m) (g.comp f) := by
76+
rw [IsStandardSmoothOfRelativeDimension]
77+
algebraize [f, g, (g.comp f)]
78+
letI : Algebra.IsStandardSmoothOfRelativeDimension m R S := hf
79+
letI : Algebra.IsStandardSmoothOfRelativeDimension n S T := hg
80+
exact Algebra.IsStandardSmoothOfRelativeDimension.trans m n R S T
81+
82+
lemma isStandardSmooth_stableUnderComposition :
83+
StableUnderComposition @IsStandardSmooth.{t, w} :=
84+
fun _ _ _ _ _ _ _ _ hf hg ↦ hg.comp hf
85+
86+
lemma isStandardSmooth_respectsIso : RespectsIso @IsStandardSmooth.{t, w} := by
87+
apply isStandardSmooth_stableUnderComposition.respectsIso
88+
introv
89+
exact (IsStandardSmoothOfRelativeDimension.equiv e).isStandardSmooth
90+
91+
lemma isStandardSmoothOfRelativeDimension_respectsIso :
92+
RespectsIso (@IsStandardSmoothOfRelativeDimension.{t, w} n) where
93+
left {R S T _ _ _} f e hf := by
94+
rw [← zero_add n]
95+
exact (IsStandardSmoothOfRelativeDimension.equiv e).comp hf
96+
right {R S T _ _ _} f e hf := by
97+
rw [← add_zero n]
98+
exact hf.comp (IsStandardSmoothOfRelativeDimension.equiv e)
99+
100+
lemma isStandardSmooth_stableUnderBaseChange : StableUnderBaseChange @IsStandardSmooth.{t, w} := by
101+
apply StableUnderBaseChange.mk
102+
· exact isStandardSmooth_respectsIso
103+
· introv h
104+
replace h : Algebra.IsStandardSmooth R T := by
105+
rw [RingHom.IsStandardSmooth] at h; convert h; ext; simp_rw [Algebra.smul_def]; rfl
106+
suffices Algebra.IsStandardSmooth S (S ⊗[R] T) by
107+
rw [RingHom.IsStandardSmooth]; convert this; ext; simp_rw [Algebra.smul_def]; rfl
108+
infer_instance
109+
110+
variable (n)
111+
112+
lemma isStandardSmoothOfRelativeDimension_stableUnderBaseChange :
113+
StableUnderBaseChange (@IsStandardSmoothOfRelativeDimension.{t, w} n) := by
114+
apply StableUnderBaseChange.mk
115+
· exact isStandardSmoothOfRelativeDimension_respectsIso
116+
· introv h
117+
replace h : Algebra.IsStandardSmoothOfRelativeDimension n R T := by
118+
rw [RingHom.IsStandardSmoothOfRelativeDimension] at h
119+
convert h; ext; simp_rw [Algebra.smul_def]; rfl
120+
suffices Algebra.IsStandardSmoothOfRelativeDimension n S (S ⊗[R] T) by
121+
rw [RingHom.IsStandardSmoothOfRelativeDimension]
122+
convert this; ext; simp_rw [Algebra.smul_def]; rfl
123+
infer_instance
124+
125+
lemma IsStandardSmoothOfRelativeDimension.algebraMap_isLocalizationAway {Rᵣ : Type*} [CommRing Rᵣ]
126+
[Algebra R Rᵣ] (r : R) [IsLocalization.Away r Rᵣ] :
127+
IsStandardSmoothOfRelativeDimension.{0, 0} 0 (algebraMap R Rᵣ) := by
128+
have : (algebraMap R Rᵣ).toAlgebra = ‹Algebra R Rᵣ› := by
129+
ext
130+
rw [Algebra.smul_def]
131+
rfl
132+
rw [IsStandardSmoothOfRelativeDimension, this]
133+
exact Algebra.IsStandardSmoothOfRelativeDimension.localization_away r
134+
135+
lemma isStandardSmooth_localizationPreserves : LocalizationPreserves IsStandardSmooth.{t, w} :=
136+
isStandardSmooth_stableUnderBaseChange.localizationPreserves
137+
138+
lemma isStandardSmoothOfRelativeDimension_localizationPreserves :
139+
LocalizationPreserves (IsStandardSmoothOfRelativeDimension.{t, w} n) :=
140+
(isStandardSmoothOfRelativeDimension_stableUnderBaseChange n).localizationPreserves
141+
142+
lemma isStandardSmooth_holdsForLocalizationAway :
143+
HoldsForLocalizationAway IsStandardSmooth.{0, 0} := by
144+
introv R h
145+
exact (IsStandardSmoothOfRelativeDimension.algebraMap_isLocalizationAway r).isStandardSmooth
146+
147+
lemma isStandardSmoothOfRelativeDimension_holdsForLocalizationAway :
148+
HoldsForLocalizationAway (IsStandardSmoothOfRelativeDimension.{0, 0} 0) := by
149+
introv R h
150+
exact IsStandardSmoothOfRelativeDimension.algebraMap_isLocalizationAway r
151+
152+
lemma isStandardSmooth_stableUnderCompositionWithLocalizationAway :
153+
StableUnderCompositionWithLocalizationAway IsStandardSmooth.{0, 0} :=
154+
isStandardSmooth_stableUnderComposition.stableUnderCompositionWithLocalizationAway
155+
isStandardSmooth_holdsForLocalizationAway
156+
157+
lemma isStandardSmoothOfRelativeDimension_stableUnderCompositionWithLocalizationAway :
158+
StableUnderCompositionWithLocalizationAway (IsStandardSmoothOfRelativeDimension.{0, 0} n) where
159+
left _ S T _ _ _ _ s _ _ hf :=
160+
have : (algebraMap S T).IsStandardSmoothOfRelativeDimension 0 :=
161+
IsStandardSmoothOfRelativeDimension.algebraMap_isLocalizationAway s
162+
zero_add n ▸ IsStandardSmoothOfRelativeDimension.comp this hf
163+
right R S _ _ _ _ _ r _ _ hf :=
164+
have : (algebraMap R S).IsStandardSmoothOfRelativeDimension 0 :=
165+
IsStandardSmoothOfRelativeDimension.algebraMap_isLocalizationAway r
166+
add_zero n ▸ IsStandardSmoothOfRelativeDimension.comp hf this
167+
168+
end RingHom

‎Mathlib/RingTheory/Smooth/StandardSmooth.lean‎

Lines changed: 1 addition & 25 deletions
Original file line numberDiff line numberDiff line change
@@ -89,8 +89,7 @@ variable (n m : ℕ)
8989

9090
namespace Algebra
9191

92-
variable (R : Type u) [CommRing R]
93-
variable (S : Type v) [CommRing S] [Algebra R S]
92+
variable (R : Type u) (S : Type v) [CommRing R] [CommRing S] [Algebra R S]
9493

9594
/--
9695
A `PreSubmersivePresentation` of an `R`-algebra `S` is a `Presentation`
@@ -556,26 +555,3 @@ instance IsStandardSmoothOfRelativeDimension.baseChange
556555
end BaseChange
557556

558557
end Algebra
559-
560-
namespace RingHom
561-
562-
variable {R : Type u} [CommRing R]
563-
variable {S : Type v} [CommRing S]
564-
565-
/-- A ring homomorphism `R →+* S` is standard smooth if `S` is standard smooth as `R`-algebra. -/
566-
def IsStandardSmooth (f : R →+* S) : Prop :=
567-
@Algebra.IsStandardSmooth.{t, w} _ _ _ _ f.toAlgebra
568-
569-
/-- A ring homomorphism `R →+* S` is standard smooth of relative dimension `n` if
570-
`S` is standard smooth of relative dimension `n` as `R`-algebra. -/
571-
def IsStandardSmoothOfRelativeDimension (f : R →+* S) : Prop :=
572-
@Algebra.IsStandardSmoothOfRelativeDimension.{t, w} n _ _ _ _ f.toAlgebra
573-
574-
lemma IsStandardSmoothOfRelativeDimension.isStandardSmooth (f : R →+* S)
575-
(hf : IsStandardSmoothOfRelativeDimension.{t, w} n f) :
576-
IsStandardSmooth.{t, w} f :=
577-
letI : Algebra R S := f.toAlgebra
578-
letI : Algebra.IsStandardSmoothOfRelativeDimension.{t, w} n R S := hf
579-
Algebra.IsStandardSmoothOfRelativeDimension.isStandardSmooth n
580-
581-
end RingHom

0 commit comments

Comments
 (0)