-
Notifications
You must be signed in to change notification settings - Fork 251
/
PowerBasis.lean
188 lines (163 loc) · 8.3 KB
/
PowerBasis.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
108
109
110
111
112
113
114
115
116
117
118
119
120
121
122
123
124
125
126
127
128
129
130
131
132
133
134
135
136
137
138
139
140
141
142
143
144
145
146
147
148
149
150
151
152
153
154
155
156
157
158
159
160
161
162
163
164
165
166
167
168
169
170
171
172
173
174
175
176
177
178
179
180
181
182
183
184
185
186
187
188
/-
Copyright (c) 2021 Anne Baanen. All rights reserved.
Released under Apache 2.0 license as described in the file LICENSE.
Authors: Anne Baanen
-/
import Mathlib.RingTheory.Adjoin.Basic
import Mathlib.RingTheory.PowerBasis
import Mathlib.LinearAlgebra.Matrix.Basis
#align_import ring_theory.adjoin.power_basis from "leanprover-community/mathlib"@"825edd3cd735e87495b0c2a2114fc3929eefce41"
/-!
# Power basis for `Algebra.adjoin R {x}`
This file defines the canonical power basis on `Algebra.adjoin R {x}`,
where `x` is an integral element over `R`.
-/
variable {K S : Type*} [Field K] [CommRing S] [Algebra K S]
namespace Algebra
open Polynomial
open PowerBasis
/-- The elements `1, x, ..., x ^ (d - 1)` for a basis for the `K`-module `K[x]`,
where `d` is the degree of the minimal polynomial of `x`. -/
noncomputable def adjoin.powerBasisAux {x : S} (hx : IsIntegral K x) :
Basis (Fin (minpoly K x).natDegree) K (adjoin K ({x} : Set S)) := by
have hST : Function.Injective (algebraMap (adjoin K ({x} : Set S)) S) := Subtype.coe_injective
have hx' :
IsIntegral K (⟨x, subset_adjoin (Set.mem_singleton x)⟩ : adjoin K ({x} : Set S)) := by
apply (isIntegral_algebraMap_iff hST).mp
convert hx
apply
@Basis.mk (Fin (minpoly K x).natDegree) _ (adjoin K {x}) fun i =>
⟨x, subset_adjoin (Set.mem_singleton x)⟩ ^ (i : ℕ)
· have : LinearIndependent K _ := linearIndependent_pow
(⟨x, self_mem_adjoin_singleton _ _⟩ : adjoin K {x})
rwa [← minpoly.algebraMap_eq hST] at this
· rintro ⟨y, hy⟩ _
have := hx'.mem_span_pow (y := ⟨y, hy⟩)
rw [← minpoly.algebraMap_eq hST] at this
apply this
rw [adjoin_singleton_eq_range_aeval] at hy
obtain ⟨f, rfl⟩ := (aeval x).mem_range.mp hy
use f
ext
exact aeval_algebraMap_apply S (⟨x, _⟩ : adjoin K {x}) _
#align algebra.adjoin.power_basis_aux Algebra.adjoin.powerBasisAux
/-- The power basis `1, x, ..., x ^ (d - 1)` for `K[x]`,
where `d` is the degree of the minimal polynomial of `x`. See `Algebra.adjoin.powerBasis'` for
a version over a more general base ring. -/
@[simps gen dim]
noncomputable def adjoin.powerBasis {x : S} (hx : IsIntegral K x) :
PowerBasis K (adjoin K ({x} : Set S)) where
gen := ⟨x, subset_adjoin (Set.mem_singleton x)⟩
dim := (minpoly K x).natDegree
basis := adjoin.powerBasisAux hx
basis_eq_pow i := by rw [adjoin.powerBasisAux, Basis.mk_apply]
#align algebra.adjoin.power_basis Algebra.adjoin.powerBasis
end Algebra
open Algebra
/-- The power basis given by `x` if `B.gen ∈ adjoin K {x}`. See `PowerBasis.ofGenMemAdjoin'`
for a version over a more general base ring. -/
@[simps!]
noncomputable def PowerBasis.ofGenMemAdjoin {x : S} (B : PowerBasis K S) (hint : IsIntegral K x)
(hx : B.gen ∈ adjoin K ({x} : Set S)) : PowerBasis K S :=
(Algebra.adjoin.powerBasis hint).map <|
(Subalgebra.equivOfEq _ _ <| PowerBasis.adjoin_eq_top_of_gen_mem_adjoin hx).trans
Subalgebra.topEquiv
#align power_basis.of_gen_mem_adjoin PowerBasis.ofGenMemAdjoin
section IsIntegral
namespace PowerBasis
open Polynomial
open Polynomial
variable {R : Type*} [CommRing R] [Algebra R S] [Algebra R K] [IsScalarTower R K S]
variable {A : Type*} [CommRing A] [Algebra R A] [Algebra S A]
variable [IsScalarTower R S A] {B : PowerBasis S A} (hB : IsIntegral R B.gen)
/-- If `B : PowerBasis S A` is such that `IsIntegral R B.gen`, then
`IsIntegral R (B.basis.repr (B.gen ^ n) i)` for all `i` if
`minpoly S B.gen = (minpoly R B.gen).map (algebraMap R S)`. This is the case if `R` is a GCD domain
and `S` is its fraction ring. -/
theorem repr_gen_pow_isIntegral [IsDomain S]
(hmin : minpoly S B.gen = (minpoly R B.gen).map (algebraMap R S)) (n : ℕ) :
∀ i, IsIntegral R (B.basis.repr (B.gen ^ n) i) := by
intro i
let Q := X ^ n %ₘ minpoly R B.gen
have : B.gen ^ n = aeval B.gen Q := by
rw [← @aeval_X_pow R _ _ _ _ B.gen, ← modByMonic_add_div (X ^ n) (minpoly.monic hB)]
simp
by_cases hQ : Q = 0
· simp [this, hQ, isIntegral_zero]
have hlt : Q.natDegree < B.dim := by
rw [← B.natDegree_minpoly, hmin, (minpoly.monic hB).natDegree_map,
natDegree_lt_natDegree_iff hQ]
letI : Nontrivial R := Nontrivial.of_polynomial_ne hQ
exact degree_modByMonic_lt _ (minpoly.monic hB)
rw [this, aeval_eq_sum_range' hlt]
simp only [map_sum, LinearEquiv.map_smulₛₗ, RingHom.id_apply, Finset.sum_apply']
refine IsIntegral.sum _ fun j hj => ?_
replace hj := Finset.mem_range.1 hj
rw [← Fin.val_mk hj, ← B.basis_eq_pow, Algebra.smul_def, IsScalarTower.algebraMap_apply R S A, ←
Algebra.smul_def, LinearEquiv.map_smul]
simp only [algebraMap_smul, Finsupp.coe_smul, Pi.smul_apply, B.basis.repr_self_apply]
by_cases hij : (⟨j, hj⟩ : Fin _) = i
· simp only [hij, eq_self_iff_true, if_true]
rw [Algebra.smul_def, mul_one]
exact isIntegral_algebraMap
· simp [hij, isIntegral_zero]
#align power_basis.repr_gen_pow_is_integral PowerBasis.repr_gen_pow_isIntegral
/-- Let `B : PowerBasis S A` be such that `IsIntegral R B.gen`, and let `x y : A` be elements with
integral coordinates in the base `B.basis`. Then `IsIntegral R ((B.basis.repr (x * y) i)` for all
`i` if `minpoly S B.gen = (minpoly R B.gen).map (algebraMap R S)`. This is the case if `R` is a GCD
domain and `S` is its fraction ring. -/
theorem repr_mul_isIntegral [IsDomain S] {x y : A} (hx : ∀ i, IsIntegral R (B.basis.repr x i))
(hy : ∀ i, IsIntegral R (B.basis.repr y i))
(hmin : minpoly S B.gen = (minpoly R B.gen).map (algebraMap R S)) :
∀ i, IsIntegral R (B.basis.repr (x * y) i) := by
intro i
rw [← B.basis.sum_repr x, ← B.basis.sum_repr y, Finset.sum_mul_sum, ← Finset.sum_product',
map_sum, Finset.sum_apply']
refine IsIntegral.sum _ fun I _ => ?_
simp only [Algebra.smul_mul_assoc, Algebra.mul_smul_comm, LinearEquiv.map_smulₛₗ,
RingHom.id_apply, Finsupp.coe_smul, Pi.smul_apply, id.smul_eq_mul]
refine (hy _).mul ((hx _).mul ?_)
simp only [coe_basis, ← pow_add]
exact repr_gen_pow_isIntegral hB hmin _ _
#align power_basis.repr_mul_is_integral PowerBasis.repr_mul_isIntegral
/-- Let `B : PowerBasis S A` be such that `IsIntegral R B.gen`, and let `x : A` be an element
with integral coordinates in the base `B.basis`. Then `IsIntegral R ((B.basis.repr (x ^ n) i)` for
all `i` and all `n` if `minpoly S B.gen = (minpoly R B.gen).map (algebraMap R S)`. This is the case
if `R` is a GCD domain and `S` is its fraction ring. -/
theorem repr_pow_isIntegral [IsDomain S] {x : A} (hx : ∀ i, IsIntegral R (B.basis.repr x i))
(hmin : minpoly S B.gen = (minpoly R B.gen).map (algebraMap R S)) (n : ℕ) :
∀ i, IsIntegral R (B.basis.repr (x ^ n) i) := by
nontriviality A using Subsingleton.elim (x ^ n) 0, isIntegral_zero
revert hx
refine Nat.case_strong_induction_on
-- Porting note: had to hint what to induct on
(p := fun n ↦ _ → ∀ (i : Fin B.dim), IsIntegral R (B.basis.repr (x ^ n) i))
n ?_ fun n hn => ?_
· intro _ i
rw [pow_zero, ← pow_zero B.gen, ← Fin.val_mk B.dim_pos, ← B.basis_eq_pow,
B.basis.repr_self_apply]
split_ifs
· exact isIntegral_one
· exact isIntegral_zero
· intro hx
rw [pow_succ]
exact repr_mul_isIntegral hB (fun _ => hn _ le_rfl (fun _ => hx _) _) hx hmin
#align power_basis.repr_pow_is_integral PowerBasis.repr_pow_isIntegral
/-- Let `B B' : PowerBasis K S` be such that `IsIntegral R B.gen`, and let `P : R[X]` be such that
`aeval B.gen P = B'.gen`. Then `IsIntegral R (B.basis.to_matrix B'.basis i j)` for all `i` and `j`
if `minpoly K B.gen = (minpoly R B.gen).map (algebraMap R L)`. This is the case
if `R` is a GCD domain and `K` is its fraction ring. -/
theorem toMatrix_isIntegral {B B' : PowerBasis K S} {P : R[X]} (h : aeval B.gen P = B'.gen)
(hB : IsIntegral R B.gen) (hmin : minpoly K B.gen = (minpoly R B.gen).map (algebraMap R K)) :
∀ i j, IsIntegral R (B.basis.toMatrix B'.basis i j) := by
intro i j
rw [B.basis.toMatrix_apply, B'.coe_basis]
refine repr_pow_isIntegral hB (fun i => ?_) hmin _ _
rw [← h, aeval_eq_sum_range, map_sum, Finset.sum_apply']
refine IsIntegral.sum _ fun n _ => ?_
rw [Algebra.smul_def, IsScalarTower.algebraMap_apply R K S, ← Algebra.smul_def,
LinearEquiv.map_smul, algebraMap_smul]
exact (repr_gen_pow_isIntegral hB hmin _ _).smul _
#align power_basis.to_matrix_is_integral PowerBasis.toMatrix_isIntegral
end PowerBasis
end IsIntegral