Skip to content

Commit 730d998

Browse files
erdOneerdOne
committed
feat(RingHom): define RingHom.Smooth (#25107)
1 parent b7922f2 commit 730d998

File tree

3 files changed

+137
-1
lines changed

3 files changed

+137
-1
lines changed

‎Mathlib.lean‎

Lines changed: 1 addition & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -5386,6 +5386,7 @@ import Mathlib.RingTheory.RingHom.Flat
53865386
import Mathlib.RingTheory.RingHom.Injective
53875387
import Mathlib.RingTheory.RingHom.Integral
53885388
import Mathlib.RingTheory.RingHom.Locally
5389+
import Mathlib.RingTheory.RingHom.Smooth
53895390
import Mathlib.RingTheory.RingHom.StandardSmooth
53905391
import Mathlib.RingTheory.RingHom.Surjective
53915392
import Mathlib.RingTheory.RingHom.Unramified

‎Mathlib/RingTheory/RingHom/Smooth.lean‎

Lines changed: 134 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,134 @@
1+
/-
2+
Copyright (c) 2025 Andrew Yang. All rights reserved.
3+
Released under Apache 2.0 license as described in the file LICENSE.
4+
Authors: Andrew Yang
5+
-/
6+
import Mathlib.RingTheory.RingHom.FinitePresentation
7+
import Mathlib.RingTheory.Smooth.Locus
8+
9+
/-!
10+
# Smooth ring homomorphisms
11+
12+
In this file we define smooth ring homomorphisms and show their meta properties.
13+
14+
-/
15+
16+
universe u
17+
18+
variable {R S : Type u} [CommRing R] [CommRing S]
19+
20+
open TensorProduct
21+
22+
namespace RingHom
23+
24+
/-- A ring homomorphism `f : R →+* S` is formally smooth
25+
if `S` is formally smooth as an `R` algebra. -/
26+
@[algebraize RingHom.FormallySmooth.toAlgebra]
27+
def FormallySmooth (f : R →+* S) : Prop :=
28+
letI := f.toAlgebra
29+
Algebra.FormallySmooth R S
30+
31+
/-- Helper lemma for the `algebraize` tactic -/
32+
lemma FormallySmooth.toAlgebra {f : R →+* S} (hf : FormallySmooth f) :
33+
@Algebra.FormallySmooth R _ S _ f.toAlgebra := hf
34+
35+
lemma formallySmooth_algebraMap [Algebra R S] :
36+
(algebraMap R S).FormallySmooth ↔ Algebra.FormallySmooth R S := by
37+
delta FormallySmooth
38+
congr!
39+
exact Algebra.algebra_ext _ _ fun _ ↦ rfl
40+
41+
lemma FormallySmooth.holdsForLocalizationAway : HoldsForLocalizationAway @FormallySmooth :=
42+
fun _ _ _ _ _ r _ ↦ formallySmooth_algebraMap.mpr <| .of_isLocalization (.powers r)
43+
44+
lemma FormallySmooth.stableUnderComposition : StableUnderComposition @FormallySmooth := by
45+
intros R S T _ _ _ f g hf hg
46+
algebraize [f, g, g.comp f]
47+
exact .comp R S T
48+
49+
lemma FormallySmooth.respectsIso : RespectsIso @FormallySmooth :=
50+
stableUnderComposition.respectsIso fun e ↦ holdsForLocalizationAway.of_bijective _ _ e.bijective
51+
52+
lemma FormallySmooth.isStableUnderBaseChange : IsStableUnderBaseChange @FormallySmooth := by
53+
refine .mk respectsIso ?_
54+
intros R S T _ _ _ _ _ H
55+
show (algebraMap _ _).FormallySmooth
56+
rw [formallySmooth_algebraMap] at H ⊢
57+
infer_instance
58+
59+
lemma FormallySmooth.localizationPreserves : LocalizationPreserves @FormallySmooth :=
60+
isStableUnderBaseChange.localizationPreserves
61+
62+
/-- A ring homomorphism `f : R →+* S` is smooth if `S` is smooth as an `R` algebra. -/
63+
@[algebraize RingHom.Smooth.toAlgebra]
64+
def Smooth (f : R →+* S) : Prop :=
65+
letI : Algebra R S := f.toAlgebra
66+
Algebra.Smooth R S
67+
68+
/-- Helper lemma for the `algebraize` tactic -/
69+
lemma Smooth.toAlgebra {f : R →+* S} (hf : Smooth f) :
70+
@Algebra.Smooth R _ S _ f.toAlgebra := hf
71+
72+
lemma smooth_algebraMap [Algebra R S] :
73+
(algebraMap R S).Smooth ↔ Algebra.Smooth R S := by
74+
simp only [RingHom.Smooth]
75+
congr!
76+
exact Algebra.algebra_ext _ _ fun _ ↦ rfl
77+
78+
lemma smooth_def {f : R →+* S} : f.Smooth ↔ f.FormallySmooth ∧ f.FinitePresentation :=
79+
letI := f.toAlgebra
80+
Algebra.smooth_iff _ _
81+
82+
namespace Smooth
83+
84+
variable {R S T : Type u} [CommRing R] [CommRing S] [CommRing T]
85+
86+
lemma stableUnderComposition : StableUnderComposition Smooth := by
87+
convert RingHom.FormallySmooth.stableUnderComposition.and
88+
RingHom.finitePresentation_stableUnderComposition
89+
rw [smooth_def]
90+
91+
lemma isStableUnderBaseChange : IsStableUnderBaseChange Smooth := by
92+
convert RingHom.FormallySmooth.isStableUnderBaseChange.and
93+
RingHom.finitePresentation_isStableUnderBaseChange
94+
rw [smooth_def]
95+
96+
lemma holdsForLocalizationAway : HoldsForLocalizationAway Smooth := by
97+
introv R h
98+
rw [smooth_algebraMap]
99+
exact ⟨Algebra.FormallySmooth.of_isLocalization (.powers r),
100+
IsLocalization.Away.finitePresentation r⟩
101+
102+
variable (R) in
103+
/-- The identity of a ring is smooth. -/
104+
lemma id : RingHom.Smooth (RingHom.id R) :=
105+
holdsForLocalizationAway.containsIdentities R
106+
107+
/-- Composition of smooth ring homomorphisms is smooth. -/
108+
lemma comp {f : R →+* S} {g : S →+* T} (hf : f.Smooth) (hg : g.Smooth) : (g.comp f).Smooth :=
109+
stableUnderComposition f g hf hg
110+
111+
lemma ofLocalizationSpanTarget : OfLocalizationSpanTarget Smooth := by
112+
introv R hs hf
113+
have : f.FinitePresentation :=
114+
finitePresentation_ofLocalizationSpanTarget _ s hs fun r ↦ (hf r).finitePresentation
115+
algebraize [f]
116+
refine ⟨?_, ‹_›⟩
117+
rw [← Algebra.smoothLocus_eq_univ_iff, ← Set.univ_subset_iff, ← TopologicalSpace.Opens.coe_top,
118+
← PrimeSpectrum.iSup_basicOpen_eq_top_iff'.mpr hs]
119+
simp only [TopologicalSpace.Opens.coe_iSup, Set.iUnion_subset_iff,
120+
Algebra.basicOpen_subset_smoothLocus_iff, ← formallySmooth_algebraMap]
121+
exact fun r hr ↦ (hf ⟨r, hr⟩).1
122+
123+
/-- Smoothness is a local property of ring homomorphisms. -/
124+
lemma propertyIsLocal : PropertyIsLocal Smooth where
125+
localizationAwayPreserves := isStableUnderBaseChange.localizationPreserves.away
126+
ofLocalizationSpanTarget := ofLocalizationSpanTarget
127+
ofLocalizationSpan := ofLocalizationSpanTarget.ofLocalizationSpan
128+
(stableUnderComposition.stableUnderCompositionWithLocalizationAway
129+
holdsForLocalizationAway).left
130+
StableUnderCompositionWithLocalizationAwayTarget :=
131+
(stableUnderComposition.stableUnderCompositionWithLocalizationAway
132+
holdsForLocalizationAway).right
133+
134+
end RingHom.Smooth

‎Mathlib/RingTheory/Smooth/Basic.lean‎

Lines changed: 2 additions & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -331,7 +331,8 @@ variable (A : Type u) [Semiring A] [Algebra R A]
331331

332332
/-- An `R` algebra `A` is smooth if it is formally smooth and of finite presentation. -/
333333
@[stacks 00T2 "In the stacks project, the definition of smooth is completely different, and tag
334-
<https://stacks.math.columbia.edu/tag/00TN> proves that their definition is equivalent to this."]
334+
<https://stacks.math.columbia.edu/tag/00TN> proves that their definition is equivalent to this.",
335+
mk_iff]
335336
class Smooth [CommSemiring R] (A : Type u) [Semiring A] [Algebra R A] : Prop where
336337
formallySmooth : FormallySmooth R A := by infer_instance
337338
finitePresentation : FinitePresentation R A := by infer_instance

0 commit comments

Comments
 (0)