[Merged by Bors] - chore(algebra/char_p): refactor char_p

src/algebra/char_p.lean → src/algebra/char_p/basic.lean

@@ -25,7 +25,8 @@ 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 :=
+@[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),
@@ -68,7 +69,8 @@ classical.by_cases
         (nat.mod_lt x $ nat.pos_of_ne_zero $ not_of_not_imp $
           nat.find_spec (not_forall.1 H))
         (not_imp_of_and_not ⟨by rwa [← nat.mod_add_div x (nat.find (not_forall.1 H)),
-          nat.cast_add, nat.cast_mul, of_not_not (not_not_of_not_imp $ nat.find_spec (not_forall.1 H)),
+          nat.cast_add, nat.cast_mul, of_not_not (not_not_of_not_imp $ nat.find_spec
+            (not_forall.1 H)),
           zero_mul, add_zero] at H1, H2⟩)),
     λ H1, by rw [← nat.mul_div_cancel' H1, nat.cast_mul,
       of_not_not (not_not_of_not_imp $ nat.find_spec (not_forall.1 H)), zero_mul]⟩⟩⟩)
@@ -80,19 +82,35 @@ let ⟨c, H⟩ := char_p.exists α in ⟨c, H, λ y H2, char_p.eq α H2 H⟩
 noncomputable def ring_char (α : Type u) [semiring α] : ℕ :=
 classical.some (char_p.exists_unique α)
 
-theorem ring_char.spec (α : Type u) [semiring α] : ∀ x:ℕ, (x:α) = 0 ↔ ring_char α ∣ x :=
+namespace ring_char
+
+theorem spec (α : Type u) [semiring α] : ∀ x:ℕ, (x:α) = 0 ↔ ring_char α ∣ x :=
 by letI := (classical.some_spec (char_p.exists_unique α)).1;
 unfold ring_char; exact char_p.cast_eq_zero_iff α (ring_char α)
 
-theorem ring_char.eq (α : Type u) [semiring α] {p : ℕ} (C : char_p α p) : p = ring_char α :=
+theorem eq (α : Type u) [semiring α] {p : ℕ} (C : char_p α p) : p = ring_char α :=
 (classical.some_spec (char_p.exists_unique α)).2 p C
 
-theorem add_pow_char_of_commute (R : Type u) [ring R] {p : ℕ} [fact p.prime]
+instance char_p (R : Type u) [semiring R] : char_p R (ring_char R) :=
+⟨spec R⟩
+
+theorem of_eq {R : Type u} [semiring R] {p : ℕ} (h : ring_char R = p) : char_p R p :=
+h ▸ ring_char.char_p R
+
+theorem eq_iff {R : Type u} [semiring R] {p : ℕ} : ring_char R = p ↔ char_p R p :=
+⟨of_eq, eq.symm ∘ eq R⟩
+
+theorem dvd {R : Type u} [semiring R] {x : ℕ} (hx : (x : R) = 0) : ring_char R ∣ x :=
+(spec R x).1 hx
+
+end ring_char
+
+theorem add_pow_char_of_commute (R : Type u) [semiring R] {p : ℕ} [fact p.prime]
   [char_p R p] (x y : R) (h : commute x y) :
   (x + y)^p = x^p + y^p :=
 begin
   rw [commute.add_pow h, finset.sum_range_succ, nat.sub_self, pow_zero, nat.choose_self],
-  rw [nat.cast_one, mul_one, mul_one, add_right_inj],
+  rw [nat.cast_one, mul_one, mul_one], congr' 1,
   convert finset.sum_eq_single 0 _ _, { simp },
   swap, { intro h1, contrapose! h1, rw finset.mem_range, apply nat.prime.pos, assumption },
   intros b h1 h2,
@@ -102,7 +120,7 @@ begin
   rwa ← finset.mem_range
 end
 
-theorem add_pow_char_pow_of_commute (R : Type u) [ring R] {p : ℕ} [fact p.prime]
+theorem add_pow_char_pow_of_commute (R : Type u) [semiring R] {p : ℕ} [fact p.prime]
   [char_p R p] {n : ℕ} (x y : R) (h : commute x y) :
   (x + y) ^ (p ^ n) = x ^ (p ^ n) + y ^ (p ^ n) :=
 begin
@@ -128,11 +146,11 @@ begin
   apply sub_pow_char_of_commute, apply commute.pow_pow h,
 end
 
