Statements about finite rings

Stream: Is there code for X?

[Michael Stoll]

I am unable to find the following statements in mathlib:

import tactic
import algebra.char_p.basic

lemma prime_dvd_char_iff_dvd_card {R} [comm_ring R] [fintype R] (p : ℕ) [fact p.prime] :
  p ∣ ring_char R ↔ p ∣ fintype.card R := sorry

lemma char_ne_zero_of_finite (R) [comm_ring R] [fintype R] : ring_char R ≠ 0 :=  sorry

(I guess [ring R] would be enough.)
Did I overlook something? Are there easy proofs using what is available?

[Michael Stoll]

Here is a proof of the second one:

lemma char_ne_zero_of_finite (R) [non_assoc_ring R] [fintype R] : ring_char R ≠ 0 :=
begin
  intro h,
  haveI := eq.mp (congr_arg (char_p R) h) (ring_char.char_p R),
  haveI := char_p.char_p_to_char_zero R,
  exact not_injective_infinite_fintype (coe : ℕ → R) nat.cast_injective,
end

[Michael Stoll]

#14454 for char_ne_zero_of_finite

[Michael Stoll]

For rings, there is char_p.char_ne_zero_of_fintype, so one has

lemma char_ne_zero_of_finite' (R) [ring R] [fintype R] : ring_char R ≠ 0 :=
char_p.char_ne_zero_of_fintype R (ring_char R)

[Michael Stoll]

OK, the proof of char_p.char_ne_zero_of_fintype also works for [non_assoc_ring R]. I'll add this (and the simpler proof) to the PR.

[Floris van Doorn]

docs#char_zero.infinite should be close to the second one.

[Michael Stoll]

Yes; the proof of docs#char_p.char_ne_zero_of_fintype is more or less (and up to fiddling with char_zero vs. char_p _ 0) the same as that of docs#char_zero.infinite.

[Michael Stoll]

Using exists_prime_add_order_of_dvd_card of #14471, I have now completed the proofs I needed:

import tactic
import algebra.char_p.basic
import group_theory.perm.cycle.type

-- still with `equiv.perm.` prefix to make it work with current mathlib
lemma exists_prime_add_order_of_dvd_card {G : Type*} [add_group G] [fintype G] (p : ℕ)
  [hp : fact p.prime] (hdvd : p ∣ fintype.card G) : ∃ x : G, add_order_of x = p :=
@equiv.perm.exists_prime_order_of_dvd_card (multiplicative G) _ _ _ _ hdvd

lemma is_unit_iff_not_dvd_char (R) [comm_ring R] [fintype R] (p : ℕ) [fact p.prime] :
  is_unit (p : R) ↔ ¬ p ∣ ring_char R :=
begin
  have hch := char_p.cast_eq_zero R (ring_char R),
  split,
  { intros h₁ h₂,
    rcases is_unit.exists_left_inv h₁ with ⟨a, ha⟩,
    rcases h₂ with ⟨q, hq⟩,
    have h₃ : ¬ ring_char R ∣ q :=
    begin
      rintro ⟨r, hr⟩,
      rw [hr, ← mul_assoc, mul_comm p, mul_assoc] at hq,
      nth_rewrite 0 ← mul_one (ring_char R) at hq,
      exact nat.prime.not_dvd_one (fact.out p.prime)
             ⟨r, mul_left_cancel₀ (char_p.char_ne_zero_of_fintype R (ring_char R)) hq⟩,
    end,
    have h₄ := mt (char_p.int_cast_eq_zero_iff R (ring_char R) q).mp,
    apply_fun (coe : ℕ → R) at hq,
    apply_fun ((*) a) at hq,
    rw [nat.cast_mul, hch, mul_zero, ← mul_assoc, ha, one_mul] at hq,
    norm_cast at h₄,
    exact h₄ h₃ hq.symm, },
  { intro h,
    rcases nat.is_coprime_iff_coprime.mpr ((nat.prime.coprime_iff_not_dvd (fact.out _)).mpr h)
      with ⟨a, b, hab⟩,
    apply_fun (coe : ℤ → R) at hab,
    push_cast at hab,
    rw [hch, mul_zero, add_zero, mul_comm] at hab,
    exact is_unit_of_mul_eq_one (p : R) a hab, },
end

lemma prime_dvd_char_iff_dvd_card {R} [comm_ring R] [fintype R] (p : ℕ) [fact p.prime] :
  p ∣ ring_char R ↔ p ∣ fintype.card R :=
begin
  split,
  { exact λ h, nat.dvd_trans h (int.coe_nat_dvd.mp ((char_p.int_cast_eq_zero_iff R (ring_char R)
                (fintype.card R)).mp (char_p.cast_card_eq_zero R))), },
  { intro h,
    by_contra h₀,
    rcases exists_prime_add_order_of_dvd_card p h with ⟨r, hr⟩,
    have hr₁ : (p : R) * r = 0 :=
    by { have h₀ := add_order_of_nsmul_eq_zero r, rw [hr, nsmul_eq_mul] at h₀, exact h₀, },
    rcases is_unit.exists_left_inv ((is_unit_iff_not_dvd_char R p).mpr h₀) with ⟨u, hu⟩,
    apply_fun ((*) u) at hr₁,
    rw [mul_zero, ← mul_assoc, hu, one_mul] at hr₁,
    exact mt add_monoid.order_of_eq_one_iff.mpr
                 (ne_of_eq_of_ne hr (nat.prime.ne_one (fact.out p.prime))) hr₁, },
end

lemma not_is_unit_prime_of_dvd_card {R} [comm_ring R] [fintype R] (p : ℕ) [fact p.prime]
 (hp : p ∣ fintype.card R) : ¬ is_unit (p : R) :=
mt (is_unit_iff_not_dvd_char R p).mp (not_not.mpr ((prime_dvd_char_iff_dvd_card p).mpr hp))

[Michael Stoll]

I'm going to add these to the auxiliary results in my working version of the Legendre symbol code, unless people want me to add this to mathlib now.

[Kevin Buzzard]

Nice! What are your long term goals here?

[Michael Stoll]

@Kevin Buzzard short-term I want the last statment for use in a proof related to Gauss sums.
A little bit longer-term, this will be part of the Gauss sum proof of Quadratic Reciprocity (and the supplementary law for 2), by which I want to replace the combinatorial proof that is currently in mathlib (which seems to be a bit inefficient; also, the Gauss sum proof gives a more general statement for quadratic characters).

[Kevin Buzzard]

Cubic and quartic reciprocity would be really cool to have; one could follow the approach in Ireland-Rosen.

[Michael Stoll]

Yes, but what I really want to do is get the product formula for the Hilbert symbol into mathlib.

[Michael Stoll]

@Kevin Buzzard I'm planning to run a seminar on formalising results from number theory during the next winter semester here. This could be an opportunity to make some progress in this direction. I'll probably contact you at some point to get advice on how to do it.

[Kevin Buzzard]

Sure! Your students would be welcome to use my Discord. They will probably have a course whatsapp group or discord anyway, and they may as well use mine because there will be more experts in it.