feat(*): finite rings with char = card = n are isomorphic to zmod n (#4234)

From the Witt vector project

I've made use of the opportunity to remove some unused arguments,
and to clean up some code by using namespacing and such.

Co-authored-by: Rob Y. Lewis <rob.y.lewis@gmail.com>

Author: jcommelin

src/algebra/char_p.lean

@@ -9,6 +9,8 @@ import data.nat.choose
 import data.int.modeq
 import algebra.module.basic
 import algebra.iterate_hom
+import group_theory.order_of_element
+import algebra.group.type_tags
 
 /-!
 # Characteristic of semirings
@@ -23,6 +25,13 @@ class char_p (α : Type u) [semiring α] (p : ℕ) : Prop :=
 theorem char_p.cast_eq_zero (α : Type u) [semiring α] (p : ℕ) [char_p α p] : (p:α) = 0 :=
 (char_p.cast_eq_zero_iff α p p).2 (dvd_refl p)
 
+@[simp] lemma char_p.cast_card_eq_zero (R : Type*) [ring R] [fintype R] : (fintype.card R : R) = 0 :=
+begin
+  have : fintype.card R •ℕ (1 : R) = 0 :=
+    @pow_card_eq_one (multiplicative R) _ _ (multiplicative.of_add 1),
+  simpa only [mul_one, nsmul_eq_mul]
+end
+
 lemma char_p.int_cast_eq_zero_iff (R : Type u) [ring R] (p : ℕ) [char_p R p] (a : ℤ) :
   (a : R) = 0 ↔ (p:ℤ) ∣ a :=
 begin
@@ -317,3 +326,38 @@ lemma nontrivial_of_char_ne_one {v : ℕ} (hv : v ≠ 1) {R : Type*} [semiring R
 end char_one
 
 end char_p
+
+section
+
+variables (n : ℕ) (R : Type*) [comm_ring R] [fintype R]
+
+lemma char_p_of_ne_zero (hn : fintype.card R = n) (hR : ∀ i < n, (i : R) = 0 → i = 0) :
+  char_p R n :=
+{ cast_eq_zero_iff :=
+  begin
+    have H : (n : R) = 0, by { rw [← hn, char_p.cast_card_eq_zero] },
+    intro k,
+    split,
+    { intro h,
+      rw [← nat.mod_add_div k n, nat.cast_add, nat.cast_mul, H, zero_mul, add_zero] at h,
+      rw nat.dvd_iff_mod_eq_zero,
+      apply hR _ (nat.mod_lt _ _) h,
+      rw [← hn, gt, fintype.card_pos_iff],
+      exact ⟨0⟩, },
+    { rintro ⟨k, rfl⟩, rw [nat.cast_mul, H, zero_mul] }
+  end }
+
+lemma char_p_of_prime_pow_injective (p : ℕ) [hp : fact p.prime] (n : ℕ) (hn : fintype.card R = p ^ n)
+  (hR : ∀ i ≤ n, (p ^ i : R) = 0 → i = n) :
+  char_p R (p ^ n) :=
+begin
+  obtain ⟨c, hc⟩ := char_p.exists R, resetI,
+  have hcpn : c ∣ p ^ n,
+  { rw [← char_p.cast_eq_zero_iff R c, ← hn, char_p.cast_card_eq_zero], },
+  obtain ⟨i, hi, hc⟩ : ∃ i ≤ n, c = p ^ i, by rwa nat.dvd_prime_pow hp at hcpn,
+  obtain rfl : i = n,
+  { apply hR i hi, rw [← nat.cast_pow, ← hc, char_p.cast_eq_zero] },
+  rwa ← hc
+end
+
+end

src/data/equiv/ring.lean

@@ -53,6 +53,16 @@ instance : has_coe_to_fun (R ≃+* S) := ⟨_, ring_equiv.to_fun⟩
 
 @[simp] lemma to_fun_eq_coe_fun (f : R ≃+* S) : f.to_fun = f := rfl
 
+/-- Two ring isomorphisms agree if they are defined by the
+    same underlying function. -/
+@[ext] lemma ext {f g : R ≃+* S} (h : ∀ x, f x = g x) : f = g :=
+begin
+  have h₁ : f.to_equiv = g.to_equiv := equiv.ext h,
+  cases f, cases g, congr,
+  { exact (funext h) },
+  { exact congr_arg equiv.inv_fun h₁ }
+end
+
 instance has_coe_to_mul_equiv : has_coe (R ≃+* S) (R ≃* S) := ⟨ring_equiv.to_mul_equiv⟩
 
 instance has_coe_to_add_equiv : has_coe (R ≃+* S) (R ≃+ S) := ⟨ring_equiv.to_add_equiv⟩
@@ -174,6 +184,10 @@ instance has_coe_to_ring_hom : has_coe (R ≃+* S) (R →+* S) := ⟨ring_equiv.
 @[norm_cast] lemma coe_ring_hom (f : R ≃+* S) (a : R) :
   (f : R →+* S) a = f a := rfl
 
+lemma coe_ring_hom_inj_iff {R S : Type*} [semiring R] [semiring S] (f g : R ≃+* S) :
+  f = g ↔ (f : R →+* S) = g :=
+⟨congr_arg _, λ h, ext $ ring_hom.ext_iff.mp h⟩
+
 /-- Reinterpret a ring equivalence as a monoid homomorphism. -/
 abbreviation to_monoid_hom (e : R ≃+* S) : R →* S := e.to_ring_hom.to_monoid_hom
 
@@ -239,16 +253,6 @@ namespace ring_equiv
 
 variables [has_add R] [has_add S] [has_mul R] [has_mul S]
 
-/-- Two ring isomorphisms agree if they are defined by the
-    same underlying function. -/
-@[ext] lemma ext {f g : R ≃+* S} (h : ∀ x, f x = g x) : f = g :=
-begin
-  have h₁ : f.to_equiv = g.to_equiv := equiv.ext h,
-  cases f, cases g, congr,
-  { exact (funext h) },
-  { exact congr_arg equiv.inv_fun h₁ }
-end
-
 @[simp] theorem trans_symm (e : R ≃+* S) : e.trans e.symm = ring_equiv.refl R := ext e.3
 @[simp] theorem symm_trans (e : R ≃+* S) : e.symm.trans e = ring_equiv.refl S := ext e.4
 

src/data/fintype/basic.lean

@@ -267,6 +267,10 @@ end set
 lemma finset.card_univ [fintype α] : (finset.univ : finset α).card = fintype.card α :=
 rfl
 
+lemma finset.eq_univ_of_card [fintype α] (s : finset α) (hs : s.card = fintype.card α) :
+  s = univ :=
+eq_of_subset_of_card_le (subset_univ _) $ by rw [hs, finset.card_univ]
+
 lemma finset.card_le_univ [fintype α] (s : finset α) :
   s.card ≤ fintype.card α :=
 card_le_of_subset (subset_univ s)
@@ -430,75 +434,73 @@ instance (α : Type u) (β : Type v) [fintype α] [fintype β] : fintype (α ⊕
   ((equiv.sum_equiv_sigma_bool _ _).symm.trans
     (equiv.sum_congr equiv.ulift equiv.ulift))
 
-lemma fintype.card_le_of_injective [fintype α] [fintype β] (f : α → β)
-  (hf : function.injective f) : fintype.card α ≤ fintype.card β :=
+namespace fintype
+variables [fintype α] [fintype β]
+
+lemma card_le_of_injective (f : α → β) (hf : function.injective f) : card α ≤ card β :=
 finset.card_le_card_of_inj_on f (λ _ _, finset.mem_univ _) (λ _ _ _ _ h, hf h)
 
-lemma fintype.card_eq_one_iff [fintype α] : fintype.card α = 1 ↔ (∃ x : α, ∀ y, y = x) :=
-by rw [← fintype.card_unit, fintype.card_eq]; exact
+lemma card_eq_one_iff : card α = 1 ↔ (∃ x : α, ∀ y, y = x) :=
+by rw [← card_unit, card_eq]; exact
 ⟨λ ⟨a⟩, ⟨a.symm (), λ y, a.injective (subsingleton.elim _ _)⟩,
   λ ⟨x, hx⟩, ⟨⟨λ _, (), λ _, x, λ _, (hx _).trans (hx _).symm,
     λ _, subsingleton.elim _ _⟩⟩⟩
 
-lemma fintype.card_eq_zero_iff [fintype α] : fintype.card α = 0 ↔ (α → false) :=
-⟨λ h a, have e : α ≃ empty := classical.choice (fintype.card_eq.1 (by simp [h])), (e a).elim,
+lemma card_eq_zero_iff : card α = 0 ↔ (α → false) :=
+⟨λ h a, have e : α ≃ empty := classical.choice (card_eq.1 (by simp [h])), (e a).elim,
   λ h, have e : α ≃ empty := ⟨λ a, (h a).elim, λ a, a.elim, λ a, (h a).elim, λ a, a.elim⟩,
-    by simp [fintype.card_congr e]⟩
+    by simp [card_congr e]⟩
 
 /-- A `fintype` with cardinality zero is (constructively) equivalent to `pempty`. -/
-def fintype.card_eq_zero_equiv_equiv_pempty {α : Type v} [fintype α] :
-  fintype.card α = 0 ≃ (α ≃ pempty.{v+1}) :=
+def card_eq_zero_equiv_equiv_pempty :
+  card α = 0 ≃ (α ≃ pempty.{v+1}) :=
 { to_fun := λ h,
-  { to_fun := λ a, false.elim (fintype.card_eq_zero_iff.1 h a),
+  { to_fun := λ a, false.elim (card_eq_zero_iff.1 h a),
     inv_fun := λ a, pempty.elim a,
-    left_inv := λ a, false.elim (fintype.card_eq_zero_iff.1 h a),
+    left_inv := λ a, false.elim (card_eq_zero_iff.1 h a),
     right_inv := λ a, pempty.elim a, },
   inv_fun := λ e,
-  by { simp only [←fintype.of_equiv_card e], convert fintype.card_pempty, },
+  by { simp only [←of_equiv_card e], convert card_pempty, },
   left_inv := λ h, rfl,
   right_inv := λ e, by { ext x, cases e x, } }
 
-lemma fintype.card_pos_iff [fintype α] : 0 < fintype.card α ↔ nonempty α :=
+lemma card_pos_iff : 0 < card α ↔ nonempty α :=
 ⟨λ h, classical.by_contradiction (λ h₁,
-  have fintype.card α = 0 := fintype.card_eq_zero_iff.2 (λ a, h₁ ⟨a⟩),
+  have card α = 0 := card_eq_zero_iff.2 (λ a, h₁ ⟨a⟩),
   lt_irrefl 0 $ by rwa this at h),
-λ ⟨a⟩, nat.pos_of_ne_zero (mt fintype.card_eq_zero_iff.1 (λ h, h a))⟩
+λ ⟨a⟩, nat.pos_of_ne_zero (mt card_eq_zero_iff.1 (λ h, h a))⟩
 
-lemma fintype.card_le_one_iff [fintype α] : fintype.card α ≤ 1 ↔ (∀ a b : α, a = b) :=
-let n := fintype.card α in
-have hn : n = fintype.card α := rfl,
+lemma card_le_one_iff : card α ≤ 1 ↔ (∀ a b : α, a = b) :=
+let n := card α in
+have hn : n = card α := rfl,
 match n, hn with
-| 0 := λ ha, ⟨λ h, λ a, (fintype.card_eq_zero_iff.1 ha.symm a).elim, λ _, ha ▸ nat.le_succ _⟩
-| 1 := λ ha, ⟨λ h, λ a b, let ⟨x, hx⟩ := fintype.card_eq_one_iff.1 ha.symm in
+| 0 := λ ha, ⟨λ h, λ a, (card_eq_zero_iff.1 ha.symm a).elim, λ _, ha ▸ nat.le_succ _⟩
+| 1 := λ ha, ⟨λ h, λ a b, let ⟨x, hx⟩ := card_eq_one_iff.1 ha.symm in
   by rw [hx a, hx b],
     λ _, ha ▸ le_refl _⟩
 | (n+2) := λ ha, ⟨λ h, by rw ← ha at h; exact absurd h dec_trivial,
-  (λ h, fintype.card_unit ▸ fintype.card_le_of_injective (λ _, ())
+  (λ h, card_unit ▸ card_le_of_injective (λ _, ())
     (λ _ _ _, h _ _))⟩
 end
 
-lemma fintype.card_le_one_iff_subsingleton [fintype α] :
-  fintype.card α ≤ 1 ↔ subsingleton α :=
-iff.trans fintype.card_le_one_iff subsingleton_iff.symm
+lemma card_le_one_iff_subsingleton : card α ≤ 1 ↔ subsingleton α :=
+iff.trans card_le_one_iff subsingleton_iff.symm
 
-lemma fintype.one_lt_card_iff_nontrivial [fintype α] :
-  1 < fintype.card α ↔ nontrivial α :=
+lemma one_lt_card_iff_nontrivial : 1 < card α ↔ nontrivial α :=
 begin
   classical,
   rw ← not_iff_not,
   push_neg,
-  rw [not_nontrivial_iff_subsingleton, fintype.card_le_one_iff_subsingleton]
+  rw [not_nontrivial_iff_subsingleton, card_le_one_iff_subsingleton]
 end
 
-lemma fintype.exists_ne_of_one_lt_card [fintype α] (h : 1 < fintype.card α) (a : α) :
-  ∃ b : α, b ≠ a :=
-by { haveI : nontrivial α := fintype.one_lt_card_iff_nontrivial.1 h, exact exists_ne a }
+lemma exists_ne_of_one_lt_card (h : 1 < card α) (a : α) : ∃ b : α, b ≠ a :=
+by { haveI : nontrivial α := one_lt_card_iff_nontrivial.1 h, exact exists_ne a }
 
-lemma fintype.exists_pair_of_one_lt_card [fintype α] (h : 1 < fintype.card α) :
-  ∃ (a b : α), a ≠ b :=
-by { haveI : nontrivial α := fintype.one_lt_card_iff_nontrivial.1 h, exact exists_pair_ne α }
+lemma exists_pair_of_one_lt_card (h : 1 < card α) : ∃ (a b : α), a ≠ b :=
+by { haveI : nontrivial α := one_lt_card_iff_nontrivial.1 h, exact exists_pair_ne α }
 
-lemma fintype.injective_iff_surjective [fintype α] {f : α → α} : injective f ↔ surjective f :=
+lemma injective_iff_surjective {f : α → α} : injective f ↔ surjective f :=
 by haveI := classical.prop_decidable; exact
 have ∀ {f : α → α}, injective f → surjective f,
 from λ f hinj x,
@@ -511,20 +513,58 @@ from λ f hinj x,
     ⟨surj_inv hsurj, left_inverse_of_surjective_of_right_inverse
       (this (injective_surj_inv _)) (right_inverse_surj_inv _)⟩⟩
 
-lemma fintype.injective_iff_bijective [fintype α] {f : α → α} : injective f ↔ bijective f :=
-by simp [bijective, fintype.injective_iff_surjective]
+lemma injective_iff_bijective {f : α → α} : injective f ↔ bijective f :=
+by simp [bijective, injective_iff_surjective]
 
-lemma fintype.surjective_iff_bijective [fintype α] {f : α → α} : surjective f ↔ bijective f :=
-by simp [bijective, fintype.injective_iff_surjective]
+lemma surjective_iff_bijective {f : α → α} : surjective f ↔ bijective f :=
+by simp [bijective, injective_iff_surjective]
 
-lemma fintype.injective_iff_surjective_of_equiv [fintype α] {f : α → β} (e : α ≃ β) :
+lemma injective_iff_surjective_of_equiv {β : Type*} {f : α → β} (e : α ≃ β) :
   injective f ↔ surjective f :=
-have injective (e.symm ∘ f) ↔ surjective (e.symm ∘ f), from fintype.injective_iff_surjective,
+have injective (e.symm ∘ f) ↔ surjective (e.symm ∘ f), from injective_iff_surjective,
 ⟨λ hinj, by simpa [function.comp] using
   e.surjective.comp (this.1 (e.symm.injective.comp hinj)),
 λ hsurj, by simpa [function.comp] using
   e.injective.comp (this.2 (e.symm.surjective.comp hsurj))⟩
 
+lemma nonempty_equiv_of_card_eq (h : card α = card β) :
+  nonempty (α ≃ β) :=
+begin
+  obtain ⟨m, ⟨f⟩⟩ := exists_equiv_fin α,
+  obtain ⟨n, ⟨g⟩⟩ := exists_equiv_fin β,
+  suffices : m = n,
+  { subst this, exact ⟨f.trans g.symm⟩ },
+  calc m = card (fin m) : (card_fin m).symm
+     ... = card α       : card_congr f.symm
+     ... = card β       : h
+     ... = card (fin n) : card_congr g
+     ... = n            : card_fin n
+end
+
+lemma bijective_iff_injective_and_card (f : α → β) :
+  bijective f ↔ injective f ∧ card α = card β :=
+begin
+  split,
+  { intro h, exact ⟨h.1, card_congr (equiv.of_bijective f h)⟩ },
+  { rintro ⟨hf, h⟩,
+    refine ⟨hf, _⟩,
+    obtain ⟨e⟩ : nonempty (α ≃ β) := nonempty_equiv_of_card_eq h,
+    rwa ← injective_iff_surjective_of_equiv e }
+end
+
+lemma bijective_iff_surjective_and_card (f : α → β) :
+  bijective f ↔ surjective f ∧ card α = card β :=
+begin
+  split,
+  { intro h, exact ⟨h.2, card_congr (equiv.of_bijective f h)⟩, },
+  { rintro ⟨hf, h⟩,
+    refine ⟨_, hf⟩,
+    obtain ⟨e⟩ : nonempty (α ≃ β) := nonempty_equiv_of_card_eq h,
+    rwa injective_iff_surjective_of_equiv e }
+end
+
+end fintype
+
 lemma fintype.coe_image_univ [fintype α] [decidable_eq β] {f : α → β} :
   ↑(finset.image f finset.univ) = set.range f :=
 by { ext x, simp }
@@ -940,7 +980,7 @@ section choose
 open fintype
 open equiv
 
-variables [decidable_eq α] [fintype α] (p : α → Prop) [decidable_pred p]
+variables [fintype α] (p : α → Prop) [decidable_pred p]
 
 def choose_x (hp : ∃! a : α, p a) : {a // p a} :=
 ⟨finset.choose p univ (by simp; exact hp), finset.choose_property _ _ _⟩
@@ -955,8 +995,8 @@ end choose
 section bijection_inverse
 open function
 
-variables [decidable_eq α] [fintype α]
-variables [decidable_eq β] [fintype β]
+variables [fintype α]
+variables [decidable_eq β]
 variables {f : α → β}
 
 /-- `

src/data/zmod/basic.lean

@@ -362,6 +362,35 @@ cast_nat_cast (dvd_refl _) k
 lemma cast_int_cast' (k : ℤ) : ((k : zmod n) : R) = k :=
 cast_int_cast (dvd_refl _) k
 
+variables (R)
+
+lemma cast_hom_injective : function.injective (zmod.cast_hom (dvd_refl n) R) :=
+begin
+  rw ring_hom.injective_iff,
+  intro x,
+  obtain ⟨k, rfl⟩ := zmod.int_cast_surjective x,
+  rw [ring_hom.map_int_cast, char_p.int_cast_eq_zero_iff R n, char_p.int_cast_eq_zero_iff (zmod n) n],
+  exact id
+end
+
+lemma cast_hom_bijective [fintype R] (h : fintype.card R = n) :
+  function.bijective (zmod.cast_hom (dvd_refl n) R) :=
+begin
+  haveI : fact (0 < n) :=
+  begin
+    rw [nat.pos_iff_ne_zero],
+    unfreezingI { rintro rfl },
+    exact fintype.card_eq_zero_iff.mp h 0
+  end,
+  rw [fintype.bijective_iff_injective_and_card, zmod.card, h, eq_self_iff_true, and_true],
+  apply zmod.cast_hom_injective
+end
+
+/-- The unique ring isomorphism between `zmod n` and a ring `R`
+of characteristic `n` and cardinality `n`. -/
+noncomputable def ring_equiv [fintype R] (h : fintype.card R = n) : zmod n ≃+* R :=
+ring_equiv.of_bijective _ (zmod.cast_hom_bijective R h)
+
 end char_eq
 
 end universal_property
@@ -771,20 +800,27 @@ begin
   rw φ.ext_int ψ,
 end
 
-instance zmod.subsingleton_ring_hom {n : ℕ} {R : Type*} [semiring R] :
-  subsingleton ((zmod n) →+* R) :=
+namespace zmod
+variables {n : ℕ} {R : Type*}
+
+instance subsingleton_ring_hom [semiring R] : subsingleton ((zmod n) →+* R) :=
 ⟨ring_hom.ext_zmod⟩
 
-lemma zmod.ring_hom_surjective {R : Type*} [comm_ring R] {n : ℕ} (f : R →+* (zmod n)) :
+instance subsingleton_ring_equiv [semiring R] : subsingleton (zmod n ≃+* R) :=
+⟨λ f g, by { rw ring_equiv.coe_ring_hom_inj_iff, apply ring_hom.ext_zmod _ _ }⟩
+
+lemma ring_hom_surjective [ring R] (f : R →+* (zmod n)) :
   function.surjective f :=
 begin
   intros k,
   rcases zmod.int_cast_surjective k with ⟨n, rfl⟩,
   refine ⟨n, f.map_int_cast n⟩
 end
 
-lemma zmod.ring_hom_eq_of_ker_eq {R : Type*} [comm_ring R] {n : ℕ} (f g : R →+* (zmod n))
+lemma ring_hom_eq_of_ker_eq [comm_ring R] (f g : R →+* (zmod n))
   (h : f.ker = g.ker) : f = g :=
 by rw [← f.lift_of_surjective_comp (zmod.ring_hom_surjective f) g (le_of_eq h),
       ring_hom.ext_zmod (f.lift_of_surjective _ _ _) (ring_hom.id _),
       ring_hom.id_comp]
+
+end zmod