Skip to content
This repository was archived by the owner on Jul 24, 2024. It is now read-only.

Commit 0723536

Browse files
chore(data/zmod/algebra): make zmod.algebra a def (#19197)
`zmod.algebra` creates a diamond about the `zmod p`-algebra structure on `zmod p`: ```lean import algebra.algebra.basic import data.zmod.algebra example (p : ℕ) : algebra.id (zmod p) = (zmod.algebra (zmod p) p) := rfl --fails ``` This is also causing troubles with the port. We turn `zmod.algebra` into a def.
1 parent e160cef commit 0723536

File tree

8 files changed

+32
-17
lines changed

8 files changed

+32
-17
lines changed

src/data/zmod/algebra.lean

Lines changed: 8 additions & 2 deletions
Original file line numberDiff line numberDiff line change
@@ -24,7 +24,9 @@ instance (p : ℕ) : subsingleton (algebra (zmod p) R) :=
2424
section
2525
variables {n : ℕ} (m : ℕ) [char_p R m]
2626

27-
/-- The `zmod n`-algebra structure on rings whose characteristic `m` divides `n` -/
27+
/-- The `zmod n`-algebra structure on rings whose characteristic `m` divides `n`.
28+
See note [reducible non-instances]. -/
29+
@[reducible]
2830
def algebra' (h : m ∣ n) : algebra (zmod n) R :=
2931
{ smul := λ a r, a * r,
3032
commutes' := λ a r, show (a * r : R) = r * a,
@@ -39,6 +41,10 @@ def algebra' (h : m ∣ n) : algebra (zmod n) R :=
3941

4042
end
4143

42-
instance (p : ℕ) [char_p R p] : algebra (zmod p) R := algebra' R p dvd_rfl
44+
/-- The `zmod p`-algebra structure on a ring of characteristic `p`. This is not an
45+
instance since it creates a diamond with `algebra.id`.
46+
See note [reducible non-instances]. -/
47+
@[reducible]
48+
def algebra (p : ℕ) [char_p R p] : algebra (zmod p) R := algebra' R p dvd_rfl
4349

4450
end zmod

src/field_theory/cardinality.lean

Lines changed: 2 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -36,8 +36,10 @@ universe u
3636
/-- A finite field has prime power cardinality. -/
3737
lemma fintype.is_prime_pow_card_of_field {α} [fintype α] [field α] : is_prime_pow (‖α‖) :=
3838
begin
39+
-- TODO: `algebra` version of `char_p.exists`, of type `Σ p, algebra (zmod p) α`
3940
casesI char_p.exists α with p _,
4041
haveI hp := fact.mk (char_p.char_is_prime α p),
42+
letI : algebra (zmod p) α := zmod.algebra _ _,
4143
let b := is_noetherian.finset_basis (zmod p) α,
4244
rw [module.card_fintype b, zmod.card, is_prime_pow_pow_iff],
4345
{ exact hp.1.is_prime_pow },

src/field_theory/finite/galois_field.lean

Lines changed: 2 additions & 2 deletions
Original file line numberDiff line numberDiff line change
@@ -152,8 +152,6 @@ begin
152152
rw [splits_iff_card_roots, h1, ←finset.card_def, finset.card_univ, h2, zmod.card],
153153
end
154154

155-
local attribute [-instance] zmod.algebra
156-
157155
/-- A Galois field with exponent 1 is equivalent to `zmod` -/
158156
def equiv_zmod_p : galois_field p 1 ≃ₐ[zmod p] (zmod p) :=
159157
let h : (X ^ p ^ 1 : (zmod p)[X]) = X ^ (fintype.card (zmod p)) :=
@@ -229,6 +227,8 @@ begin
229227
all_goals {apply_instance}, },
230228
rw ← hpp' at *,
231229
haveI := fact_iff.2 hp,
230+
letI : algebra (zmod p) K := zmod.algebra _ _,
231+
letI : algebra (zmod p) K' := zmod.algebra _ _,
232232
exact alg_equiv_of_card_eq p hKK',
233233
end
234234

src/field_theory/finite/trace.lean

Lines changed: 4 additions & 3 deletions
Original file line numberDiff line numberDiff line change
@@ -19,14 +19,15 @@ finite field, trace
1919
namespace finite_field
2020

2121
/-- The trace map from a finite field to its prime field is nongedenerate. -/
22-
lemma trace_to_zmod_nondegenerate (F : Type*) [field F] [finite F] {a : F}
23-
(ha : a ≠ 0) : ∃ b : F, algebra.trace (zmod (ring_char F)) F (a * b) ≠ 0 :=
22+
lemma trace_to_zmod_nondegenerate (F : Type*) [field F] [finite F]
23+
[algebra (zmod (ring_char F)) F] {a : F} (ha : a ≠ 0) :
24+
∃ b : F, algebra.trace (zmod (ring_char F)) F (a * b) ≠ 0 :=
2425
begin
2526
haveI : fact (ring_char F).prime := ⟨char_p.char_is_prime F _⟩,
2627
have htr := trace_form_nondegenerate (zmod (ring_char F)) F a,
2728
simp_rw [algebra.trace_form_apply] at htr,
2829
by_contra' hf,
29-
exact ha (htr hf),
30+
exact ha (htr hf)
3031
end
3132

3233
end finite_field

src/field_theory/is_alg_closed/classification.lean

Lines changed: 11 additions & 10 deletions
Original file line numberDiff line numberDiff line change
@@ -158,10 +158,9 @@ variables {K L : Type} [field K] [field L] [is_alg_closed K] [is_alg_closed L]
158158

159159
/-- Two uncountable algebraically closed fields of characteristic zero are isomorphic
160160
if they have the same cardinality. -/
161-
@[nolint def_lemma] lemma ring_equiv_of_cardinal_eq_of_char_zero [char_zero K] [char_zero L]
162-
(hK : ℵ₀ < #K) (hKL : #K = #L) : K ≃+* L :=
161+
lemma ring_equiv_of_cardinal_eq_of_char_zero [char_zero K] [char_zero L]
162+
(hK : ℵ₀ < #K) (hKL : #K = #L) : nonempty (K ≃+* L) :=
163163
begin
164-
apply classical.choice,
165164
cases exists_is_transcendence_basis ℤ
166165
(show function.injective (algebra_map ℤ K),
167166
from int.cast_injective) with s hs,
@@ -177,9 +176,10 @@ begin
177176
end
178177

179178
private lemma ring_equiv_of_cardinal_eq_of_char_p (p : ℕ) [fact p.prime]
180-
[char_p K p] [char_p L p] (hK : ℵ₀ < #K) (hKL : #K = #L) : K ≃+* L :=
179+
[char_p K p] [char_p L p] (hK : ℵ₀ < #K) (hKL : #K = #L) : nonempty (K ≃+* L) :=
181180
begin
182-
apply classical.choice,
181+
letI : algebra (zmod p) K := zmod.algebra _ _,
182+
letI : algebra (zmod p) L := zmod.algebra _ _,
183183
cases exists_is_transcendence_basis (zmod p)
184184
(show function.injective (algebra_map (zmod p) K),
185185
from ring_hom.injective _) with s hs,
@@ -198,18 +198,19 @@ end
198198

199199
/-- Two uncountable algebraically closed fields are isomorphic
200200
if they have the same cardinality and the same characteristic. -/
201-
@[nolint def_lemma] lemma ring_equiv_of_cardinal_eq_of_char_eq (p : ℕ) [char_p K p] [char_p L p]
202-
(hK : ℵ₀ < #K) (hKL : #K = #L) : K ≃+* L :=
201+
lemma ring_equiv_of_cardinal_eq_of_char_eq (p : ℕ) [char_p K p] [char_p L p]
202+
(hK : ℵ₀ < #K) (hKL : #K = #L) : nonempty (K ≃+* L) :=
203203
begin
204-
apply classical.choice,
205204
rcases char_p.char_is_prime_or_zero K p with hp | hp,
206205
{ haveI : fact p.prime := ⟨hp⟩,
207-
exact ⟨ring_equiv_of_cardinal_eq_of_char_p p hK hKL⟩ },
206+
letI : algebra (zmod p) K := zmod.algebra _ _,
207+
letI : algebra (zmod p) L := zmod.algebra _ _,
208+
exact ring_equiv_of_cardinal_eq_of_char_p p hK hKL },
208209
{ rw [hp] at *,
209210
resetI,
210211
letI : char_zero K := char_p.char_p_to_char_zero K,
211212
letI : char_zero L := char_p.char_p_to_char_zero L,
212-
exact ring_equiv_of_cardinal_eq_of_char_zero hK hKL }
213+
exact ring_equiv_of_cardinal_eq_of_char_zero hK hKL }
213214
end
214215

215216
end is_alg_closed

src/number_theory/legendre_symbol/add_character.lean

Lines changed: 1 addition & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -355,6 +355,7 @@ begin
355355
exact λ hf, nat.prime.ne_zero hp.1 (zero_dvd_iff.mp hf), },
356356
end,
357357
let ψ := primitive_zmod_char pp F' (ne_zero_iff.mp (ne_zero.of_not_dvd F' hp₂)),
358+
letI : algebra (zmod p) F := zmod.algebra _ _,
358359
let ψ' := ψ.char.comp (algebra.trace (zmod p) F).to_add_monoid_hom.to_multiplicative,
359360
have hψ' : is_nontrivial ψ' :=
360361
begin

src/ring_theory/polynomial/cyclotomic/expand.lean

Lines changed: 3 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -126,6 +126,7 @@ section char_p
126126
lemma cyclotomic_mul_prime_eq_pow_of_not_dvd (R : Type*) {p n : ℕ} [hp : fact (nat.prime p)]
127127
[ring R] [char_p R p] (hn : ¬p ∣ n) : cyclotomic (n * p) R = (cyclotomic n R) ^ (p - 1) :=
128128
begin
129+
letI : algebra (zmod p) R := zmod.algebra _ _,
129130
suffices : cyclotomic (n * p) (zmod p) = (cyclotomic n (zmod p)) ^ (p - 1),
130131
{ rw [← map_cyclotomic _ (algebra_map (zmod p) R), ← map_cyclotomic _ (algebra_map (zmod p) R),
131132
this, polynomial.map_pow] },
@@ -141,6 +142,7 @@ end
141142
lemma cyclotomic_mul_prime_dvd_eq_pow (R : Type*) {p n : ℕ} [hp : fact (nat.prime p)] [ring R]
142143
[char_p R p] (hn : p ∣ n) : cyclotomic (n * p) R = (cyclotomic n R) ^ p :=
143144
begin
145+
letI : algebra (zmod p) R := zmod.algebra _ _,
144146
suffices : cyclotomic (n * p) (zmod p) = (cyclotomic n (zmod p)) ^ p,
145147
{ rw [← map_cyclotomic _ (algebra_map (zmod p) R), ← map_cyclotomic _ (algebra_map (zmod p) R),
146148
this, polynomial.map_pow] },
@@ -171,6 +173,7 @@ lemma is_root_cyclotomic_prime_pow_mul_iff_of_char_p {m k p : ℕ} {R : Type*} [
171173
[is_domain R] [hp : fact (nat.prime p)] [hchar : char_p R p] {μ : R} [ne_zero (m : R)] :
172174
(polynomial.cyclotomic (p ^ k * m) R).is_root μ ↔ is_primitive_root μ m :=
173175
begin
176+
letI : algebra (zmod p) R := zmod.algebra _ _,
174177
rcases k.eq_zero_or_pos with rfl | hk,
175178
{ rw [pow_zero, one_mul, is_root_cyclotomic_iff] },
176179
refine ⟨λ h, _, λ h, _⟩,

src/ring_theory/witt_vector/frobenius.lean

Lines changed: 1 addition & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -282,6 +282,7 @@ lemma coeff_frobenius_char_p (x : 𝕎 R) (n : ℕ) :
282282
coeff (frobenius x) n = (x.coeff n) ^ p :=
283283
begin
284284
rw [coeff_frobenius],
285+
letI : algebra (zmod p) R := zmod.algebra _ _,
285286
-- outline of the calculation, proofs follow below
286287
calc aeval (λ k, x.coeff k) (frobenius_poly p n)
287288
= aeval (λ k, x.coeff k)

0 commit comments

Comments
 (0)