feat(number_theory/cyclotomic/primitive_roots): generalize finrank le…

…mma (#14550)

We generalize certain results from fields to domains.



Co-authored-by: Eric Rodriguez <ericrboidi@gmail.com>

src/number_theory/cyclotomic/discriminant.lean

@@ -129,8 +129,8 @@ begin
       { replace h := pow_eq_zero h,
         rw [coe_coe] at h,
         exact ne_zero.ne _ h } },
-    { apply_instance } },
-  { apply_instance }
+    all_goals { apply_instance } },
+  all_goals { apply_instance }
 end
 
 /-- If `p` is a prime and `is_cyclotomic_extension {p ^ (k + 1)} K L`, then the discriminant of
@@ -164,7 +164,8 @@ begin
     simp only [trace_matrix, map_one, one_pow, matrix.det_unique, trace_form_apply, mul_one],
     rw [← (algebra_map K L).map_one, trace_algebra_map, finrank _ hirr],
     { simp },
-    { simpa using hcycl } },
+    { apply_instance },
+    { exact hcycl } },
   { by_cases hk : p ^ (k + 1) = 2,
     { haveI : ne_zero ((↑(p ^ (k + 1)) : ℕ) : K),
       { refine ⟨λ hzero, _⟩,
@@ -189,7 +190,8 @@ begin
         pow_zero, trace_form_apply, mul_one],
       rw [← (algebra_map K L).map_one, trace_algebra_map, finrank _ hirr, hp, hk],
       { simp },
-      { apply_instance } },
+      { apply_instance },
+      { exact hcycl } },
     { exact discr_prime_pow_ne_two hζ hirr hk } }
 end
 

src/number_theory/cyclotomic/gal.lean

@@ -143,7 +143,7 @@ let hζ := (zeta_primitive_root n K L).eq_pow_of_pow_eq_one hμ.pow_eq_one n.pos
 lemma from_zeta_aut_spec [ne_zero ((n : ℕ) : K)] : from_zeta_aut hμ h (zeta n K L) = μ :=
 begin
   simp_rw [from_zeta_aut, aut_equiv_pow_symm_apply],
-  generalize_proofs _ hζ h _ hμ _,
+  generalize_proofs _ _ hζ h _ hμ _,
   rw [←hζ.power_basis_gen K] {occs := occurrences.pos [4]},
   rw [power_basis.equiv_of_minpoly_gen, hμ.power_basis_gen K],
   convert h.some_spec.some_spec,

src/number_theory/cyclotomic/primitive_roots.lean

@@ -101,36 +101,37 @@ end zeta
 
 section no_order
 
-variables [field K] [field L] [comm_ring C] [algebra K L] [algebra K C]
-          [is_cyclotomic_extension {n} K L]
+variables [field K] [comm_ring L] [is_domain L] [algebra K L] [is_cyclotomic_extension {n} K L]
           {ζ : L} (hζ : is_primitive_root ζ n)
 
 namespace is_primitive_root
 
-/-- The `power_basis` given by a primitive root `ζ`. -/
-@[simps] noncomputable def power_basis : power_basis K L :=
+variable {C}
+
+/-- The `power_basis` given by a primitive root `η`. -/
+@[simps] protected noncomputable def power_basis : power_basis K L :=
 power_basis.map (algebra.adjoin.power_basis $ integral {n} K L ζ) $
   (subalgebra.equiv_of_eq _ _ (is_cyclotomic_extension.adjoin_primitive_root_eq_top n _ hζ)).trans
   subalgebra.top_equiv
 
 lemma power_basis_gen_mem_adjoin_zeta_sub_one :
-  (power_basis K hζ).gen ∈ adjoin K ({ζ - 1} : set L) :=
+  (hζ.power_basis K).gen ∈ adjoin K ({ζ - 1} : set L) :=
 begin
   rw [power_basis_gen, adjoin_singleton_eq_range_aeval, alg_hom.mem_range],
   exact ⟨X + 1, by simp⟩
 end
 
-/-- The `power_basis` given by `ζ - 1`. -/
-@[simps] noncomputable def sub_one_power_basis (hζ : is_primitive_root ζ n) :
-  _root_.power_basis K L :=
+/-- The `power_basis` given by `η - 1`. -/
+@[simps] noncomputable def sub_one_power_basis : power_basis K L :=
   (hζ.power_basis K).of_gen_mem_adjoin
     (is_integral_sub (is_cyclotomic_extension.integral {n} K L ζ) is_integral_one)
     (hζ.power_basis_gen_mem_adjoin_zeta_sub_one _)
 
-variables {K}
+variables {K} (C)
 
-/-- The equivalence between `L →ₐ[K] A` and `primitive_roots n A` given by a primitive root `ζ`. -/
-@[simps] noncomputable def embeddings_equiv_primitive_roots [is_domain C] [ne_zero ((n : ℕ) : K)]
+/-- The equivalence between `L →ₐ[K] C` and `primitive_roots n C` given by a primitive root `ζ`. -/
+@[simps] noncomputable def embeddings_equiv_primitive_roots (C : Type*) [comm_ring C] [is_domain C]
+  [algebra K C] [ne_zero ((n : ℕ) : K)]
   (hirr : irreducible (cyclotomic n K)) : (L →ₐ[K] C) ≃ primitive_roots n C :=
 ((hζ.power_basis K).lift_equiv).trans
 { to_fun    := λ x,
@@ -222,7 +223,7 @@ begin
   { unfreezingI {subst hn},
     convert norm_eq_neg_one_pow hζ,
     erw [is_cyclotomic_extension.finrank _ hirr, totient_two, pow_one],
-    apply_instance },
+    all_goals { apply_instance } },
   { exact hζ.norm_eq_one hn hirr }
 end