-theorem add_pow_char (α : Type u) [comm_ring α] {p : ℕ} [fact p.prime]
+theorem add_pow_char (α : Type u) [comm_semiring α] {p : ℕ} [fact p.prime]
   [char_p α p] (x y : α) : (x + y)^p = x^p + y^p :=
 add_pow_char_of_commute _ _ _ (commute.all _ _)
 
-theorem add_pow_char_pow (R : Type u) [comm_ring R] {p : ℕ} [fact p.prime]
+theorem add_pow_char_pow (R : Type u) [comm_semiring R] {p : ℕ} [fact p.prime]
   [char_p R p] {n : ℕ} (x y : R) :
   (x + y) ^ (p ^ n) = x ^ (p ^ n) + y ^ (p ^ n) :=
 add_pow_char_pow_of_commute _ _ _ (commute.all _ _)
@@ -173,7 +191,9 @@ end
 
 section frobenius
 
-variables (R : Type u) [comm_ring R] {S : Type v} [comm_ring S] (f : R →* S) (g : R →+* S)
+section comm_semiring
+
+variables (R : Type u) [comm_semiring R] {S : Type v} [comm_semiring S] (f : R →* S) (g : R →+* S)
   (p : ℕ) [fact p.prime] [char_p R p]  [char_p S p] (x y : R)
 
 /-- The frobenius map that sends x to x^p -/
@@ -230,12 +250,21 @@ theorem frobenius_zero : frobenius R p 0 = 0 := (frobenius R p).map_zero
 theorem frobenius_add : frobenius R p (x + y) = frobenius R p x + frobenius R p y :=
 (frobenius R p).map_add x y
 
+theorem frobenius_nat_cast (n : ℕ) : frobenius R p n = n := (frobenius R p).map_nat_cast n
+
+end comm_semiring
+
+section comm_ring
+
+variables (R : Type u) [comm_ring R] {S : Type v} [comm_ring S] (f : R →* S) (g : R →+* S)
+  (p : ℕ) [fact p.prime] [char_p R p]  [char_p S p] (x y : R)
+
 theorem frobenius_neg : frobenius R p (-x) = -frobenius R p x := (frobenius R p).map_neg x
 
 theorem frobenius_sub : frobenius R p (x - y) = frobenius R p x - frobenius R p y :=
 (frobenius R p).map_sub x y
 
-theorem frobenius_nat_cast (n : ℕ) : frobenius R p n = n := (frobenius R p).map_nat_cast n
+end comm_ring
 
 end frobenius
 

src/algebra/char_p/default.lean

@@ -0,0 +1,4 @@
+import algebra.char_p.basic
+import algebra.char_p.pi
+import algebra.char_p.quotient
+import algebra.char_p.subring

src/algebra/char_p/pi.lean

@@ -0,0 +1,30 @@
+/-
+Copyright (c) 2020 Kenny Lau. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+Authors: Kenny Lau
+-/
+
+import algebra.char_p.basic
+import algebra.ring.pi
+
+/-!
+# Characteristic of semirings of functions
+-/
+
+universes u v
+
+namespace char_p
+
+instance pi (ι : Type u) [hi : nonempty ι] (R : Type v) [semiring R] (p : ℕ) [char_p R p] :
+  char_p (ι → R) p :=
+⟨λ x, let ⟨i⟩ := hi in iff.symm $ (char_p.cast_eq_zero_iff R p x).symm.trans
+⟨λ h, funext $ λ j, show ring_hom.apply (λ _, R) j (↑x : ι → R) = 0,
+    by rw [ring_hom.map_nat_cast, h],
+  λ h, (ring_hom.apply (λ _, R) i).map_nat_cast x ▸ by rw [h, ring_hom.map_zero]⟩⟩
+
+-- diamonds
+instance pi' (ι : Type u) [hi : nonempty ι] (R : Type v) [comm_ring R] (p : ℕ) [char_p R p] :
+  char_p (ι → R) p :=
+char_p.pi ι R p
+
+end char_p

src/algebra/char_p/quotient.lean

