feat(RingTheory): generalise perfection to monoids (#31007)

1. We generalise `PerfectRing` to monoids (without changing the name).
2. We move `Submonoid.perfection` and `Ring.Perfection` to the already existing `Perfection` namespace, which solves the problem that `Ring.Perfection` and its lemmas `Perfection.xxx` are in different namespaces. Also, the monoid perfection and ring perfection have the same underlying set, so this unify the two approaches.
3. `Perfection.lift` is now generalised to monoids: `liftMonoidHom : (M →* N) ≃ (M →* Perfection N p)` where `M` is a perfect monoid.

Author: kckennylau

Mathlib/FieldTheory/Perfect.lean

@@ -43,12 +43,51 @@ open Function Polynomial
 
 NB: This is not related to the concept with the same name introduced by Bass (related to projective
 covers of modules). -/
-class PerfectRing (R : Type*) (p : ℕ) [CommSemiring R] [ExpChar R p] : Prop where
+class PerfectRing (R : Type*) (p : ℕ) [Pow R ℕ] : Prop where
   /-- A ring is perfect if the Frobenius map is bijective. -/
-  bijective_frobenius : Bijective <| frobenius R p
+  bijective_frobenius : Bijective fun x : R ↦ x ^ p
 
 section PerfectRing
 
+section Monoid
+variable (M : Type*) (p q : ℕ) [CommMonoid M] [PerfectRing M p] [PerfectRing M q]
+
+instance one : PerfectRing M 1 :=
+  ⟨by simpa using bijective_id⟩
+
+instance mul : PerfectRing M (p * q) :=
+  ⟨by simp_rw [pow_mul]; exact PerfectRing.bijective_frobenius.comp PerfectRing.bijective_frobenius⟩
+
+instance pow (n : ℕ) : PerfectRing M (p ^ n) :=
+  n.recOn (inferInstanceAs (PerfectRing M 1)) fun n _ ↦ inferInstanceAs (PerfectRing M (p ^ n * p))
+
+/-- The `p`-th power automorphism for a perfect monoid. -/
+@[simps! apply]
+noncomputable def powMulEquiv : M ≃* M :=
+  .ofBijective (powMonoidHom p) PerfectRing.bijective_frobenius
+
+@[simp]
+theorem powMulEquiv_symm_pow_p (x : M) : ((powMulEquiv M p).symm x) ^ p = x :=
+  (powMulEquiv M p).apply_symm_apply x
+
+@[simp] theorem powMulEquiv_one : powMulEquiv M 1 = .refl M :=
+  MulEquiv.ext pow_one
+
+theorem powMulEquiv_mul : powMulEquiv M (p * q) = (powMulEquiv M p).trans (powMulEquiv M q) :=
+  MulEquiv.ext fun x ↦ pow_mul x p q
+
+theorem powMulEquiv_mul' : powMulEquiv M (p * q) = (powMulEquiv M q).trans (powMulEquiv M p) :=
+  MulEquiv.ext fun x ↦ pow_mul' x p q
+
+theorem powMulEquiv_pow (n : ℕ) : powMulEquiv M (p ^ n) = powMulEquiv M p ^ n :=
+  n.recOn (powMulEquiv_one M) fun n ih ↦ by
+    rw [pow_succ (powMulEquiv M p), ← ih, MulAut.mul_def, ← powMulEquiv_mul]
+    congr
+    rw [pow_succ']
+
+end Monoid
+
+section CommSemiring
 variable (R : Type*) (p m n : ℕ) [CommSemiring R] [ExpChar R p]
 
 /-- For a reduced ring, surjectivity of the Frobenius map is a sufficient condition for perfection.
@@ -67,7 +106,7 @@ variable [PerfectRing R p]
 theorem bijective_frobenius : Bijective (frobenius R p) := PerfectRing.bijective_frobenius
 
 theorem bijective_iterateFrobenius : Bijective (iterateFrobenius R p n) :=
-  coe_iterateFrobenius R p n ▸ (bijective_frobenius R p).iterate n
+  PerfectRing.bijective_frobenius
 
 @[simp]
 theorem injective_frobenius : Injective (frobenius R p) := (bijective_frobenius R p).1
@@ -80,6 +119,9 @@ theorem surjective_frobenius : Surjective (frobenius R p) := (bijective_frobeniu
 noncomputable def frobeniusEquiv : R ≃+* R :=
   RingEquiv.ofBijective (frobenius R p) PerfectRing.bijective_frobenius
 
+@[simp] theorem powMulEquiv_eq_toMulEquiv_frobeniusEquiv :
+    powMulEquiv R p = (frobeniusEquiv R p).toMulEquiv := rfl
+
 @[simp]
 theorem coe_frobeniusEquiv : ⇑(frobeniusEquiv R p) = frobenius R p := rfl
 
@@ -235,6 +277,8 @@ instance instPerfectRingProd (S : Type*) [CommSemiring S] [ExpChar S p] [Perfect
     PerfectRing (R × S) p where
   bijective_frobenius := (bijective_frobenius R p).prodMap (bijective_frobenius S p)
 
+end CommSemiring
+
 end PerfectRing
 
 /-- A perfect field.

Mathlib/FieldTheory/PerfectClosure.lean

@@ -406,6 +406,7 @@ instance instReduced : IsReduced (PerfectClosure K p) where
 
 instance instPerfectRing : PerfectRing (PerfectClosure K p) p where
   bijective_frobenius := by
+    simp_rw [← frobenius_def]
     let f : PerfectClosure K p → PerfectClosure K p := fun e ↦
       liftOn e (fun x => mk K p (x.1 + 1, x.2)) fun x y H =>
       match x, y, H with