feat(RingTheory/Perfection): lemmas for frobeniusEquiv.symm (#26386)

This PR continues the work from #22330.

Original PR: #22330

Co-authored-by: pre-commit-ci-lite[bot] <117423508+pre-commit-ci-lite[bot]@users.noreply.github.com>
Co-authored-by: Jiedong Jiang <emailboxofjjd@163.com>
Co-authored-by: jjdishere <emailboxofjjd@163.com>

Author: jjdishere

Mathlib/FieldTheory/Perfect.lean

@@ -150,6 +150,18 @@ theorem frobeniusEquiv_symm_comp_frobenius :
     ((frobeniusEquiv R p).symm : R →+* R).comp (frobenius R p) = RingHom.id R := by
   ext; simp
 
+@[simp]
+theorem coe_frobenius_comp_coe_frobeniusEquiv_symm :
+    ⇑(frobenius R p) ∘ ⇑(frobeniusEquiv R p).symm = id := by
+  ext
+  simp
+
+@[simp]
+theorem coe_frobeniusEquiv_symm_comp_coe_frobenius :
+    ⇑(frobeniusEquiv R p).symm ∘ ⇑(frobenius R p) = id := by
+  ext
+  simp
+
 @[simp]
 theorem frobeniusEquiv_symm_pow_p (x : R) : ((frobeniusEquiv R p).symm x) ^ p = x :=
   frobenius_apply_frobeniusEquiv_symm R p x
@@ -161,6 +173,43 @@ theorem iterate_frobeniusEquiv_symm_pow_p_pow (x : R) (n : ℕ) :
   | zero => simp
   | succ n ih => simp [pow_succ, pow_mul, ih]
 
+section commute
+
+variable {R S : Type*} [CommSemiring R] [CommSemiring S] (p : ℕ)
+    [ExpChar R p] [PerfectRing R p] [ExpChar S p] [PerfectRing S p]
+
+/--
+The `(frobeniusEquiv R p).symm` version of `MonoidHom.map_frobenius`.
+`(frobeniusEquiv R p).symm` commute with any monoid homomorphisms.
+-/
+theorem MonoidHom.map_frobeniusEquiv_symm (f : R →* S) (x : R) :
+    f ((frobeniusEquiv R p).symm x) = (frobeniusEquiv S p).symm (f x) := by
+  apply_fun (frobeniusEquiv S p)
+  simp [← MonoidHom.map_frobenius]
+
+theorem RingHom.map_frobeniusEquiv_symm (f : R →+* S) (x : R) :
+    f ((frobeniusEquiv R p).symm x) = (frobeniusEquiv S p).symm (f x) := by
+  apply_fun (frobeniusEquiv S p)
+  simp [← RingHom.map_frobenius]
+
+theorem MonoidHom.map_iterate_frobeniusEquiv_symm (f : R →* S) (n : ℕ) (x : R) :
+    f (((frobeniusEquiv R p).symm ^[n]) x) = ((frobeniusEquiv S p).symm ^[n]) (f x) := by
+  apply_fun (frobeniusEquiv S p)^[n]
+  · simp only [coe_frobeniusEquiv, ← map_iterate_frobenius]
+    · rw [← Function.comp_apply (f := (⇑(frobenius R p))^[n]),
+          ← Function.comp_apply (f := (⇑(frobenius S p))^[n]),
+          ← Function.Commute.comp_iterate, ← Function.Commute.comp_iterate]
+      · simp
+      all_goals rw [← coe_frobeniusEquiv]; simp [Function.Commute, Function.Semiconj]
+  apply Function.Injective.iterate
+  simp
+
+theorem RingHom.map_iterate_frobeniusEquiv_symm (f : R →+* S) (n : ℕ) (x : R) :
+    f (((frobeniusEquiv R p).symm ^[n]) x) = ((frobeniusEquiv S p).symm ^[n]) (f x) :=
+  MonoidHom.map_iterate_frobeniusEquiv_symm p (f.toMonoidHom) n x
+
+end commute
+
 theorem injective_pow_p {x y : R} (h : x ^ p = y ^ p) : x = y := (frobeniusEquiv R p).injective h
 
 lemma polynomial_expand_eq (f : R[X]) :

Mathlib/RingTheory/Perfection.lean

@@ -106,19 +106,24 @@ variable {R p}
 @[simp]
 theorem coeff_mk (f : ℕ → R) (hf) (n : ℕ) : coeff R p n ⟨f, hf⟩ = f n := rfl
 
+@[simp]
 theorem coeff_pthRoot (f : Ring.Perfection R p) (n : ℕ) :
     coeff R p n (pthRoot R p f) = coeff R p (n + 1) f := rfl
 
+@[simp]
 theorem coeff_pow_p (f : Ring.Perfection R p) (n : ℕ) :
     coeff R p (n + 1) (f ^ p) = coeff R p n f := by rw [RingHom.map_pow]; exact f.2 n
 
+@[simp]
 theorem coeff_pow_p' (f : Ring.Perfection R p) (n : ℕ) : coeff R p (n + 1) f ^ p = coeff R p n f :=
   f.2 n
 
+@[simp]
 theorem coeff_frobenius (f : Ring.Perfection R p) (n : ℕ) :
     coeff R p (n + 1) (frobenius _ p f) = coeff R p n f := by apply coeff_pow_p f n
 
 -- `coeff_pow_p f n` also works but is slow!
+@[simp]
 theorem coeff_iterate_frobenius (f : Ring.Perfection R p) (n m : ℕ) :
     coeff R p (n + m) ((frobenius _ p)^[m] f) = coeff R p n f :=
   Nat.recOn m rfl fun m ih => by
@@ -128,10 +133,12 @@ theorem coeff_iterate_frobenius' (f : Ring.Perfection R p) (n m : ℕ) (hmn : m
     coeff R p n ((frobenius _ p)^[m] f) = coeff R p (n - m) f :=
   Eq.symm <| (coeff_iterate_frobenius _ _ m).symm.trans <| (tsub_add_cancel_of_le hmn).symm ▸ rfl
 
+@[simp]
 theorem pthRoot_frobenius : (pthRoot R p).comp (frobenius _ p) = RingHom.id _ :=
   RingHom.ext fun x =>
     ext fun n => by rw [RingHom.comp_apply, RingHom.id_apply, coeff_pthRoot, coeff_frobenius]
 
+@[simp]
 theorem frobenius_pthRoot : (frobenius _ p).comp (pthRoot R p) = RingHom.id _ :=
   RingHom.ext fun x =>
     ext fun n => by
@@ -149,14 +156,31 @@ theorem coeff_ne_zero_of_le {f : Ring.Perfection R p} {m n : ℕ} (hfm : coeff R
   let ⟨k, hk⟩ := Nat.exists_eq_add_of_le hmn
   hk.symm ▸ coeff_add_ne_zero hfm k
 
-variable (R p)
-
+variable (R p) in
 instance perfectRing : PerfectRing (Ring.Perfection R p) p where
   bijective_frobenius := Function.bijective_iff_has_inverse.mpr
     ⟨pthRoot R p,
      DFunLike.congr_fun <| @frobenius_pthRoot R _ p _ _,
      DFunLike.congr_fun <| @pthRoot_frobenius R _ p _ _⟩
 
+@[simp]
+theorem coeff_frobeniusEquiv_symm (f : Ring.Perfection R p) (n : ℕ) :
+    Perfection.coeff R p n ((frobeniusEquiv (Ring.Perfection R p) p).symm f) =
+    Perfection.coeff R p (n + 1) f := by
+  nth_rw 2 [← frobenius_apply_frobeniusEquiv_symm _ p f]
+  rw [coeff_frobenius]
+
+@[simp]
+theorem coeff_iterate_frobeniusEquiv_symm (f : Ring.Perfection R p) (n m : ℕ) :
+    Perfection.coeff _ p n ((frobeniusEquiv _ p).symm ^[m] f) =
+    Perfection.coeff _ p (n + m) f := by
+  induction m generalizing f n with
+  | zero => simp
+  | succ m ih =>
+    simp [ih, ← add_assoc]
+
+variable (R p)
+
 /-- Given rings `R` and `S` of characteristic `p`, with `R` being perfect,
 any homomorphism `R →+* S` can be lifted to a homomorphism `R →+* Perfection S p`. -/
 @[simps]
@@ -323,7 +347,7 @@ section ModP
 variable (O : Type u₂) [CommRing O] (p : ℕ)
 
 /-- `O/(p)` for `O`, ring of integers of `K`. -/
-def ModP :=
+abbrev ModP :=
   O ⧸ (Ideal.span {(p : O)} : Ideal O)
 
 namespace ModP
@@ -456,6 +480,37 @@ instance : CommRing (PreTilt O p) :=
 instance : CharP (PreTilt O p) p :=
   Perfection.charP (ModP O p) p
 
+instance : PerfectRing (PreTilt O p) p :=
+  Perfection.perfectRing (ModP O p) p
+
+section coeff
+
+@[simp]
+theorem coeff_frobenius (n : ℕ) (x : PreTilt O p) :
+    ((Perfection.coeff (ModP O p) p (n + 1)) (((frobenius (PreTilt O p) p)) x)) =
+    ((Perfection.coeff (ModP O p) p n) x):= by
+  simp [PreTilt]
+
+@[simp]
+theorem coeff_frobenius_pow (m n : ℕ) (x : PreTilt O p) :
+    ((Perfection.coeff (ModP O p) p (m + n)) (((frobenius (PreTilt O p) p) ^[n]) x)) =
+    ((Perfection.coeff (ModP O p) p m) x):= by
+  simp [PreTilt]
+
+@[simp]
+theorem coeff_frobeniusEquiv_symm (n : ℕ) (x : PreTilt O p) :
+    ((Perfection.coeff (ModP O p) p n) (((frobeniusEquiv (PreTilt O p) p).symm) x)) =
+    ((Perfection.coeff (ModP O p) p (n + 1)) x):= by
+  simp [PreTilt]
+
+@[simp]
+theorem coeff_iterate_frobeniusEquiv_symm (m n : ℕ) (x : PreTilt O p) :
+    ((Perfection.coeff (ModP O p) p m) (((frobeniusEquiv (PreTilt O p) p).symm ^[n]) x)) =
+    ((Perfection.coeff (ModP O p) p (m + n)) x):= by
+  simp [PreTilt]
+
+end coeff
+
 section Classical
 
 open Perfection

Mathlib/RingTheory/Perfectoid/Untilt.lean

@@ -149,6 +149,7 @@ def untilt : PreTilt O p →* O where
 The composition of the mod `p` map
 with the untilt function equals taking the zeroth component of the perfection.
 -/
+@[simp]
 theorem mk_untilt_eq_coeff_zero (x : PreTilt O p) :
     Ideal.Quotient.mk (Ideal.span {(p : O)}) (x.untilt) = coeff (ModP O p) p 0 x := by
   simp only [untilt]
@@ -160,10 +161,18 @@ The composition of the mod `p` map
 with the untilt function equals taking the zeroth component of the perfection.
 A variation of `PreTilt.mk_untilt_eq_coeff_zero`.
 -/
+@[simp]
 theorem mk_comp_untilt_eq_coeff_zero :
     Ideal.Quotient.mk (Ideal.span {(p : O)}) ∘ untilt = coeff (ModP O p) p 0 :=
   funext mk_untilt_eq_coeff_zero
 
+@[simp]
+theorem untilt_iterate_frobeniusEquiv_symm_pow (x : PreTilt O p) (n : ℕ) :
+    untilt (((frobeniusEquiv (PreTilt O p) p).symm ^[n]) x) ^ p ^ n = x.untilt := by
+  simp only [← map_pow]
+  congr
+  simp
+
 end IsAdicComplete
 
 end PreTilt