@@ -0,0 +1,27 @@
+/-
+Copyright (c) 2020 Kenny Lau. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+Authors: Kenny Lau
+-/
+
+import algebra.char_p.basic
+import algebra.ring_quot
+
+/-!
+# Characteristic of quotients rings
+-/
+
+universes u v
+
+namespace char_p
+
+theorem quotient (R : Type u) [comm_ring R] (p : ℕ) [hp1 : fact p.prime] (hp2 : ↑p ∈ nonunits R) :
+  char_p (ideal.span {p} : ideal R).quotient p :=
+have hp0 : (p : (ideal.span {p} : ideal R).quotient) = 0,
+  from (ideal.quotient.mk (ideal.span {p} : ideal R)).map_nat_cast p ▸
+    ideal.quotient.eq_zero_iff_mem.2 (ideal.subset_span $ set.mem_singleton _),
+ring_char.of_eq $ or.resolve_left ((nat.dvd_prime hp1).1 $ ring_char.dvd hp0) $ λ h1,
+hp2 $ is_unit_iff_dvd_one.2 $ ideal.mem_span_singleton.1 $ ideal.quotient.eq_zero_iff_mem.1 $
+@@subsingleton.elim (@@char_p.subsingleton _ $ ring_char.of_eq h1) _ _
+
+end char_p

src/algebra/char_p/subring.lean

@@ -0,0 +1,34 @@
+/-
+Copyright (c) 2020 Kenny Lau. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+Authors: Kenny Lau
+-/
+
+import algebra.char_p.basic
+import ring_theory.subring
+
+/-!
+# Characteristic of subrings
+-/
+
+universes u v
+
+namespace char_p
+
+instance subsemiring (R : Type u) [semiring R] (p : ℕ) [char_p R p] (S : subsemiring R) :
+  char_p S p :=
+⟨λ x, iff.symm $ (char_p.cast_eq_zero_iff R p x).symm.trans
+⟨λ h, subtype.eq $ show S.subtype x = 0, by rw [ring_hom.map_nat_cast, h],
+  λ h, S.subtype.map_nat_cast x ▸ by rw [h, ring_hom.map_zero]⟩⟩
+
+instance subring (R : Type u) [ring R] (p : ℕ) [char_p R p] (S : subring R) :
+  char_p S p :=
+⟨λ x, iff.symm $ (char_p.cast_eq_zero_iff R p x).symm.trans
+⟨λ h, subtype.eq $ show S.subtype x = 0, by rw [ring_hom.map_nat_cast, h],
+  λ h, S.subtype.map_nat_cast x ▸ by rw [h, ring_hom.map_zero]⟩⟩
+
+instance subring' (R : Type u) [comm_ring R] (p : ℕ) [char_p R p] (S : subring R) :
+  char_p S p :=
+char_p.subring R p S
+
+end char_p

src/algebra/invertible.lean

@@ -7,7 +7,7 @@ A typeclass for the two-sided multiplicative inverse.
 -/
 
 import algebra.char_zero
-import algebra.char_p
+import algebra.char_p.basic
 
 /-!
 # Invertible elements

src/data/matrix/char_p.lean

@@ -4,7 +4,7 @@ Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Aaron Anderson
 -/
 import data.matrix.basic
-import algebra.char_p
+import algebra.char_p.basic
 /-!
 # Matrices in prime characteristic
 -/

src/data/zmod/basic.lean

@@ -5,7 +5,7 @@ Author: Chris Hughes
 -/
 
 import data.int.modeq
-import algebra.char_p
+import algebra.char_p.basic
 import data.nat.totient
 import ring_theory.ideal.operations
 

src/field_theory/mv_polynomial.lean

@@ -8,7 +8,7 @@ Multivariate functions of the form `α^n → α` are isomorphic to multivariate
 -/
 
 import linear_algebra.finsupp_vector_space
-import algebra.char_p
+import algebra.char_p.basic
 
 noncomputable theory
 

src/field_theory/perfect_closure.lean

@@ -3,7 +3,7 @@ Copyright (c) 2018 Kenny Lau. All rights reserved.
 Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Kenny Lau, Yury Kudryashov
 -/
-import algebra.char_p
+import algebra.char_p.basic
 import data.equiv.ring
 import algebra.group_with_zero.power
 import algebra.iterate_hom

src/representation_theory/maschke.lean

@@ -5,7 +5,7 @@ Author: Scott Morrison
 -/
 import algebra.monoid_algebra
 import algebra.invertible
-import algebra.char_p
+import algebra.char_p.basic
 import linear_algebra.basis
 
 /-!

src/ring_theory/polynomial/basic.lean

@@ -15,7 +15,7 @@ Authors: Kenny Lau
 * `polynomial.unique_factorization_monoid`:
   If an integral domain is a `unique_factorization_monoid`, then so is its polynomial ring.
 -/
-import algebra.char_p
+import algebra.char_p.basic
 import data.mv_polynomial.comm_ring
 import data.mv_polynomial.equiv
 import data.polynomial.field_division