Skip to content

Commit e7f7075

Browse files
Parcly-TaxelParcly-Taxel
committed
feat: port RingTheory.DedekindDomain.IntegralClosure (#5304)
1 parent 6074c43 commit e7f7075

File tree

2 files changed

+292
-0
lines changed

2 files changed

+292
-0
lines changed

‎Mathlib.lean‎

Lines changed: 1 addition & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -2498,6 +2498,7 @@ import Mathlib.RingTheory.DedekindDomain.Basic
24982498
import Mathlib.RingTheory.DedekindDomain.Dvr
24992499
import Mathlib.RingTheory.DedekindDomain.Factorization
25002500
import Mathlib.RingTheory.DedekindDomain.Ideal
2501+
import Mathlib.RingTheory.DedekindDomain.IntegralClosure
25012502
import Mathlib.RingTheory.DedekindDomain.PID
25022503
import Mathlib.RingTheory.Derivation.Basic
25032504
import Mathlib.RingTheory.Derivation.Lie

‎Mathlib/RingTheory/DedekindDomain/IntegralClosure.lean‎

Lines changed: 291 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,291 @@
1+
/-
2+
Copyright (c) 2020 Kenji Nakagawa. All rights reserved.
3+
Released under Apache 2.0 license as described in the file LICENSE.
4+
Authors: Kenji Nakagawa, Anne Baanen, Filippo A. E. Nuccio
5+
6+
! This file was ported from Lean 3 source module ring_theory.dedekind_domain.integral_closure
7+
! leanprover-community/mathlib commit 4cf7ca0e69e048b006674cf4499e5c7d296a89e0
8+
! Please do not edit these lines, except to modify the commit id
9+
! if you have ported upstream changes.
10+
-/
11+
import Mathlib.LinearAlgebra.FreeModule.PID
12+
import Mathlib.RingTheory.DedekindDomain.Basic
13+
import Mathlib.RingTheory.Localization.Module
14+
import Mathlib.RingTheory.Trace
15+
16+
/-!
17+
# Integral closure of Dedekind domains
18+
19+
This file shows the integral closure of a Dedekind domain (in particular, the ring of integers
20+
of a number field) is a Dedekind domain.
21+
22+
## Implementation notes
23+
24+
The definitions that involve a field of fractions choose a canonical field of fractions,
25+
but are independent of that choice. The `..._iff` lemmas express this independence.
26+
27+
Often, definitions assume that Dedekind domains are not fields. We found it more practical
28+
to add a `(h : ¬IsField A)` assumption whenever this is explicitly needed.
29+
30+
## References
31+
32+
* [D. Marcus, *Number Fields*][marcus1977number]
33+
* [J.W.S. Cassels, A. Frölich, *Algebraic Number Theory*][cassels1967algebraic]
34+
* [J. Neukirch, *Algebraic Number Theory*][Neukirch1992]
35+
36+
## Tags
37+
38+
dedekind domain, dedekind ring
39+
-/
40+
41+
42+
variable (R A K : Type _) [CommRing R] [CommRing A] [Field K]
43+
44+
open scoped nonZeroDivisors Polynomial
45+
46+
variable [IsDomain A]
47+
48+
section IsIntegralClosure
49+
50+
/-! ### `IsIntegralClosure` section
51+
52+
We show that an integral closure of a Dedekind domain in a finite separable
53+
field extension is again a Dedekind domain. This implies the ring of integers
54+
of a number field is a Dedekind domain. -/
55+
56+
57+
open Algebra
58+
59+
open scoped BigOperators
60+
61+
variable [Algebra A K] [IsFractionRing A K]
62+
63+
variable (L : Type _) [Field L] (C : Type _) [CommRing C]
64+
65+
variable [Algebra K L] [Algebra A L] [IsScalarTower A K L]
66+
67+
variable [Algebra C L] [IsIntegralClosure C A L] [Algebra A C] [IsScalarTower A C L]
68+
69+
/- If `L` is a separable extension of `K = Frac(A)` and `L` has no zero smul divisors by `A`,
70+
then `L` is the localization of the integral closure `C` of `A` in `L` at `A⁰`. -/
71+
theorem IsIntegralClosure.isLocalization [IsSeparable K L] [NoZeroSMulDivisors A L] :
72+
IsLocalization (Algebra.algebraMapSubmonoid C A⁰) L := by
73+
haveI : IsDomain C :=
74+
(IsIntegralClosure.equiv A C L (integralClosure A L)).toRingEquiv.isDomain (integralClosure A L)
75+
haveI : NoZeroSMulDivisors A C := IsIntegralClosure.noZeroSMulDivisors A L
76+
refine' ⟨_, fun z => _, fun {x y} => ⟨fun h => ⟨1, _⟩, _⟩⟩
77+
· rintro ⟨_, x, hx, rfl⟩
78+
rw [isUnit_iff_ne_zero, map_ne_zero_iff _ (IsIntegralClosure.algebraMap_injective C A L),
79+
Subtype.coe_mk, map_ne_zero_iff _ (NoZeroSMulDivisors.algebraMap_injective A C)]
80+
exact mem_nonZeroDivisors_iff_ne_zero.mp hx
81+
· obtain ⟨m, hm⟩ :=
82+
IsIntegral.exists_multiple_integral_of_isLocalization A⁰ z (IsSeparable.isIntegral K z)
83+
obtain ⟨x, hx⟩ : ∃ x, algebraMap C L x = m • z := IsIntegralClosure.isIntegral_iff.mp hm
84+
refine' ⟨⟨x, algebraMap A C m, m, SetLike.coe_mem m, rfl⟩, _⟩
85+
rw [Subtype.coe_mk, ← IsScalarTower.algebraMap_apply, hx, mul_comm, Submonoid.smul_def,
86+
smul_def]
87+
· simp only [IsIntegralClosure.algebraMap_injective C A L h]
88+
· rintro ⟨⟨_, m, hm, rfl⟩, h⟩
89+
refine' congr_arg (algebraMap C L) ((mul_right_inj' _).mp h)
90+
rw [Subtype.coe_mk, map_ne_zero_iff _ (NoZeroSMulDivisors.algebraMap_injective A C)]
91+
exact mem_nonZeroDivisors_iff_ne_zero.mp hm
92+
#align is_integral_closure.is_localization IsIntegralClosure.isLocalization
93+
94+
variable [FiniteDimensional K L]
95+
96+
variable {A K L}
97+
98+
theorem IsIntegralClosure.range_le_span_dualBasis [IsSeparable K L] {ι : Type _} [Fintype ι]
99+
[DecidableEq ι] (b : Basis ι K L) (hb_int : ∀ i, IsIntegral A (b i)) [IsIntegrallyClosed A] :
100+
LinearMap.range ((Algebra.linearMap C L).restrictScalars A) ≤
101+
Submodule.span A (Set.range <| (traceForm K L).dualBasis (traceForm_nondegenerate K L) b) := by
102+
let db := (traceForm K L).dualBasis (traceForm_nondegenerate K L) b
103+
rintro _ ⟨x, rfl⟩
104+
simp only [LinearMap.coe_restrictScalars, Algebra.linearMap_apply]
105+
have hx : IsIntegral A (algebraMap C L x) := (IsIntegralClosure.isIntegral A L x).algebraMap
106+
rsuffices ⟨c, x_eq⟩ : ∃ c : ι → A, algebraMap C L x = ∑ i, c i • db i
107+
· rw [x_eq]
108+
refine' Submodule.sum_mem _ fun i _ => Submodule.smul_mem _ _ (Submodule.subset_span _)
109+
rw [Set.mem_range]
110+
exact ⟨i, rfl⟩
111+
suffices ∃ c : ι → K, (∀ i, IsIntegral A (c i)) ∧ algebraMap C L x = ∑ i, c i • db i by
112+
obtain ⟨c, hc, hx⟩ := this
113+
have hc' : ∀ i, IsLocalization.IsInteger A (c i) := fun i =>
114+
IsIntegrallyClosed.isIntegral_iff.mp (hc i)
115+
use fun i => Classical.choose (hc' i)
116+
refine' hx.trans (Finset.sum_congr rfl fun i _ => _)
117+
conv_lhs => rw [← Classical.choose_spec (hc' i)]
118+
rw [← IsScalarTower.algebraMap_smul K (Classical.choose (hc' i)) (db i)]
119+
refine' ⟨fun i => db.repr (algebraMap C L x) i, fun i => _, (db.sum_repr _).symm⟩
120+
simp_rw [BilinForm.dualBasis_repr_apply]
121+
exact isIntegral_trace (isIntegral_mul hx (hb_int i))
122+
#align is_integral_closure.range_le_span_dual_basis IsIntegralClosure.range_le_span_dualBasis
123+
124+
theorem integralClosure_le_span_dualBasis [IsSeparable K L] {ι : Type _} [Fintype ι] [DecidableEq ι]
125+
(b : Basis ι K L) (hb_int : ∀ i, IsIntegral A (b i)) [IsIntegrallyClosed A] :
126+
Subalgebra.toSubmodule (integralClosure A L) ≤
127+
Submodule.span A (Set.range <| (traceForm K L).dualBasis (traceForm_nondegenerate K L) b) := by
128+
refine' le_trans _ (IsIntegralClosure.range_le_span_dualBasis (integralClosure A L) b hb_int)
129+
intro x hx
130+
exact ⟨⟨x, hx⟩, rfl⟩
131+
#align integral_closure_le_span_dual_basis integralClosure_le_span_dualBasis
132+
133+
variable (A K)
134+
135+
/-- Send a set of `x`s in a finite extension `L` of the fraction field of `R`
136+
to `(y : R) • x ∈ integralClosure R L`. -/
137+
theorem exists_integral_multiples (s : Finset L) :
138+
∃ (y : _) (_ : y ≠ (0 : A)), ∀ x ∈ s, IsIntegral A (y • x) := by
139+
haveI := Classical.decEq L
140+
refine' s.induction _ _
141+
· use 1, one_ne_zero
142+
rintro x ⟨⟩
143+
· rintro x s hx ⟨y, hy, hs⟩
144+
have := exists_integral_multiple
145+
((IsFractionRing.isAlgebraic_iff A K L).mpr (isAlgebraic_of_finite _ _ x))
146+
((injective_iff_map_eq_zero (algebraMap A L)).mp ?_)
147+
rcases this with ⟨x', y', hy', hx'⟩
148+
refine' ⟨y * y', mul_ne_zero hy hy', fun x'' hx'' => _⟩
149+
rcases Finset.mem_insert.mp hx'' with (rfl | hx'')
150+
· rw [mul_smul, Algebra.smul_def, Algebra.smul_def, mul_comm _ x'', hx']
151+
exact isIntegral_mul isIntegral_algebraMap x'.2
152+
· rw [mul_comm, mul_smul, Algebra.smul_def]
153+
exact isIntegral_mul isIntegral_algebraMap (hs _ hx'')
154+
· rw [IsScalarTower.algebraMap_eq A K L]
155+
apply (algebraMap K L).injective.comp
156+
exact IsFractionRing.injective _ _
157+
#align exists_integral_multiples exists_integral_multiples
158+
159+
variable (L)
160+
161+
/-- If `L` is a finite extension of `K = Frac(A)`,
162+
then `L` has a basis over `A` consisting of integral elements. -/
163+
theorem FiniteDimensional.exists_is_basis_integral :
164+
∃ (s : Finset L) (b : Basis s K L), ∀ x, IsIntegral A (b x) := by
165+
letI := Classical.decEq L
166+
letI : IsNoetherian K L := IsNoetherian.iff_fg.2 inferInstance
167+
let s' := IsNoetherian.finsetBasisIndex K L
168+
let bs' := IsNoetherian.finsetBasis K L
169+
obtain ⟨y, hy, his'⟩ := exists_integral_multiples A K (Finset.univ.image bs')
170+
have hy' : algebraMap A L y ≠ 0 := by
171+
refine' mt ((injective_iff_map_eq_zero (algebraMap A L)).mp _ _) hy
172+
rw [IsScalarTower.algebraMap_eq A K L]
173+
exact (algebraMap K L).injective.comp (IsFractionRing.injective A K)
174+
refine ⟨s', bs'.map {Algebra.lmul _ _ (algebraMap A L y) with
175+
toFun := fun x => algebraMap A L y * x
176+
invFun := fun x => (algebraMap A L y)⁻¹ * x
177+
left_inv := ?_
178+
right_inv := ?_}, ?_⟩
179+
· intro x; simp only [inv_mul_cancel_left₀ hy']
180+
· intro x; simp only [mul_inv_cancel_left₀ hy']
181+
· rintro ⟨x', hx'⟩
182+
simp only [Algebra.smul_def, Finset.mem_image, exists_prop, Finset.mem_univ,
183+
true_and_iff] at his'
184+
simp only [Basis.map_apply, LinearEquiv.coe_mk]
185+
exact his' _ ⟨_, rfl⟩
186+
#align finite_dimensional.exists_is_basis_integral FiniteDimensional.exists_is_basis_integral
187+
188+
variable [IsSeparable K L]
189+
190+
/- If `L` is a finite separable extension of `K = Frac(A)`, where `A` is
191+
integrally closed and Noetherian, the integral closure `C` of `A` in `L` is
192+
Noetherian over `A`. -/
193+
theorem IsIntegralClosure.isNoetherian [IsIntegrallyClosed A] [IsNoetherianRing A] :
194+
IsNoetherian A C := by
195+
haveI := Classical.decEq L
196+
obtain ⟨s, b, hb_int⟩ := FiniteDimensional.exists_is_basis_integral A K L
197+
let b' := (traceForm K L).dualBasis (traceForm_nondegenerate K L) b
198+
letI := isNoetherian_span_of_finite A (Set.finite_range b')
199+
let f : C →ₗ[A] Submodule.span A (Set.range b') :=
200+
(Submodule.ofLe (IsIntegralClosure.range_le_span_dualBasis C b hb_int)).comp
201+
((Algebra.linearMap C L).restrictScalars A).rangeRestrict
202+
refine' isNoetherian_of_ker_bot f _
203+
rw [LinearMap.ker_comp, Submodule.ker_ofLe, Submodule.comap_bot, LinearMap.ker_codRestrict]
204+
exact LinearMap.ker_eq_bot_of_injective (IsIntegralClosure.algebraMap_injective C A L)
205+
#align is_integral_closure.is_noetherian IsIntegralClosure.isNoetherian
206+
207+
/- If `L` is a finite separable extension of `K = Frac(A)`, where `A` is
208+
integrally closed and Noetherian, the integral closure `C` of `A` in `L` is
209+
Noetherian. -/
210+
theorem IsIntegralClosure.isNoetherianRing [IsIntegrallyClosed A] [IsNoetherianRing A] :
211+
IsNoetherianRing C :=
212+
isNoetherianRing_iff.mpr <| isNoetherian_of_tower A (IsIntegralClosure.isNoetherian A K L C)
213+
#align is_integral_closure.is_noetherian_ring IsIntegralClosure.isNoetherianRing
214+
215+
/- If `L` is a finite separable extension of `K = Frac(A)`, where `A` is a principal ring
216+
and `L` has no zero smul divisors by `A`, the integral closure `C` of `A` in `L` is
217+
a free `A`-module. -/
218+
theorem IsIntegralClosure.module_free [NoZeroSMulDivisors A L] [IsPrincipalIdealRing A] :
219+
Module.Free A C := by
220+
haveI : NoZeroSMulDivisors A C := IsIntegralClosure.noZeroSMulDivisors A L
221+
haveI : IsNoetherian A C := IsIntegralClosure.isNoetherian A K L _
222+
exact Module.free_of_finite_type_torsion_free'
223+
#align is_integral_closure.module_free IsIntegralClosure.module_free
224+
225+
/- If `L` is a finite separable extension of `K = Frac(A)`, where `A` is a principal ring
226+
and `L` has no zero smul divisors by `A`, the `A`-rank of the integral closure `C` of `A` in `L`
227+
is equal to the `K`-rank of `L`. -/
228+
theorem IsIntegralClosure.rank [IsPrincipalIdealRing A] [NoZeroSMulDivisors A L] :
229+
FiniteDimensional.finrank A C = FiniteDimensional.finrank K L := by
230+
haveI : Module.Free A C := IsIntegralClosure.module_free A K L C
231+
haveI : IsNoetherian A C := IsIntegralClosure.isNoetherian A K L C
232+
haveI : IsLocalization (Algebra.algebraMapSubmonoid C A⁰) L :=
233+
IsIntegralClosure.isLocalization A K L C
234+
let b := Basis.localizationLocalization K A⁰ L (Module.Free.chooseBasis A C)
235+
rw [FiniteDimensional.finrank_eq_card_chooseBasisIndex, FiniteDimensional.finrank_eq_card_basis b]
236+
#align is_integral_closure.rank IsIntegralClosure.rank
237+
238+
variable {A K}
239+
240+
/- If `L` is a finite separable extension of `K = Frac(A)`, where `A` is
241+
integrally closed and Noetherian, the integral closure of `A` in `L` is
242+
Noetherian. -/
243+
theorem integralClosure.isNoetherianRing [IsIntegrallyClosed A] [IsNoetherianRing A] :
244+
IsNoetherianRing (integralClosure A L) :=
245+
IsIntegralClosure.isNoetherianRing A K L (integralClosure A L)
246+
#align integral_closure.is_noetherian_ring integralClosure.isNoetherianRing
247+
248+
variable (A K) [IsDomain C]
249+
250+
/- If `L` is a finite separable extension of `K = Frac(A)`, where `A` is a Dedekind domain,
251+
the integral closure `C` of `A` in `L` is a Dedekind domain.
252+
253+
Can't be an instance since `A`, `K` or `L` can't be inferred. See also the instance
254+
`integralClosure.isDedekindDomain_fractionRing` where `K := FractionRing A`
255+
and `C := integralClosure A L`.
256+
-/
257+
theorem IsIntegralClosure.isDedekindDomain [h : IsDedekindDomain A] : IsDedekindDomain C :=
258+
haveI : IsFractionRing C L := IsIntegralClosure.isFractionRing_of_finite_extension A K L C
259+
⟨IsIntegralClosure.isNoetherianRing A K L C, h.dimensionLEOne.isIntegralClosure _ L _,
260+
(isIntegrallyClosed_iff L).mpr fun {x} hx =>
261+
⟨IsIntegralClosure.mk' C x (isIntegral_trans (IsIntegralClosure.isIntegral_algebra A L) _ hx),
262+
IsIntegralClosure.algebraMap_mk' _ _ _⟩⟩
263+
#align is_integral_closure.is_dedekind_domain IsIntegralClosure.isDedekindDomain
264+
265+
/- If `L` is a finite separable extension of `K = Frac(A)`, where `A` is a Dedekind domain,
266+
the integral closure of `A` in `L` is a Dedekind domain.
267+
268+
Can't be an instance since `K` can't be inferred. See also the instance
269+
`integralClosure.isDedekindDomain_fractionRing` where `K := FractionRing A`.
270+
-/
271+
theorem integralClosure.isDedekindDomain [IsDedekindDomain A] :
272+
IsDedekindDomain (integralClosure A L) :=
273+
IsIntegralClosure.isDedekindDomain A K L (integralClosure A L)
274+
#align integral_closure.is_dedekind_domain integralClosure.isDedekindDomain
275+
276+
variable [Algebra (FractionRing A) L] [IsScalarTower A (FractionRing A) L]
277+
278+
variable [FiniteDimensional (FractionRing A) L] [IsSeparable (FractionRing A) L]
279+
280+
/- If `L` is a finite separable extension of `Frac(A)`, where `A` is a Dedekind domain,
281+
the integral closure of `A` in `L` is a Dedekind domain.
282+
283+
See also the lemma `integralClosure.isDedekindDomain` where you can choose
284+
the field of fractions yourself.
285+
-/
286+
instance integralClosure.isDedekindDomain_fractionRing [IsDedekindDomain A] :
287+
IsDedekindDomain (integralClosure A L) :=
288+
integralClosure.isDedekindDomain A (FractionRing A) L
289+
#align integral_closure.is_dedekind_domain_fraction_ring integralClosure.isDedekindDomain_fractionRing
290+
291+
end IsIntegralClosure

0 commit comments

Comments
 (0)