feat(RingTheory): isomorphism between perfection of R and perfection of R/I (leanprover-community#36161)

We construct the following isomorphism:
```lean
def Perfection.quotientMulEquiv (p : ℕ) [Fact (Nat.Prime p)]
    {R : Type*} [CommRing R] (I : Ideal R) [CharP (R ⧸ I) p] [IsAdicComplete I R] :
    Perfection R p ≃* Perfection (R ⧸ I) p
```

I also removed simp lemmas which expose the raw definition and instead prioritised lemmas which talk about the intended constructors, i.e. for `x : Perfection R p` we don't want `x.1 n` and instead want `x.coeff R p n`, and when `M` is perfect then maps `M -> Perfection N p` is determined by the zeroth coefficients.

Author: kckennylau

Mathlib/LinearAlgebra/SModEq/Basic.lean

@@ -60,7 +60,7 @@ lemma of_toAddSubgroup_le {U : Submodule R M} {V : Submodule S M}
   simp only [SModEq, Submodule.Quotient.eq] at hxy ⊢
   exact h hxy
 
-@[refl]
+@[refl, simp]
 protected theorem refl (x : M) : x ≡ x [SMOD U] :=
   @rfl _ _
 

Mathlib/RingTheory/AdicCompletion/Algebra.lean

@@ -190,7 +190,7 @@ lemma evalOneₐ_surjective : Function.Surjective (evalOneₐ I) := by
 /-- `AdicCauchySequence I R` is an `R`-subalgebra of `ℕ → R`. -/
 def AdicCauchySequence.subalgebra : Subalgebra R (ℕ → R) :=
   Submodule.toSubalgebra (AdicCauchySequence.submodule I R)
-    (fun {m n} _ ↦ by simp; rfl)
+    (fun {m n} _ ↦ by simp)
     (fun x y hx hy {m n} hmn ↦ by
       simp only [Pi.mul_apply]
       exact SModEq.mul (hx hmn) (hy hmn))

Mathlib/RingTheory/Perfection.lean

@@ -126,6 +126,16 @@ theorem coeffMonoidHom_pow_p_pow (f : Perfection M p) (m n : ℕ) :
     coeffMonoidHom M p (m + n) (f ^ p ^ n) = coeffMonoidHom M p m f :=
   n.recOn (by simp) fun n ih ↦ by rw [pow_succ, pow_mul, Nat.add_succ, coeffMonoidHom_pow_p, ih]
 
+@[simp]
+theorem coeffMonoidHom_pow_p_pow' (f : Perfection M p) (m n : ℕ) :
+    coeffMonoidHom M p (m + n) f ^ p ^ n = coeffMonoidHom M p m f := by
+  rw [← map_pow, coeffMonoidHom_pow_p_pow]
+
+@[simp]
+theorem coeffMonoidHom_pow_p_pow_self (f : Perfection M p) (n : ℕ) :
+    coeffMonoidHom M p n f ^ p ^ n = coeffMonoidHom M p 0 f := by
+  rw [← coeffMonoidHom_pow_p_pow' _ 0 n, zero_add]
+
 theorem coeffMonoidHom_powMonoidHom (f : Perfection M p) (n : ℕ) :
     coeffMonoidHom M p (n + 1) (powMonoidHom p f) = coeffMonoidHom M p n f :=
   coeffMonoidHom_pow_p f n
@@ -141,7 +151,7 @@ theorem coeffMonoidHom_iterate_powMonoidHom' (f : Perfection M p) (n m : ℕ) (h
 
 /-- Given monoids `M` and `N`, with `M` being perfect,
 any homomorphism `M →+* N` can be lifted uniquely to a homomorphism `M →* Perfection N p`. -/
-@[simps]
+@[simps! symm_apply]
 noncomputable def liftMonoidHom (p : ℕ) (M : Type*) [CommMonoid M] [PerfectRing M p]
     (N : Type*) [CommMonoid N] : (M →* N) ≃* (M →* Perfection N p) where
   toFun f :=
@@ -159,8 +169,11 @@ noncomputable def liftMonoidHom (p : ℕ) (M : Type*) [CommMonoid M] [PerfectRin
     rw [← coeffMonoidHom_pow_p_pow _ 0 n, ← map_pow, powMulEquiv_symm_pow_p, zero_add]
   map_mul' _ _ := by ext; simp
 
+@[simp] lemma coeffMonoidHom_zero_liftMonoidHom
+    (p : ℕ) {M N : Type*} [CommMonoid M] [PerfectRing M p] [CommMonoid N] (e : M →* N) (x : M) :
+    coeffMonoidHom N p 0 (liftMonoidHom p M N e x) = e x := by simp [liftMonoidHom]
+
 /-- A monoid homomorphism `M →* N` induces `Perfection M p →* Perfection N p`. -/
-@[simps!]
 def mapMonoidHom (p : ℕ) {M N : Type*} [CommMonoid M] [CommMonoid N] (φ : M →* N) :
     Perfection M p →* Perfection N p where
   toFun f := ⟨fun n ↦ φ (f.coeffMonoidHom M p n), fun n ↦ by rw [← map_pow, coeffMonoidHom_pow_p']⟩
@@ -339,13 +352,12 @@ theorem hom_ext {R : Type u₁} [CommSemiring R] [CharP R p] [PerfectRing R p] {
 variable {R} {S : Type u₂} [CommSemiring S] [CharP S p]
 
 /-- A ring homomorphism `R →+* S` induces `Perfection R p →+* Perfection S p`. -/
-@[simps!]
 def map (φ : R →+* S) : Perfection R p →+* Perfection S p where
   __ := mapMonoidHom p (φ : R →* S)
   map_zero' := Subtype.ext <| funext fun _ => φ.map_zero
   map_add' _ _ := Subtype.ext <| funext fun _ => φ.map_add _ _
 
-theorem coeff_map (φ : R →+* S) (f : Perfection R p) (n : ℕ) :
+@[simp] theorem coeff_map (φ : R →+* S) (f : Perfection R p) (n : ℕ) :
     coeff S p n (map p φ f) = φ (coeff R p n f) := rfl
 
 end CommSemiring
@@ -371,6 +383,14 @@ instance : CommRing (Perfection R p) :=
 
 end CommRing
 
+section CommMonoid_CommRing
+
+@[simp] theorem coeff_mapMonoidHom {p : ℕ} [Fact p.Prime] {M N : Type*} [CommMonoid M] [CommRing N]
+    [CharP N p] (e : M →* N) (n : ℕ) (x : Perfection M p) :
+    coeff N p n (mapMonoidHom p e x) = e (coeffMonoidHom M p n x) := rfl
+
+end CommMonoid_CommRing
+
 end Perfection
 
 /-- A perfection map to a ring of characteristic `p` is a map that is isomorphic

Mathlib/RingTheory/Teichmuller.lean

@@ -100,7 +100,7 @@ limit of `p^n`-th powers of arbitrary lifts in `R` of the `n`-th component from
 The simp NF is `teichmuller₀`. -/
 noncomputable def teichmuller : Perfection (R ⧸ I) p →* R where
   toFun := teichmullerFun
-  map_one' := teichmullerFun_spec fun _ ↦ ⟨1, by simp; rfl⟩
+  map_one' := teichmullerFun_spec fun _ ↦ ⟨1, by simp⟩
   map_mul' x y := by
     refine teichmullerFun_spec fun n ↦ ?_
     refine ⟨(coeff _ p n x).out * (coeff _ p n y).out, by simp, ?_⟩
@@ -125,7 +125,7 @@ theorem teichmuller_spec {x : Perfection (R ⧸ I) p} {y : R}
 
 theorem teichmuller_zero : teichmuller p I 0 = 0 :=
   have : p ≠ 0 := Nat.Prime.ne_zero Fact.out
-  teichmuller_spec fun n ↦ ⟨0, by simp [zero_pow (pow_ne_zero n this)]; rfl⟩
+  teichmuller_spec fun n ↦ ⟨0, by simp [zero_pow (pow_ne_zero n this)]⟩
 
 variable (p I) in
 /-- `teichmuller` as a `MonoidWithZeroHom`. This is the simp NF. -/
@@ -158,12 +158,19 @@ theorem teichmuller₀_spec {x : Perfection (R ⧸ I) p} {y : R}
     teichmuller₀ p I x = y :=
   teichmullerFun_spec h
 
+@[simp] theorem teichmuller₀_mapMonoidHom_idealQuotientMk {x : Perfection R p} :
+    teichmuller₀ p I (mapMonoidHom p (Ideal.Quotient.mk I) x) = coeffMonoidHom R p 0 x :=
+  teichmuller₀_spec fun n ↦ ⟨coeffMonoidHom R p n x, by simp⟩
+
 theorem mk_teichmuller (x : Perfection (R ⧸ I) p) :
     Ideal.Quotient.mk I (teichmuller p I x) = coeff _ p 0 x := by
   have := teichmuller_sModEq <| Ideal.Quotient.mk_out <| coeff _ p 0 x
   simp_rw [zero_add, pow_one] at this
   simpa [SModEq.idealQuotientMk] using this
 
+@[simp] theorem mk_teichmuller₀ (x : Perfection (R ⧸ I) p) :
+    Ideal.Quotient.mk I (teichmuller₀ p I x) = coeff _ p 0 x := mk_teichmuller _
+
 variable (p I) in
 theorem mk_comp_teichmuller :
     (Ideal.Quotient.mk I : _ →* _).comp (teichmuller p I) =
@@ -181,4 +188,26 @@ theorem mk_comp_teichmuller' :
     Ideal.Quotient.mk I ∘ (teichmuller p I) = coeff (R ⧸ I) p 0 :=
   funext mk_teichmuller
 
+set_option backward.isDefEq.respectTransparency false in
+/-- If `R` is `I`-adically complete and `R ⧸ I` has characteristic `p`, then
+`Perfection R p` and `Perfection (R ⧸ I) p` are isomorphic as monoids.
+
+Note that `Perfection R p` is generally not a ring, and the forward map is induced by
+the quotient map, and the backwards map is constructed using the Teichmüller map. -/
+noncomputable def quotientMulEquiv (p : ℕ) [Fact p.Prime]
+    {R : Type*} [CommRing R] (I : Ideal R) [CharP (R ⧸ I) p] [IsAdicComplete I R] :
+    Perfection R p ≃* Perfection (R ⧸ I) p := MonoidHom.toMulEquiv
+  (mapMonoidHom _ <| Ideal.Quotient.mk I)
+  (liftMonoidHom p _ _ <| teichmuller p I)
+  ((liftMonoidHom p _ _).symm.injective <| by ext; simp)
+  ((liftMonoidHom p _ _).symm.injective <| by ext; simp)
+
+@[simp] theorem coeff_quotientMulEquiv (x : Perfection R p) (n : ℕ) :
+    coeff (R ⧸ I) p n (quotientMulEquiv p I x) = Ideal.Quotient.mk I (coeffMonoidHom R p n x) := rfl
+
+set_option backward.isDefEq.respectTransparency false in
+@[simp] theorem coeff_zero_symm_quotientMulEquiv (x : Perfection (R ⧸ I) p) :
+    coeffMonoidHom R p 0 (quotientMulEquiv p I |>.symm x) = teichmuller₀ p I x := by
+  simp [quotientMulEquiv]
+
 end Perfection