Skip to content

Commit 30e9b28

Browse files
erdOneerdOne
committed
feat(RingTheory): H¹(L) under localization (#20591)
Co-authored-by: Andrew Yang <36414270+erdOne@users.noreply.github.com>
1 parent 3bf4857 commit 30e9b28

File tree

4 files changed

+374
-2
lines changed

4 files changed

+374
-2
lines changed

‎Mathlib/RingTheory/Etale/Basic.lean‎

Lines changed: 21 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -214,3 +214,24 @@ theorem of_isLocalization_Away (r : R) [IsLocalization.Away r A] : Etale R A whe
214214
end Etale
215215

216216
end Algebra
217+
218+
namespace RingHom
219+
220+
variable {R S : Type u} [CommRing R] [CommRing S]
221+
222+
/--
223+
A ring homomorphism `R →+* A` is formally etale if it is formally unramified and formally smooth.
224+
See `Algebra.FormallyEtale`.
225+
-/
226+
@[algebraize Algebra.FormallyEtale]
227+
def FormallyEtale (f : R →+* S) : Prop :=
228+
letI := f.toAlgebra
229+
Algebra.FormallyEtale R S
230+
231+
lemma formallyEtale_algebraMap [Algebra R S] :
232+
(algebraMap R S).FormallyEtale ↔ Algebra.FormallyEtale R S := by
233+
delta FormallyEtale
234+
congr!
235+
exact Algebra.algebra_ext _ _ fun _ ↦ rfl
236+
237+
end RingHom

‎Mathlib/RingTheory/Etale/Kaehler.lean‎

Lines changed: 326 additions & 2 deletions
Original file line numberDiff line numberDiff line change
@@ -7,13 +7,16 @@ import Mathlib.RingTheory.Etale.Basic
77
import Mathlib.RingTheory.Kaehler.JacobiZariski
88
import Mathlib.RingTheory.Localization.BaseChange
99
import Mathlib.RingTheory.Smooth.Kaehler
10+
import Mathlib.RingTheory.Flat.Localization
1011

1112
/-!
1213
# The differential module and etale algebras
1314
1415
## Main results
15-
`KaehlerDifferential.tensorKaehlerEquivOfFormallyEtale`:
16-
The canonical isomorphism `T ⊗[S] Ω[S⁄R] ≃ₗ[T] Ω[T⁄R]` for `T` a formally etale `S`-algebra.
16+
- `KaehlerDifferential.tensorKaehlerEquivOfFormallyEtale`:
17+
The canonical isomorphism `T ⊗[S] Ω[S⁄R] ≃ₗ[T] Ω[T⁄R]` for `T` a formally etale `S`-algebra.
18+
- `Algebra.tensorH1CotangentOfIsLocalization`:
19+
The canonical isomorphism `T ⊗[S] H¹(L_{S⁄R}) ≃ₗ[T] H¹(L_{T⁄R})` for `T` a localization of `S`.
1720
-/
1821

1922
universe u
@@ -37,6 +40,12 @@ def KaehlerDifferential.tensorKaehlerEquivOfFormallyEtale [Algebra.FormallyEtale
3740
obtain ⟨x, rfl⟩ := (Algebra.H1Cotangent.exact_δ_mapBaseChange R S T x).mp hx
3841
rw [Subsingleton.elim x 0, map_zero]
3942

43+
lemma KaehlerDifferential.tensorKaehlerEquivOfFormallyEtale_symm_D_algebraMap
44+
[Algebra.FormallyEtale S T] (s : S) :
45+
(tensorKaehlerEquivOfFormallyEtale R S T).symm (D R T (algebraMap S T s)) = 1 ⊗ₜ D R S s := by
46+
rw [LinearEquiv.symm_apply_eq, tensorKaehlerEquivOfFormallyEtale_apply, mapBaseChange_tmul,
47+
one_smul, map_D]
48+
4049
lemma KaehlerDifferential.isBaseChange_of_formallyEtale [Algebra.FormallyEtale S T] :
4150
IsBaseChange T (map R R S T) := by
4251
show Function.Bijective _
@@ -51,3 +60,318 @@ instance KaehlerDifferential.isLocalizedModule_map (M : Submonoid S) [IsLocaliza
5160
IsLocalizedModule M (map R R S T) :=
5261
have := Algebra.FormallyEtale.of_isLocalization (Rₘ := T) M
5362
(isLocalizedModule_iff_isBaseChange M T _).mpr (isBaseChange_of_formallyEtale R S T)
63+
64+
namespace Algebra.Extension
65+
66+
open KaehlerDifferential
67+
68+
attribute [local instance] SMulCommClass.of_commMonoid
69+
70+
variable {R S T}
71+
72+
/-!
73+
Suppose we have a morphism of extensions of `R`-algebras
74+
```
75+
0 → J → Q → T → 0
76+
↑ ↑ ↑
77+
0 → I → P → S → 0
78+
```
79+
-/
80+
variable {P : Extension.{u} R S} {Q : Extension.{u} R T} (f : P.Hom Q)
81+
82+
/-- If `P → Q` is formally etale, then `T ⊗ₛ (S ⊗ₚ Ω[P/R]) ≃ T ⊗_Q Ω[Q/R]`. -/
83+
noncomputable
84+
def tensorCotangentSpace
85+
(H : f.toRingHom.FormallyEtale) :
86+
T ⊗[S] P.CotangentSpace ≃ₗ[T] Q.CotangentSpace :=
87+
letI := f.toRingHom.toAlgebra
88+
haveI : IsScalarTower R P.Ring Q.Ring :=
89+
.of_algebraMap_eq fun r ↦ (f.toRingHom_algebraMap r).symm
90+
letI := ((algebraMap S T).comp (algebraMap P.Ring S)).toAlgebra
91+
haveI : IsScalarTower P.Ring S T := .of_algebraMap_eq' rfl
92+
haveI : IsScalarTower P.Ring Q.Ring T :=
93+
.of_algebraMap_eq fun r ↦ (f.algebraMap_toRingHom r).symm
94+
haveI : FormallyEtale P.Ring Q.Ring := ‹_›
95+
{ __ := (CotangentSpace.map f).liftBaseChange T
96+
invFun := LinearMap.liftBaseChange T (by
97+
refine LinearMap.liftBaseChange _ ?_ ∘ₗ
98+
(tensorKaehlerEquivOfFormallyEtale R P.Ring Q.Ring).symm.toLinearMap
99+
exact (TensorProduct.mk _ _ _ 1).restrictScalars P.Ring ∘ₗ
100+
(TensorProduct.mk _ _ _ 1).restrictScalars P.Ring)
101+
left_inv x := by
102+
show (LinearMap.liftBaseChange _ _ ∘ₗ LinearMap.liftBaseChange _ _) x =
103+
LinearMap.id (R := T) x
104+
congr 1
105+
ext : 4
106+
refine Derivation.liftKaehlerDifferential_unique
107+
(R := R) (S := P.Ring) (M := T ⊗[S] P.CotangentSpace) _ _ ?_
108+
ext a
109+
have : (tensorKaehlerEquivOfFormallyEtale R P.Ring Q.Ring).symm
110+
((D R Q.Ring) (f.toRingHom a)) = 1 ⊗ₜ D _ _ a :=
111+
tensorKaehlerEquivOfFormallyEtale_symm_D_algebraMap R P.Ring Q.Ring a
112+
simp [this]
113+
right_inv x := by
114+
show (LinearMap.liftBaseChange _ _ ∘ₗ LinearMap.liftBaseChange _ _) x =
115+
LinearMap.id (R := T) x
116+
congr 1
117+
ext a
118+
dsimp
119+
obtain ⟨x, hx⟩ := (tensorKaehlerEquivOfFormallyEtale R P.Ring _).surjective (D R Q.Ring a)
120+
simp only [one_smul, ← hx, LinearEquiv.symm_apply_apply]
121+
show (((CotangentSpace.map f).liftBaseChange T).restrictScalars Q.Ring ∘ₗ
122+
LinearMap.liftBaseChange _ _) x = ((TensorProduct.mk _ _ _ 1) ∘ₗ
123+
(tensorKaehlerEquivOfFormallyEtale R P.Ring Q.Ring).toLinearMap) x
124+
congr 1
125+
ext a
126+
simp; rfl }
127+
128+
/-- (Implementation)
129+
If `J ≃ Q ⊗ₚ I` (e.g. when `T = Q ⊗ₚ S` and `P → Q` is flat), then `T ⊗ₛ I/I² ≃ J/J²`.
130+
This is the inverse. -/
131+
noncomputable
132+
def tensorCotangentInvFun
133+
[alg : Algebra P.Ring Q.Ring] (halg : algebraMap P.Ring Q.Ring = f.toRingHom)
134+
(H : Function.Bijective ((f.mapKer halg).liftBaseChange Q.Ring)) :
135+
Q.Cotangent →+ T ⊗[S] P.Cotangent :=
136+
letI := ((algebraMap S T).comp (algebraMap P.Ring S)).toAlgebra
137+
haveI : IsScalarTower P.Ring S T := .of_algebraMap_eq' rfl
138+
haveI : IsScalarTower P.Ring Q.Ring T :=
139+
.of_algebraMap_eq fun r ↦ halg ▸ (f.algebraMap_toRingHom r).symm
140+
letI e := LinearEquiv.ofBijective _ H
141+
letI f' : Q.ker →ₗ[Q.Ring] T ⊗[S] P.Cotangent :=
142+
(LinearMap.liftBaseChange _
143+
((TensorProduct.mk _ _ _ 1).restrictScalars _ ∘ₗ Cotangent.mk)) ∘ₗ e.symm.toLinearMap
144+
QuotientAddGroup.lift _ f' <| by
145+
intro x hx
146+
refine Submodule.smul_induction_on hx ?_ fun _ _ ↦ add_mem
147+
clear x hx
148+
rintro a ha b -
149+
obtain ⟨x, hx⟩ := e.surjective ⟨a, ha⟩
150+
obtain rfl : (e x).1 = a := congr_arg Subtype.val hx
151+
obtain ⟨y, rfl⟩ := e.surjective b
152+
simp only [AddMonoidHom.mem_ker, AddMonoidHom.coe_coe, map_smul,
153+
LinearMap.coe_comp, LinearEquiv.coe_coe, Function.comp_apply,
154+
LinearEquiv.symm_apply_apply, f']
155+
clear hx ha
156+
induction x with
157+
| zero => simp only [LinearEquiv.map_zero, ZeroMemClass.coe_zero, zero_smul]
158+
| add x y _ _ =>
159+
simp only [LinearEquiv.map_add, Submodule.coe_add, add_smul, zero_add, *]
160+
| tmul a b =>
161+
induction y with
162+
| zero => simp only [LinearEquiv.map_zero, LinearMap.map_zero, smul_zero]
163+
| add x y hx hy => simp only [LinearMap.map_add, smul_add, hx, hy, zero_add]
164+
| tmul c d =>
165+
simp only [LinearMap.liftBaseChange_tmul, LinearMap.coe_comp, SetLike.val_smul,
166+
LinearMap.coe_restrictScalars, Function.comp_apply, mk_apply, smul_eq_mul, e,
167+
LinearMap.liftBaseChange_tmul, LinearEquiv.ofBijective_apply]
168+
have h₂ : b.1 • Cotangent.mk d = 0 := by ext; simp [Cotangent.smul_eq_zero_of_mem _ b.2]
169+
rw [TensorProduct.smul_tmul', mul_smul, f.mapKer_apply_coe, ← halg,
170+
algebraMap_smul, ← TensorProduct.tmul_smul, h₂, tmul_zero, smul_zero]
171+
172+
omit [IsScalarTower R S T] in
173+
lemma tensorCotangentInvFun_smul_mk
174+
[alg : Algebra P.Ring Q.Ring] (halg : algebraMap P.Ring Q.Ring = f.toRingHom)
175+
(H : Function.Bijective ((f.mapKer halg).liftBaseChange Q.Ring)) (x : Q.Ring) (y : P.ker) :
176+
tensorCotangentInvFun f halg H (x • .mk ⟨f.toRingHom y, (f.mapKer halg y).2⟩) =
177+
x • 1 ⊗ₜ .mk y := by
178+
letI := ((algebraMap S T).comp (algebraMap P.Ring S)).toAlgebra
179+
haveI : IsScalarTower P.Ring S T := .of_algebraMap_eq' rfl
180+
haveI : IsScalarTower P.Ring Q.Ring T :=
181+
.of_algebraMap_eq fun r ↦ halg ▸ (f.algebraMap_toRingHom r).symm
182+
letI e := LinearEquiv.ofBijective _ H
183+
trans tensorCotangentInvFun f halg H (.mk ((f.mapKer halg).liftBaseChange Q.Ring (x ⊗ₜ y)))
184+
· simp; rfl
185+
show ((TensorProduct.mk _ _ _ 1).restrictScalars _ ∘ₗ Cotangent.mk).liftBaseChange _
186+
(e.symm (e (x ⊗ₜ y))) = _
187+
rw [e.symm_apply_apply]
188+
simp
189+
190+
/-- If `J ≃ Q ⊗ₚ I` (e.g. when `T = Q ⊗ₚ S` and `P → Q` is flat), then `T ⊗ₛ I/I² ≃ J/J²`. -/
191+
noncomputable
192+
def tensorCotangent [alg : Algebra P.Ring Q.Ring] (halg : algebraMap P.Ring Q.Ring = f.toRingHom)
193+
(H : Function.Bijective ((f.mapKer halg).liftBaseChange Q.Ring)) :
194+
T ⊗[S] P.Cotangent ≃ₗ[T] Q.Cotangent :=
195+
{ __ := (Cotangent.map f).liftBaseChange T
196+
invFun := tensorCotangentInvFun f halg H
197+
left_inv x := by
198+
simp only [AddHom.toFun_eq_coe, LinearMap.coe_toAddHom]
199+
induction x with
200+
| zero => simp only [map_zero]
201+
| add x y _ _ => simp only [map_add, *]
202+
| tmul a b =>
203+
obtain ⟨b, rfl⟩ := Cotangent.mk_surjective b
204+
obtain ⟨a, rfl⟩ := Q.algebraMap_surjective a
205+
simp only [LinearMap.liftBaseChange_tmul, Cotangent.map_mk, Hom.toAlgHom_apply,
206+
algebraMap_smul, map_smul]
207+
refine (tensorCotangentInvFun_smul_mk f halg H a b).trans ?_
208+
simp [algebraMap_eq_smul_one, TensorProduct.smul_tmul']
209+
right_inv x := by
210+
obtain ⟨x, rfl⟩ := Cotangent.mk_surjective x
211+
obtain ⟨x, rfl⟩ := H.surjective x
212+
simp only [AddHom.toFun_eq_coe, LinearMap.coe_toAddHom]
213+
induction x with
214+
| zero => simp only [map_zero]
215+
| add x y _ _ => simp only [map_add, *]
216+
| tmul a b =>
217+
simp only [LinearMap.liftBaseChange_tmul, map_smul]
218+
erw [tensorCotangentInvFun_smul_mk]
219+
simp
220+
rfl }
221+
222+
/-- If `J ≃ Q ⊗ₚ I`, `S → T` is flat and `P → Q` is formally etale, then `T ⊗ H¹(L_P) ≃ H¹(L_Q)`. -/
223+
noncomputable
224+
def tensorH1Cotangent [alg : Algebra P.Ring Q.Ring] (halg : algebraMap P.Ring Q.Ring = f.toRingHom)
225+
[Module.Flat S T]
226+
(H₁ : f.toRingHom.FormallyEtale)
227+
(H₂ : Function.Bijective ((f.mapKer halg).liftBaseChange Q.Ring)) :
228+
T ⊗[S] P.H1Cotangent ≃ₗ[T] Q.H1Cotangent := by
229+
refine .ofBijective ((H1Cotangent.map f).liftBaseChange T) ?_
230+
constructor
231+
· rw [injective_iff_map_eq_zero]
232+
intro x hx
233+
apply Module.Flat.lTensor_preserves_injective_linearMap _ h1Cotangentι_injective
234+
apply (Extension.tensorCotangent f halg H₂).injective
235+
simp only [map_zero]
236+
rw [← h1Cotangentι.map_zero, ← hx]
237+
show ((Cotangent.map f).liftBaseChange T ∘ₗ h1Cotangentι.baseChange T) x =
238+
(h1Cotangentι ∘ₗ _) x
239+
congr 1
240+
ext x
241+
simp
242+
· intro x
243+
have : Function.Exact (h1Cotangentι.baseChange T) (P.cotangentComplex.baseChange T) :=
244+
Module.Flat.lTensor_exact T (LinearMap.exact_subtype_ker_map _)
245+
obtain ⟨a, ha⟩ := (this ((Extension.tensorCotangent f halg H₂).symm x.1)).mp (by
246+
apply (Extension.tensorCotangentSpace f H₁).injective
247+
rw [map_zero, ← x.2]
248+
have : (CotangentSpace.map f).liftBaseChange T ∘ₗ P.cotangentComplex.baseChange T =
249+
Q.cotangentComplex ∘ₗ (Cotangent.map f).liftBaseChange T := by
250+
ext x; obtain ⟨x, rfl⟩ := Cotangent.mk_surjective x; dsimp
251+
simp only [CotangentSpace.map_tmul,
252+
map_one, Hom.toAlgHom_apply, one_smul, cotangentComplex_mk]
253+
exact (DFunLike.congr_fun this _).trans (DFunLike.congr_arg Q.cotangentComplex
254+
((tensorCotangent f halg H₂).apply_symm_apply x.1)))
255+
refine ⟨a, Subtype.ext (.trans ?_ ((LinearEquiv.eq_symm_apply _).mp ha))⟩
256+
show (h1Cotangentι ∘ₗ (H1Cotangent.map f).liftBaseChange T) _ =
257+
((Cotangent.map f).liftBaseChange T ∘ₗ h1Cotangentι.baseChange T) _
258+
congr 1
259+
ext; simp
260+
261+
end Extension
262+
263+
variable {S}
264+
265+
/-- let `p` be a submonoid of an `R`-algebra `S`. Then `Sₚ ⊗ H¹(L_{S/R}) ≃ H¹(L_{Sₚ/R})`. -/
266+
noncomputable
267+
def tensorH1CotangentOfIsLocalization (M : Submonoid S) [IsLocalization M T] :
268+
T ⊗[S] H1Cotangent R S ≃ₗ[T] H1Cotangent R T := by
269+
letI P : Extension R S := (Generators.self R S).toExtension
270+
letI M' := M.comap (algebraMap P.Ring S)
271+
letI fQ : Localization M' →ₐ[R] T := IsLocalization.liftAlgHom (M := M')
272+
(f := (IsScalarTower.toAlgHom R S T).comp (IsScalarTower.toAlgHom R P.Ring S)) (fun ⟨y, hy⟩ ↦
273+
by simpa using IsLocalization.map_units T ⟨algebraMap P.Ring S y, hy⟩)
274+
letI Q : Extension R T := .ofSurjective fQ (by
275+
intro x
276+
obtain ⟨x, ⟨s, hs⟩, rfl⟩ := IsLocalization.mk'_surjective M x
277+
obtain ⟨x, rfl⟩ := P.algebraMap_surjective x
278+
obtain ⟨s, rfl⟩ := P.algebraMap_surjective s
279+
refine ⟨IsLocalization.mk' _ x ⟨s, show s ∈ M' from hs⟩, ?_⟩
280+
simp only [fQ, IsLocalization.coe_liftAlgHom, AlgHom.toRingHom_eq_coe]
281+
rw [IsLocalization.lift_mk'_spec]
282+
simp)
283+
letI f : P.Hom Q :=
284+
{ toRingHom := algebraMap P.Ring (Localization M')
285+
toRingHom_algebraMap x := (IsScalarTower.algebraMap_apply R P.Ring (Localization M') _).symm
286+
algebraMap_toRingHom x := @IsLocalization.lift_eq .. }
287+
haveI : FormallySmooth R P.Ring := inferInstanceAs (FormallySmooth R (MvPolynomial _ _))
288+
haveI : FormallySmooth P.Ring (Localization M') := .of_isLocalization M'
289+
haveI : FormallySmooth R Q.Ring := .comp R P.Ring (Localization M')
290+
haveI : Module.Flat S T := IsLocalization.flat T M
291+
letI : Algebra P.Ring Q.Ring := inferInstanceAs (Algebra P.Ring (Localization M'))
292+
letI := ((algebraMap S T).comp (algebraMap P.Ring S)).toAlgebra
293+
letI := fQ.toRingHom.toAlgebra
294+
haveI : IsScalarTower P.Ring S T := .of_algebraMap_eq' rfl
295+
haveI : IsScalarTower P.Ring (Localization M') T :=
296+
.of_algebraMap_eq fun r ↦ (f.algebraMap_toRingHom r).symm
297+
haveI : IsLocalizedModule M' (IsScalarTower.toAlgHom P.Ring S T).toLinearMap := by
298+
rw [isLocalizedModule_iff_isLocalization]
299+
convert ‹IsLocalization M T› using 1
300+
exact Submonoid.map_comap_eq_of_surjective P.algebraMap_surjective _
301+
refine Extension.tensorH1Cotangent f rfl ?_ ?_ ≪≫ₗ Extension.equivH1CotangentOfFormallySmooth _
302+
· exact RingHom.formallyEtale_algebraMap.mpr
303+
(FormallyEtale.of_isLocalization (M := M') (Rₘ := Localization M'))
304+
· let F : P.ker →ₗ[P.Ring] RingHom.ker fQ := f.mapKer rfl
305+
refine (isLocalizedModule_iff_isBaseChange M' (Localization M') F).mp ?_
306+
have : (Algebra.linearMap P.Ring S).ker.localized' (Localization M') M'
307+
(Algebra.linearMap P.Ring (Localization M')) = RingHom.ker fQ := by
308+
rw [LinearMap.localized'_ker_eq_ker_localizedMap (Localization M') M'
309+
(Algebra.linearMap P.Ring (Localization M'))
310+
(f' := (IsScalarTower.toAlgHom P.Ring S T).toLinearMap)]
311+
ext x
312+
obtain ⟨x, ⟨s, hs⟩, rfl⟩ := IsLocalization.mk'_surjective M' x
313+
simp only [LinearMap.mem_ker, LinearMap.extendScalarsOfIsLocalization_apply', RingHom.mem_ker,
314+
IsLocalization.coe_liftAlgHom, AlgHom.toRingHom_eq_coe, IsLocalization.lift_mk'_spec,
315+
RingHom.coe_coe, AlgHom.coe_comp, IsScalarTower.coe_toAlgHom', Function.comp_apply,
316+
mul_zero, fQ]
317+
have : IsLocalization.mk' (Localization M') x ⟨s, hs⟩ =
318+
IsLocalizedModule.mk' (Algebra.linearMap P.Ring (Localization M')) x ⟨s, hs⟩ := by
319+
rw [IsLocalization.mk'_eq_iff_eq_mul, mul_comm, ← Algebra.smul_def, ← Submonoid.smul_def,
320+
IsLocalizedModule.mk'_cancel']
321+
rfl
322+
simp [this, ← IsScalarTower.algebraMap_apply]
323+
have : F = ((LinearEquiv.ofEq _ _ this).restrictScalars P.Ring).toLinearMap ∘ₗ
324+
P.ker.toLocalized' (Localization M') M' (Algebra.linearMap P.Ring (Localization M')) := by
325+
ext; rfl
326+
rw [this]
327+
exact IsLocalizedModule.of_linearEquiv _ _ _
328+
329+
lemma tensorH1CotangentOfIsLocalization_toLinearMap
330+
(M : Submonoid S) [IsLocalization M T] :
331+
(tensorH1CotangentOfIsLocalization R T M).toLinearMap =
332+
(Algebra.H1Cotangent.map R R S T).liftBaseChange T := by
333+
ext x : 3
334+
simp only [AlgebraTensorModule.curry_apply, curry_apply, LinearMap.coe_restrictScalars,
335+
LinearEquiv.coe_coe, LinearMap.liftBaseChange_tmul, one_smul]
336+
simp only [tensorH1CotangentOfIsLocalization, Generators.toExtension_Ring,
337+
Generators.toExtension_commRing, Generators.self_vars, Generators.toExtension_algebra₂,
338+
Generators.self_algebra, AlgHom.toRingHom_eq_coe, Extension.tensorH1Cotangent,
339+
LinearEquiv.ofBijective_apply, LinearMap.liftBaseChange_tmul, one_smul,
340+
Extension.equivH1CotangentOfFormallySmooth, LinearEquiv.trans_apply]
341+
letI P : Extension R S := (Generators.self R S).toExtension
342+
letI M' := M.comap (algebraMap P.Ring S)
343+
letI fQ : Localization M' →ₐ[R] T := IsLocalization.liftAlgHom (M := M')
344+
(f := (IsScalarTower.toAlgHom R S T).comp (IsScalarTower.toAlgHom R P.Ring S)) (fun ⟨y, hy⟩ ↦
345+
by simpa using IsLocalization.map_units T ⟨algebraMap P.Ring S y, hy⟩)
346+
letI Q : Extension R T := .ofSurjective fQ (by
347+
intro x
348+
obtain ⟨x, ⟨s, hs⟩, rfl⟩ := IsLocalization.mk'_surjective M x
349+
obtain ⟨x, rfl⟩ := P.algebraMap_surjective x
350+
obtain ⟨s, rfl⟩ := P.algebraMap_surjective s
351+
refine ⟨IsLocalization.mk' _ x ⟨s, show s ∈ M' from hs⟩, ?_⟩
352+
simp only [fQ, IsLocalization.coe_liftAlgHom, AlgHom.toRingHom_eq_coe]
353+
rw [IsLocalization.lift_mk'_spec]
354+
simp)
355+
letI f : (Generators.self R T).toExtension.Hom Q :=
356+
{ toRingHom := (MvPolynomial.aeval Q.σ).toRingHom
357+
toRingHom_algebraMap := (MvPolynomial.aeval Q.σ).commutes
358+
algebraMap_toRingHom := by
359+
have : (IsScalarTower.toAlgHom R Q.Ring T).comp (MvPolynomial.aeval Q.σ) =
360+
IsScalarTower.toAlgHom _ (Generators.self R T).toExtension.Ring _ := by
361+
ext i
362+
show _ = algebraMap (Generators.self R T).Ring _ (.X i)
363+
simp
364+
exact DFunLike.congr_fun this }
365+
rw [← Extension.H1Cotangent.equivOfFormallySmooth_symm, LinearEquiv.symm_apply_eq,
366+
@Extension.H1Cotangent.equivOfFormallySmooth_apply (f := f),
367+
Algebra.H1Cotangent.map, ← (Extension.H1Cotangent.map f).coe_restrictScalars S,
368+
← LinearMap.comp_apply, ← Extension.H1Cotangent.map_comp, Extension.H1Cotangent.map_eq]
369+
370+
instance H1Cotangent.isLocalizedModule (M : Submonoid S) [IsLocalization M T] :
371+
IsLocalizedModule M (Algebra.H1Cotangent.map R R S T) := by
372+
rw [isLocalizedModule_iff_isBaseChange M T]
373+
show Function.Bijective ((Algebra.H1Cotangent.map R R S T).liftBaseChange T)
374+
rw [← tensorH1CotangentOfIsLocalization_toLinearMap R T M]
375+
exact (tensorH1CotangentOfIsLocalization R T M).bijective
376+
377+
end Algebra

‎Mathlib/RingTheory/Extension.lean‎

Lines changed: 9 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -227,6 +227,15 @@ lemma Hom.comp_id (f : Hom P P') : f.comp (Hom.id P) = f := by ext; simp
227227
lemma Hom.id_comp (f : Hom P P') : (Hom.id P').comp f = f := by
228228
ext; simp [Hom.id, aeval_X_left]
229229

230+
/-- A map between extensions induce a map between kernels. -/
231+
@[simps]
232+
def Hom.mapKer (f : P.Hom P')
233+
[alg : Algebra P.Ring P'.Ring] (halg : algebraMap P.Ring P'.Ring = f.toRingHom) :
234+
P.ker →ₗ[P.Ring] P'.ker where
235+
toFun x := ⟨f.toRingHom x, by simp [show algebraMap P.Ring S x = 0 from x.2]⟩
236+
map_add' _ _ := Subtype.ext (map_add _ _ _)
237+
map_smul' := by simp [Algebra.smul_def, ← halg]
238+
230239
end
231240

232241
end Hom

0 commit comments

Comments
 (0)