-
Notifications
You must be signed in to change notification settings - Fork 396
/
Copy pathDiscriminant.lean
107 lines (87 loc) · 4.96 KB
/
Discriminant.lean
1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
44
45
46
47
48
49
50
51
52
53
54
55
56
57
58
59
60
61
62
63
64
65
66
67
68
69
70
71
72
73
74
75
76
77
78
79
80
81
82
83
84
85
86
87
88
89
90
91
92
93
94
95
96
97
98
99
100
101
102
103
104
105
106
107
/-
Copyright (c) 2023 Xavier Roblot. All rights reserved.
Released under Apache 2.0 license as described in the file LICENSE.
Authors: Xavier Roblot
-/
import Mathlib.NumberTheory.NumberField.CanonicalEmbedding
import Mathlib.RingTheory.Localization.NormTrace
/-!
# Number field discriminant
This file defines the discriminant of a number field.
## Main definitions
- `discr` the absolute discriminant of a number field.
## Tags
number field, discriminant
-/
-- TODO. Rewrite some of the FLT results on the disciminant using the definitions and results of
-- this file
local macro_rules | `($x ^ $y) => `(HPow.hPow $x $y) -- Porting note: See issue lean4#2220
namespace NumberField
open Classical NumberField Matrix NumberField.InfinitePlace
variable (K : Type*) [Field K] [NumberField K]
/-- The absolute discriminant of a number field. -/
noncomputable abbrev discr : ℤ := Algebra.discr ℤ (RingOfIntegers.basis K)
theorem coe_discr : (discr K : ℚ) = Algebra.discr ℚ (integralBasis K) :=
(Algebra.discr_localizationLocalization ℤ _ K (RingOfIntegers.basis K)).symm
theorem discr_ne_zero : discr K ≠ 0 := by
rw [← (Int.cast_injective (α := ℚ)).ne_iff, coe_discr]
exact Algebra.discr_not_zero_of_basis ℚ (integralBasis K)
theorem discr_eq_discr {ι : Type*} [Fintype ι] [DecidableEq ι] (b : Basis ι ℤ (𝓞 K)) :
Algebra.discr ℤ b = discr K := by
let b₀ := Basis.reindex (RingOfIntegers.basis K) (Basis.indexEquiv (RingOfIntegers.basis K) b)
rw [Algebra.discr_eq_discr (𝓞 K) b b₀, Basis.coe_reindex, Algebra.discr_reindex]
open MeasureTheory MeasureTheory.Measure Zspan NumberField.mixedEmbedding
NumberField.InfinitePlace ENNReal NNReal Complex
theorem _root_.NumberField.mixedEmbedding.volume_fundamentalDomain_latticeBasis :
volume (fundamentalDomain (latticeBasis K)) =
(2 : ℝ≥0∞)⁻¹ ^ (NrComplexPlaces K) * sqrt ‖discr K‖₊ := by
let f : Module.Free.ChooseBasisIndex ℤ (𝓞 K) ≃ (K →+* ℂ) :=
(canonicalEmbedding.latticeBasis K).indexEquiv (Pi.basisFun ℂ _)
let e : (index K) ≃ Module.Free.ChooseBasisIndex ℤ (𝓞 K) := (indexEquiv K).trans f.symm
let M := (mixedEmbedding.stdBasis K).toMatrix ((latticeBasis K).reindex e.symm)
let N := Algebra.embeddingsMatrixReindex ℚ ℂ (integralBasis K ∘ f.symm)
RingHom.equivRatAlgHom
suffices M.map Complex.ofReal = (matrixToStdBasis K) *
(Matrix.reindex (indexEquiv K).symm (indexEquiv K).symm N).transpose by
calc volume (fundamentalDomain (latticeBasis K))
_ = ‖((mixedEmbedding.stdBasis K).toMatrix ((latticeBasis K).reindex e.symm)).det‖₊ := by
rw [← fundamentalDomain_reindex _ e.symm, ← norm_toNNReal, measure_fundamentalDomain
((latticeBasis K).reindex e.symm), volume_fundamentalDomain_stdBasis, mul_one]
rfl
_ = ‖(matrixToStdBasis K).det * N.det‖₊ := by
rw [← nnnorm_real, ← ofReal_eq_coe, RingHom.map_det, RingHom.mapMatrix_apply, this,
det_mul, det_transpose, det_reindex_self]
_ = (2 : ℝ≥0∞)⁻¹ ^ Fintype.card {w : InfinitePlace K // IsComplex w} * sqrt ‖N.det ^ 2‖₊ := by
have : ‖Complex.I‖₊ = 1 := by rw [← norm_toNNReal, norm_eq_abs, abs_I, Real.toNNReal_one]
rw [det_matrixToStdBasis, nnnorm_mul, nnnorm_pow, nnnorm_mul, this, mul_one, nnnorm_inv,
coe_mul, ENNReal.coe_pow, ← norm_toNNReal, IsROrC.norm_two, Real.toNNReal_ofNat,
coe_inv two_ne_zero, coe_ofNat, nnnorm_pow, NNReal.sqrt_sq]
_ = (2 : ℝ≥0∞)⁻¹ ^ Fintype.card { w // IsComplex w } * NNReal.sqrt ‖discr K‖₊ := by
rw [← Algebra.discr_eq_det_embeddingsMatrixReindex_pow_two, Algebra.discr_reindex,
← coe_discr, map_intCast, ← Complex.nnnorm_int]
ext : 2
dsimp only
rw [Matrix.map_apply, Basis.toMatrix_apply, Basis.coe_reindex, Function.comp, Equiv.symm_symm,
latticeBasis_apply, ← commMap_canonical_eq_mixed, Complex.ofReal_eq_coe,
stdBasis_repr_eq_matrixToStdBasis_mul K _ (fun _ => rfl)]
rfl
end NumberField
namespace Rat
open NumberField
/-- The absolute discriminant of the number field `ℚ` is 1. -/
@[simp]
theorem numberField_discr : discr ℚ = 1 := by
let b : Basis (Fin 1) ℤ (𝓞 ℚ) :=
Basis.map (Basis.singleton (Fin 1) ℤ) ringOfIntegersEquiv.toAddEquiv.toIntLinearEquiv.symm
calc NumberField.discr ℚ
_ = Algebra.discr ℤ b := by convert (discr_eq_discr ℚ b).symm
_ = Algebra.trace ℤ (𝓞 ℚ) (b default * b default) := by
rw [Algebra.discr_def, Matrix.det_unique, Algebra.traceMatrix_apply, Algebra.traceForm_apply]
_ = Algebra.trace ℤ (𝓞 ℚ) 1 := by
rw [Basis.map_apply, RingEquiv.toAddEquiv_eq_coe, AddEquiv.toIntLinearEquiv_symm,
AddEquiv.coe_toIntLinearEquiv, Basis.singleton_apply,
show (AddEquiv.symm ↑ringOfIntegersEquiv) (1 : ℤ) = ringOfIntegersEquiv.symm 1 by rfl,
map_one, mul_one]
_ = 1 := by rw [Algebra.trace_eq_matrix_trace b]; norm_num
alias _root_.NumberField.discr_rat := numberField_discr
end Rat