chore(data/zmod/algebra): make zmod.algebra a def (#19197)

riccardobrasca · riccardobrasca · commit 0723536a0522 · 2023-06-19T20:03:53.000Z
`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.
diff --git a/src/data/zmod/algebra.lean b/src/data/zmod/algebra.lean
@@ -24,7 +24,9 @@ instance (p : ℕ) : subsingleton (algebra (zmod p) R) :=
 section
 variables {n : ℕ} (m : ℕ) [char_p R m]
 
-/-- The `zmod n`-algebra structure on rings whose characteristic `m` divides `n` -/
+/-- The `zmod n`-algebra structure on rings whose characteristic `m` divides `n`.
+See note [reducible non-instances]. -/
+@[reducible]
 def algebra' (h : m ∣ n) : algebra (zmod n) R :=
 { smul := λ a r, a * r,
   commutes' := λ a r, show (a * r : R) = r * a,
@@ -39,6 +41,10 @@ def algebra' (h : m ∣ n) : algebra (zmod n) R :=
 
 end
 
-instance (p : ℕ) [char_p R p] : algebra (zmod p) R := algebra' R p dvd_rfl
+/-- The `zmod p`-algebra structure on a ring of characteristic `p`. This is not an
+instance since it creates a diamond with `algebra.id`.
+See note [reducible non-instances]. -/
+@[reducible]
+def algebra (p : ℕ) [char_p R p] : algebra (zmod p) R := algebra' R p dvd_rfl
 
 end zmod
diff --git a/src/field_theory/cardinality.lean b/src/field_theory/cardinality.lean
@@ -36,8 +36,10 @@ universe u
 /-- A finite field has prime power cardinality. -/
 lemma fintype.is_prime_pow_card_of_field {α} [fintype α] [field α] : is_prime_pow (‖α‖) :=
 begin
+  -- TODO: `algebra` version of `char_p.exists`, of type `Σ p, algebra (zmod p) α`
   casesI char_p.exists α with p _,
   haveI hp := fact.mk (char_p.char_is_prime α p),
+  letI : algebra (zmod p) α := zmod.algebra _ _,
   let b := is_noetherian.finset_basis (zmod p) α,
   rw [module.card_fintype b, zmod.card, is_prime_pow_pow_iff],
   { exact hp.1.is_prime_pow },
diff --git a/src/field_theory/finite/galois_field.lean b/src/field_theory/finite/galois_field.lean
@@ -152,8 +152,6 @@ begin
   rw [splits_iff_card_roots, h1, ←finset.card_def, finset.card_univ, h2, zmod.card],
 end
 
-local attribute [-instance] zmod.algebra
-
 /-- A Galois field with exponent 1 is equivalent to `zmod` -/
 def equiv_zmod_p : galois_field p 1 ≃ₐ[zmod p] (zmod p) :=
 let h : (X ^ p ^ 1 : (zmod p)[X]) = X ^ (fintype.card (zmod p)) :=
@@ -229,6 +227,8 @@ begin
     all_goals {apply_instance}, },
   rw ← hpp' at *,
   haveI := fact_iff.2 hp,
+  letI : algebra (zmod p) K := zmod.algebra _ _,
+  letI : algebra (zmod p) K' := zmod.algebra _ _,
   exact alg_equiv_of_card_eq p hKK',
 end
 
diff --git a/src/field_theory/finite/trace.lean b/src/field_theory/finite/trace.lean
@@ -19,14 +19,15 @@ finite field, trace
 namespace finite_field
 
 /-- The trace map from a finite field to its prime field is nongedenerate. -/
-lemma trace_to_zmod_nondegenerate (F : Type*) [field F] [finite F] {a : F}
- (ha : a ≠ 0) : ∃ b : F, algebra.trace (zmod (ring_char F)) F (a * b) ≠ 0 :=
+lemma trace_to_zmod_nondegenerate (F : Type*) [field F] [finite F]
+  [algebra (zmod (ring_char F)) F] {a : F} (ha : a ≠ 0) :
+  ∃ b : F, algebra.trace (zmod (ring_char F)) F (a * b) ≠ 0 :=
 begin
   haveI : fact (ring_char F).prime := ⟨char_p.char_is_prime F _⟩,
   have htr := trace_form_nondegenerate (zmod (ring_char F)) F a,
   simp_rw [algebra.trace_form_apply] at htr,
   by_contra' hf,
-  exact ha (htr hf),
+  exact ha (htr hf)
 end
 
 end finite_field
diff --git a/src/field_theory/is_alg_closed/classification.lean b/src/field_theory/is_alg_closed/classification.lean
@@ -158,10 +158,9 @@ variables {K L : Type} [field K] [field L] [is_alg_closed K] [is_alg_closed L]
 
 /-- Two uncountable algebraically closed fields of characteristic zero are isomorphic
 if they have the same cardinality. -/
-@[nolint def_lemma] lemma ring_equiv_of_cardinal_eq_of_char_zero [char_zero K] [char_zero L]
-  (hK : ℵ₀ < #K) (hKL : #K = #L) : K ≃+* L :=
+lemma ring_equiv_of_cardinal_eq_of_char_zero [char_zero K] [char_zero L]
+  (hK : ℵ₀ < #K) (hKL : #K = #L) : nonempty (K ≃+* L) :=
 begin
-  apply classical.choice,
   cases exists_is_transcendence_basis ℤ
     (show function.injective (algebra_map ℤ K),
       from int.cast_injective) with s hs,
@@ -177,9 +176,10 @@ begin
 end
 
 private lemma ring_equiv_of_cardinal_eq_of_char_p (p : ℕ) [fact p.prime]
-  [char_p K p] [char_p L p] (hK : ℵ₀ < #K) (hKL : #K = #L) : K ≃+* L :=
+  [char_p K p] [char_p L p] (hK : ℵ₀ < #K) (hKL : #K = #L) : nonempty (K ≃+* L) :=
 begin
-  apply classical.choice,
+  letI : algebra (zmod p) K := zmod.algebra _ _,
+  letI : algebra (zmod p) L := zmod.algebra _ _,
   cases exists_is_transcendence_basis (zmod p)
     (show function.injective (algebra_map (zmod p) K),
       from ring_hom.injective _) with s hs,
@@ -198,18 +198,19 @@ end
 
 /-- Two uncountable algebraically closed fields are isomorphic
 if they have the same cardinality and the same characteristic. -/
-@[nolint def_lemma] lemma ring_equiv_of_cardinal_eq_of_char_eq (p : ℕ) [char_p K p] [char_p L p]
-  (hK : ℵ₀ < #K) (hKL : #K = #L) : K ≃+* L :=
+lemma ring_equiv_of_cardinal_eq_of_char_eq (p : ℕ) [char_p K p] [char_p L p]
+  (hK : ℵ₀ < #K) (hKL : #K = #L) : nonempty (K ≃+* L) :=
 begin
-  apply classical.choice,
   rcases char_p.char_is_prime_or_zero K p with hp | hp,
   { haveI : fact p.prime := ⟨hp⟩,
-    exact ⟨ring_equiv_of_cardinal_eq_of_char_p p hK hKL⟩ },
+    letI : algebra (zmod p) K := zmod.algebra _ _,
+    letI : algebra (zmod p) L := zmod.algebra _ _,
+    exact ring_equiv_of_cardinal_eq_of_char_p p hK hKL },
   { rw [hp] at *,
     resetI,
     letI : char_zero K := char_p.char_p_to_char_zero K,
     letI : char_zero L := char_p.char_p_to_char_zero L,
-    exact ⟨ring_equiv_of_cardinal_eq_of_char_zero hK hKL⟩ }
+    exact ring_equiv_of_cardinal_eq_of_char_zero hK hKL }
 end
 
 end is_alg_closed
diff --git a/src/number_theory/legendre_symbol/add_character.lean b/src/number_theory/legendre_symbol/add_character.lean
@@ -355,6 +355,7 @@ begin
       exact λ hf, nat.prime.ne_zero hp.1 (zero_dvd_iff.mp hf), },
   end,
   let ψ := primitive_zmod_char pp F' (ne_zero_iff.mp (ne_zero.of_not_dvd F' hp₂)),
+  letI : algebra (zmod p) F := zmod.algebra _ _,
   let ψ' := ψ.char.comp (algebra.trace (zmod p) F).to_add_monoid_hom.to_multiplicative,
   have hψ' : is_nontrivial ψ' :=
   begin
diff --git a/src/ring_theory/polynomial/cyclotomic/expand.lean b/src/ring_theory/polynomial/cyclotomic/expand.lean
@@ -126,6 +126,7 @@ section char_p
 lemma cyclotomic_mul_prime_eq_pow_of_not_dvd (R : Type*) {p n : ℕ} [hp : fact (nat.prime p)]
   [ring R] [char_p R p] (hn : ¬p ∣ n) : cyclotomic (n * p) R = (cyclotomic n R) ^ (p - 1) :=
 begin
+  letI : algebra (zmod p) R := zmod.algebra _ _,
   suffices : cyclotomic (n * p) (zmod p) = (cyclotomic n (zmod p)) ^ (p - 1),
   { rw [← map_cyclotomic _ (algebra_map (zmod p) R), ← map_cyclotomic _ (algebra_map (zmod p) R),
       this, polynomial.map_pow] },
@@ -141,6 +142,7 @@ end
 lemma cyclotomic_mul_prime_dvd_eq_pow (R : Type*) {p n : ℕ} [hp : fact (nat.prime p)] [ring R]
   [char_p R p] (hn : p ∣ n) : cyclotomic (n * p) R = (cyclotomic n R) ^ p :=
 begin
+  letI : algebra (zmod p) R := zmod.algebra _ _,
   suffices : cyclotomic (n * p) (zmod p) = (cyclotomic n (zmod p)) ^ p,
   { rw [← map_cyclotomic _ (algebra_map (zmod p) R), ← map_cyclotomic _ (algebra_map (zmod p) R),
       this, polynomial.map_pow] },
@@ -171,6 +173,7 @@ lemma is_root_cyclotomic_prime_pow_mul_iff_of_char_p {m k p : ℕ} {R : Type*} [
   [is_domain R] [hp : fact (nat.prime p)] [hchar : char_p R p] {μ : R} [ne_zero (m : R)] :
   (polynomial.cyclotomic (p ^ k * m) R).is_root μ ↔ is_primitive_root μ m :=
 begin
+  letI : algebra (zmod p) R := zmod.algebra _ _,
   rcases k.eq_zero_or_pos with rfl | hk,
   { rw [pow_zero, one_mul, is_root_cyclotomic_iff] },
   refine ⟨λ h, _, λ h, _⟩,
diff --git a/src/ring_theory/witt_vector/frobenius.lean b/src/ring_theory/witt_vector/frobenius.lean
@@ -282,6 +282,7 @@ lemma coeff_frobenius_char_p (x : 𝕎 R) (n : ℕ) :
   coeff (frobenius x) n = (x.coeff n) ^ p :=
 begin
   rw [coeff_frobenius],
+  letI : algebra (zmod p) R := zmod.algebra _ _,
   -- outline of the calculation, proofs follow below
   calc aeval (λ k, x.coeff k) (frobenius_poly p n)
       = aeval (λ k, x.coeff k)
