refactor(field_theory/perfect_closure): use bundled homs, review (#2357)

* refactor(field_theory/perfect_closure): use bundled homs, review

Also add lemmas like `monoid_hom.iterate_map_mul`.

* Fix a typo spotted by `lint`

* Apply suggestions from code review

Co-Authored-By: Johan Commelin <johan@commelin.net>

Co-authored-by: Johan Commelin <johan@commelin.net>
Co-authored-by: mergify[bot] <37929162+mergify[bot]@users.noreply.github.com>

src/algebra/char_p.lean

@@ -71,43 +71,71 @@ begin
   rw [pow_zero, nat.sub_zero, one_mul, nat.choose_zero_right, nat.cast_one, mul_one]
 end
 
+section frobenius
+
+variables (R : Type u) [comm_ring R] {S : Type v} [comm_ring S] (f : R →* S) (g : R →+* S)
+  (p : ℕ) [nat.prime p] [char_p R p]  [char_p S p] (x y : R)
+
 /-- The frobenius map that sends x to x^p -/
-def frobenius (α : Type u) [monoid α] (p : ℕ) (x : α) : α := x^p
+def frobenius : R →+* R :=
+{ to_fun := λ x, x^p,
+  map_one' := one_pow p,
+  map_mul' := λ x y, mul_pow x y p,
+  map_zero' := zero_pow (lt_trans zero_lt_one ‹nat.prime p›.one_lt),
+  map_add' := add_pow_char R ‹nat.prime p› }
 
-theorem frobenius_def (α : Type u) [monoid α] (p : ℕ) (x : α) : frobenius α p x = x ^ p := rfl
+variable {R}
 
-theorem frobenius_mul (α : Type u) [comm_monoid α] (p : ℕ) (x y : α) :
-  frobenius α p (x * y) = frobenius α p x * frobenius α p y := mul_pow x y p
-theorem frobenius_one (α : Type u) [monoid α] (p : ℕ) :
-  frobenius α p 1 = 1 := one_pow _
+theorem frobenius_def : frobenius R p x = x ^ p := rfl
 
-theorem is_monoid_hom.map_frobenius {α : Type u} {β : Type v} [monoid α] [monoid β] (f : α → β) [is_monoid_hom f]
-  (p : ℕ) (x : α) : f (frobenius α p x) = frobenius β p (f x) :=
-by unfold frobenius; induction p; simp only [pow_zero, pow_succ,
-  is_monoid_hom.map_one f, is_monoid_hom.map_mul f, *]
+theorem frobenius_mul : frobenius R p (x * y) = frobenius R p x * frobenius R p y :=
+(frobenius R p).map_mul x y
 
-instance {α : Type u} [comm_ring α] (p : ℕ) [hp : nat.prime p] [char_p α p] : is_ring_hom (frobenius α p) :=
-{ map_one := frobenius_one α p,
-  map_mul := frobenius_mul α p,
-  map_add := add_pow_char α hp }
+theorem frobenius_one : frobenius R p 1 = 1 := one_pow _
 
-section
-variables (α : Type u) [comm_ring α] (p : ℕ) [hp : nat.prime p]
-theorem frobenius_zero : frobenius α p 0 = 0 := zero_pow hp.pos
-variables [char_p α p] (x y : α)
-include hp
-theorem frobenius_add : frobenius α p (x + y) = frobenius α p x + frobenius α p y := is_ring_hom.map_add _
-theorem frobenius_neg : frobenius α p (-x) = -frobenius α p x := is_ring_hom.map_neg _
-theorem frobenius_sub : frobenius α p (x - y) = frobenius α p x - frobenius α p y := is_ring_hom.map_sub _
-end
+variable {R}
+
+theorem monoid_hom.map_frobenius : f (frobenius R p x) = frobenius S p (f x) :=
+f.map_pow x p
+
+theorem ring_hom.map_frobenius : g (frobenius R p x) = frobenius S p (g x) :=
+g.map_pow x p
+
+theorem monoid_hom.map_iterate_frobenius (n : ℕ) :
+  f (frobenius R p^[n] x) = (frobenius S p^[n] (f x)) :=
+(nat.iterate₁ $ λ x, (f.map_frobenius p x).symm).symm
+
+theorem ring_hom.map_iterate_frobenius (n : ℕ) :
+  g (frobenius R p^[n] x) = (frobenius S p^[n] (g x)) :=
+g.to_monoid_hom.map_iterate_frobenius p x n
+
+theorem monoid_hom.iterate_map_frobenius (f : R →* R) (p : ℕ) [nat.prime p] [char_p R p] (n : ℕ) :
+  f^[n] (frobenius R p x) = frobenius R p (f^[n] x) :=
+f.iterate_map_pow _ _ _
+
+theorem ring_hom.iterate_map_frobenius (f : R →+* R) (p : ℕ) [nat.prime p] [char_p R p] (n : ℕ) :
+  f^[n] (frobenius R p x) = frobenius R p (f^[n] x) :=
+f.iterate_map_pow _ _ _
+
+variable (R)
+
+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_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
 
-theorem frobenius_inj (α : Type u) [integral_domain α] (p : ℕ) [nat.prime p] [char_p α p] (x y : α)
-  (H : frobenius α p x = frobenius α p y) : x = y :=
-by rw ← sub_eq_zero at H ⊢; rw ← frobenius_sub at H; exact pow_eq_zero H
+end frobenius
 
-theorem frobenius_nat_cast (α : Type u) [comm_ring α] (p : ℕ) [nat.prime p] [char_p α p] (x : ℕ) :
-  frobenius α p x = x :=
-by induction x; simp only [nat.cast_zero, nat.cast_succ, frobenius_zero, frobenius_one, frobenius_add, *]
+theorem frobenius_inj (α : Type u) [integral_domain α] (p : ℕ) [nat.prime p] [char_p α p] :
+  function.injective (frobenius α p) :=
+λ x h H, by { rw ← sub_eq_zero at H ⊢, rw ← frobenius_sub at H, exact pow_eq_zero H }
 
 namespace char_p
 

src/algebra/group_power.lean

@@ -135,9 +135,17 @@ theorem monoid_hom.map_pow (f : M →* N) (a : M) : ∀(n : ℕ), f (a ^ n) = (f
 | 0     := f.map_one
 | (n+1) := by rw [pow_succ, pow_succ, f.map_mul, monoid_hom.map_pow]
 
+theorem monoid_hom.iterate_map_pow (f : M →* M) (a) (n m : ℕ) : f^[n] (a^m) = (f^[n] a)^m :=
+show f^[n] ((λ x, x^m) a) = (λ x, x^m) (f^[n] a),
+from nat.iterate₁ $ λ x, f.map_pow x m
+
 theorem add_monoid_hom.map_smul (f : A →+ B) (a : A) (n : ℕ) : f (n • a) = n • f a :=
 f.to_multiplicative.map_pow a n
 
+theorem add_monoid_hom.iterate_map_smul (f : A →+ A) (a : A) (n m : ℕ) :
+  f^[n] (m • a) = m • (f^[n] a) :=
+f.to_multiplicative.iterate_map_pow a n m
+
 theorem is_monoid_hom.map_pow (f : M → N) [is_monoid_hom f] (a : M) :
   ∀(n : ℕ), f (a ^ n) = (f a) ^ n :=
 (monoid_hom.of f).map_pow a
@@ -397,10 +405,24 @@ by induction m with m ih; [exact int.coe_nat_one, rw [nat.pow_succ, pow_succ', i
 theorem int.nat_abs_pow (n : ℤ) (k : ℕ) : int.nat_abs (n ^ k) = (int.nat_abs n) ^ k :=
 by induction k with k ih; [refl, rw [pow_succ', int.nat_abs_mul, nat.pow_succ, ih]]
 
-@[simp] lemma ring_hom.map_pow [semiring R] [semiring S] (f : R →+* S) (a) :
+namespace ring_hom
+
+variables [semiring R] [semiring S]
+
+@[simp] lemma map_pow (f : R →+* S) (a) :
   ∀ n : ℕ, f (a ^ n) = (f a) ^ n :=
 f.to_monoid_hom.map_pow a
 
+variable (f : R →+* R)
+
+lemma iterate_map_pow (a) (n m : ℕ) : f^[n] (a^m) = (f^[n] a)^m :=
+f.to_monoid_hom.iterate_map_pow a n m
+
+lemma iterate_map_smul (a) (n m : ℕ) : f^[n] (m • a) = m • (f^[n] a) :=
+f.to_add_monoid_hom.iterate_map_smul a n m
+
+end ring_hom
+
 lemma is_semiring_hom.map_pow [semiring R] [semiring S] (f : R → S) [is_semiring_hom f] (a) :
   ∀ n : ℕ, f (a ^ n) = (f a) ^ n :=
 is_monoid_hom.map_pow f a

src/data/nat/basic.lean

@@ -1448,3 +1448,56 @@ by { rw [subsingleton.elim mn (le_trans (le_succ m) smn), decreasing_induction_t
          decreasing_induction_succ'] }
 
 end nat
+
+namespace monoid_hom
+
+variables {M : Type*} {G : Type*} [monoid M] [group G]
+
+@[simp, to_additive]
+theorem iterate_map_one (f : M →* M) (n : ℕ) : f^[n] 1 = 1 :=
+nat.iterate₀ f.map_one
+
+@[simp, to_additive]
+theorem iterate_map_mul (f : M →* M) (n : ℕ) (x y) :
+  f^[n] (x * y) = (f^[n] x) * (f^[n] y) :=
+nat.iterate₂ f.map_mul
+
+@[simp, to_additive]
+theorem iterate_map_inv (f : G →* G) (n : ℕ) (x) :
+  f^[n] (x⁻¹) = (f^[n] x)⁻¹ :=
+nat.iterate₁ f.map_inv
+
+@[simp]
+theorem iterate_map_sub {A : Type*} [add_group A] (f : A →+ A) (n : ℕ) (x y) :
+  f^[n] (x - y) = (f^[n] x) - (f^[n] y) :=
+nat.iterate₂ f.map_sub
+
+end monoid_hom
+
+namespace ring_hom
+
+variables {R : Type*} [semiring R] {S : Type*} [ring S]
+
+@[simp] theorem iterate_map_one (f : R →+* R) (n : ℕ) : f^[n] 1 = 1 :=
+nat.iterate₀ f.map_one
+
+@[simp] theorem iterate_map_zero (f : R →+* R) (n : ℕ) : f^[n] 0 = 0 :=
+nat.iterate₀ f.map_zero
+
+@[simp] theorem iterate_map_mul (f : R →+* R) (n : ℕ) (x y) :
+  f^[n] (x * y) = (f^[n] x) * (f^[n] y) :=
+nat.iterate₂ f.map_mul
+
+@[simp] theorem iterate_map_add (f : R →+* R) (n : ℕ) (x y) :
+  f^[n] (x + y) = (f^[n] x) + (f^[n] y) :=
+nat.iterate₂ f.map_add
+
+@[simp] theorem iterate_map_neg (f : S →+* S) (n : ℕ) (x) :
+  f^[n] (-x) = -(f^[n] x) :=
+nat.iterate₁ f.map_neg
+
+@[simp] theorem iterate_map_sub (f : S →+* S) (n : ℕ) (x y) :
+  f^[n] (x - y) = (f^[n] x) - (f^[n] y) :=
+nat.iterate₂ f.map_sub
+
+end ring_hom