feat(ring_theory/perfection): define characteristic predicate of perfection (#5386)

Name changes:
- `perfect_field` --> `perfect_ring` (generalization)
- `semiring.perfection` --> `ring.perfection`
- Original `ring.perfection` deleted.

Author: kckennylau

src/field_theory/perfect_closure.lean

@@ -18,65 +18,82 @@ open function
 
 section defs
 
-variables (K : Type u) [field K] (p : ℕ) [fact p.prime] [char_p K p]
+variables (R : Type u) [comm_semiring R] (p : ℕ) [fact p.prime] [char_p R p]
 
-/-- A perfect field is a field of characteristic p that has p-th root. -/
-class perfect_field (K : Type u) [field K] (p : ℕ) [fact p.prime] [char_p K p] : Type u :=
-(pth_root' : K → K)
-(frobenius_pth_root' : ∀ x, frobenius K p (pth_root' x) = x)
+/-- A perfect ring is a ring of characteristic p that has p-th root. -/
+class perfect_ring : Type u :=
+(pth_root' : R → R)
+(frobenius_pth_root' : ∀ x, frobenius R p (pth_root' x) = x)
+(pth_root_frobenius' : ∀ x, pth_root' (frobenius R p x) = x)
 
-/-- Frobenius automorphism of a perfect field. -/
-def frobenius_equiv [perfect_field K p] : K ≃+* K :=
-{ inv_fun := perfect_field.pth_root' p,
-  left_inv := λ x, frobenius_inj K p $ perfect_field.frobenius_pth_root' _,
-  right_inv := perfect_field.frobenius_pth_root',
-  .. frobenius K p }
+/-- Frobenius automorphism of a perfect ring. -/
+def frobenius_equiv [perfect_ring R p] : R ≃+* R :=
+{ inv_fun := perfect_ring.pth_root' p,
+  left_inv := perfect_ring.pth_root_frobenius',
+  right_inv := perfect_ring.frobenius_pth_root',
+  .. frobenius R p }
 
-/-- `p`-th root of a number in a `perfect_field` as a `ring_hom`. -/
-def pth_root [perfect_field K p] : K →+* K :=
-(frobenius_equiv K p).symm.to_ring_hom
+/-- `p`-th root of an element in a `perfect_ring` as a `ring_hom`. -/
+def pth_root [perfect_ring R p] : R →+* R :=
+(frobenius_equiv R p).symm
 
 end defs
 
 section
 
-variables {K : Type u} [field K] {L : Type v} [field L] (f : K →* L) (g : K →+* L)
-  {p : ℕ} [fact p.prime] [char_p K p] [perfect_field K p] [char_p L p] [perfect_field L p]
+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] [perfect_ring R p] [char_p S p] [perfect_ring S p]
 
-@[simp] lemma coe_frobenius_equiv : ⇑(frobenius_equiv K p) = frobenius K p := rfl
+@[simp] lemma coe_frobenius_equiv : ⇑(frobenius_equiv R p) = frobenius R p := rfl
 
-@[simp] lemma  coe_frobenius_equiv_symm : ⇑(frobenius_equiv K p).symm = pth_root K p := rfl
+@[simp] lemma coe_frobenius_equiv_symm : ⇑(frobenius_equiv R p).symm = pth_root R p := rfl
 
-@[simp] theorem frobenius_pth_root (x : K) : frobenius K p (pth_root K p x) = x :=
-(frobenius_equiv K p).apply_symm_apply x
+@[simp] theorem frobenius_pth_root (x : R) : frobenius R p (pth_root R p x) = x :=
+(frobenius_equiv R p).apply_symm_apply x
 
-@[simp] theorem pth_root_frobenius (x : K) : pth_root K p (frobenius K p x) = x :=
-(frobenius_equiv K p).symm_apply_apply x
+@[simp] theorem pth_root_pow_p (x : R) : pth_root R p x ^ p = x :=
+frobenius_pth_root x
 
-theorem left_inverse_pth_root_frobenius : left_inverse (pth_root K p) (frobenius K p) :=
+@[simp] theorem pth_root_frobenius (x : R) : pth_root R p (frobenius R p x) = x :=
+(frobenius_equiv R p).symm_apply_apply x
+
+@[simp] theorem pth_root_pow_p' (x : R) : pth_root R p (x ^ p) = x :=
+pth_root_frobenius x
+
+theorem left_inverse_pth_root_frobenius : left_inverse (pth_root R p) (frobenius R p) :=
 pth_root_frobenius
 
-theorem eq_pth_root_iff {x y : K} : x = pth_root K p y ↔ frobenius K p x = y :=
-(frobenius_equiv K p).to_equiv.eq_symm_apply
+theorem right_inverse_pth_root_frobenius : function.right_inverse (pth_root R p) (frobenius R p) :=
+frobenius_pth_root
+
+theorem commute_frobenius_pth_root : function.commute (frobenius R p) (pth_root R p) :=
+λ x, (frobenius_pth_root x).trans (pth_root_frobenius x).symm
 
-theorem pth_root_eq_iff {x y : K} : pth_root K p x = y ↔ x = frobenius K p y :=
-(frobenius_equiv K p).to_equiv.symm_apply_eq
+theorem eq_pth_root_iff {x y : R} : x = pth_root R p y ↔ frobenius R p x = y :=
+(frobenius_equiv R p).to_equiv.eq_symm_apply
 
-theorem monoid_hom.map_pth_root (x : K) : f (pth_root K p x) = pth_root L p (f x) :=
+theorem pth_root_eq_iff {x y : R} : pth_root R p x = y ↔ x = frobenius R p y :=
+(frobenius_equiv R p).to_equiv.symm_apply_eq
+
+theorem monoid_hom.map_pth_root (x : R) : f (pth_root R p x) = pth_root S p (f x) :=
 eq_pth_root_iff.2 $ by rw [← f.map_frobenius, frobenius_pth_root]
 
-theorem monoid_hom.map_iterate_pth_root (x : K) (n : ℕ) :
-  f (pth_root K p^[n] x) = (pth_root L p^[n] (f x)) :=
+theorem monoid_hom.map_iterate_pth_root (x : R) (n : ℕ) :
+  f (pth_root R p^[n] x) = (pth_root S p^[n] (f x)) :=
 semiconj.iterate_right f.map_pth_root n x
 
-theorem ring_hom.map_pth_root (x : K) :
-  g (pth_root K p x) = pth_root L p (g x) :=
+theorem ring_hom.map_pth_root (x : R) :
+  g (pth_root R p x) = pth_root S p (g x) :=
 g.to_monoid_hom.map_pth_root x
 
-theorem ring_hom.map_iterate_pth_root (x : K) (n : ℕ) :
-  g (pth_root K p^[n] x) = (pth_root L p^[n] (g x)) :=
+theorem ring_hom.map_iterate_pth_root (x : R) (n : ℕ) :
+  g (pth_root R p^[n] x) = (pth_root S p^[n] (g x)) :=
 g.to_monoid_hom.map_iterate_pth_root x n
 
+variables (p)
+lemma injective_pow_p {x y : R} (hxy : x ^ p = y ^ p) : x = y :=
+left_inverse_pth_root_frobenius.injective hxy
+
 end
 
 section
@@ -361,12 +378,14 @@ instance : field (perfect_closure K p) :=
   .. (infer_instance : comm_ring (perfect_closure K p)) }
 
 
-instance : perfect_field (perfect_closure K p) p :=
+instance : perfect_ring (perfect_closure K p) p :=
 { pth_root' := λ e, lift_on e (λ x, mk K p (x.1 + 1, x.2)) (λ x y H,
     match x, y, H with
     | _, _, r.intro n x := quot.sound (r.intro _ _)
     end),
   frobenius_pth_root' := λ e, induction_on e (λ ⟨n, x⟩,
+    by { simp only [lift_on_mk, frobenius_mk], exact (quot.sound $ r.intro _ _).symm }),
+  pth_root_frobenius' := λ e, induction_on e (λ ⟨n, x⟩,
     by { simp only [lift_on_mk, frobenius_mk], exact (quot.sound $ r.intro _ _).symm }) }
 
 theorem eq_pth_root (x : ℕ × K) :
@@ -377,9 +396,9 @@ begin
   rw [iterate_succ_apply', ← ih]; refl
 end
 
-/-- Given a field `K` of characteristic `p` and a perfect field `L` of the same characteristic,
+/-- Given a field `K` of characteristic `p` and a perfect ring `L` of the same characteristic,
 any homomorphism `K →+* L` can be lifted to `perfect_closure K p`. -/
-def lift (L : Type v) [field L] [char_p L p] [perfect_field L p] :
+def lift (L : Type v) [comm_semiring L] [char_p L p] [perfect_ring L p] :
   (K →+* L) ≃ (perfect_closure K p →+* L) :=
 begin
   have := left_inverse_pth_root_frobenius.iterate,

src/ring_theory/perfection.lean

@@ -36,27 +36,19 @@ def monoid.perfection (M : Type u₁) [comm_monoid M] (p : ℕ) : submonoid (ℕ
   one_mem' := λ n, one_pow _,
   mul_mem' := λ f g hf hg n, (mul_pow _ _ _).trans $ congr_arg2 _ (hf n) (hg n) }
 
-/-- The perfection of a semiring `R` with characteristic `p`,
+/-- The perfection of a ring `R` with characteristic `p`,
 defined to be the projective limit of `R` using the Frobenius maps `R → R`
 indexed by the natural numbers, implemented as `{ f : ℕ → R | ∀ n, f (n + 1) ^ p = f n }`. -/
-def semiring.perfection (R : Type u₁) [comm_semiring R]
+def ring.perfection (R : Type u₁) [comm_semiring R]
   (p : ℕ) [hp : fact p.prime] [char_p R p] :
   subsemiring (ℕ → R) :=
 { zero_mem' := λ n, zero_pow $ hp.pos,
   add_mem' := λ f g hf hg n, (frobenius_add R p _ _).trans $ congr_arg2 _ (hf n) (hg n),
   .. monoid.perfection R p }
 
-/-- The perfection of a ring `R` with characteristic `p`,
-defined to be the projective limit of `R` using the Frobenius maps `R → R`
-indexed by the natural numbers, implemented as `{ f : ℕ → R | ∀ n, f (n + 1) ^ p = f n }`. -/
-def ring.perfection (R : Type u₁) [comm_ring R] (p : ℕ) [hp : fact p.prime] [char_p R p] :
-  subring (ℕ → R) :=
-{ neg_mem' := λ f hf n, (frobenius_neg R p _).trans $ congr_arg _ (hf n),
-  .. semiring.perfection R p }
-
-namespace ring.perfection
+namespace perfection
 
-variables (R : Type u₁) [comm_ring R] (p : ℕ) [hp : fact p.prime] [char_p R p]
+variables (R : Type u₁) [comm_semiring R] (p : ℕ) [hp : fact p.prime] [char_p R p]
 include hp
 
 /-- The `n`-th coefficient of an element of the perfection. -/
@@ -84,6 +76,8 @@ def pth_root : ring.perfection R p →+* ring.perfection R p :=
 
 variables {R p}
 
+@[simp] lemma coeff_mk (f : ℕ → R) (hf) (n : ℕ) : coeff R p n ⟨f, hf⟩ = f n := rfl
+
 lemma coeff_pth_root (f : ring.perfection R p) (n : ℕ) :
   coeff R p n (pth_root R p f) = coeff R p (n + 1) f :=
 rfl
@@ -96,6 +90,14 @@ lemma coeff_frobenius (f : ring.perfection R p) (n : ℕ) :
   coeff R p (n + 1) (frobenius _ p f) = coeff R p n f :=
 by convert coeff_pow_p f n
 
+lemma 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.rec_on m rfl $ λ m ih, by erw [function.iterate_succ_apply', coeff_frobenius, ih]
+
+lemma coeff_iterate_frobenius' (f : ring.perfection R p) (n m : ℕ) (hmn : m ≤ n) :
+  coeff R p n (frobenius _ p ^[m] f) = coeff R p (n - m) f :=
+eq.symm $ (coeff_iterate_frobenius _ _ m).symm.trans $ (nat.sub_add_cancel hmn).symm ▸ rfl
+
 lemma pth_root_frobenius : (pth_root R p).comp (frobenius _ p) = ring_hom.id _ :=
 ring_hom.ext $ λ x, ext $ λ n,
 by rw [ring_hom.comp_apply, ring_hom.id_apply, coeff_pth_root, coeff_frobenius]
@@ -113,7 +115,106 @@ lemma coeff_ne_zero_of_le {f : ring.perfection R p} {m n : ℕ} (hfm : coeff R p
   (hmn : m ≤ n) : coeff R p n f ≠ 0 :=
 let ⟨k, hk⟩ := nat.exists_eq_add_of_le hmn in hk.symm ▸ coeff_add_ne_zero hfm k
 
-end ring.perfection
+variables (R p)
+
+instance perfect_ring : perfect_ring (ring.perfection R p) p :=
+{ pth_root' := pth_root R p,
+  frobenius_pth_root' := congr_fun $ congr_arg ring_hom.to_fun $ @frobenius_pth_root R _ p _ _,
+  pth_root_frobenius' := congr_fun $ congr_arg ring_hom.to_fun $ @pth_root_frobenius R _ p _ _ }
+
+instance ring (R : Type u₁) [comm_ring R] [char_p R p] : ring (ring.perfection R p) :=
+((ring.perfection R p).to_subring $ λ n, by simp_rw [← frobenius_def, pi.neg_apply,
+    pi.one_apply, ring_hom.map_neg, ring_hom.map_one]).to_ring
+
+instance comm_ring (R : Type u₁) [comm_ring R] [char_p R p] : comm_ring (ring.perfection R p) :=
+((ring.perfection R p).to_subring $ λ n, by simp_rw [← frobenius_def, pi.neg_apply,
+    pi.one_apply, ring_hom.map_neg, ring_hom.map_one]).to_comm_ring
+
+/-- 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] def lift (R : Type u₁) [comm_semiring R] [char_p R p] [perfect_ring R p]
+  (S : Type u₂) [comm_semiring S] [char_p S p] :
+  (R →+* S) ≃ (R →+* ring.perfection S p) :=
+{ to_fun := λ f,
+  { to_fun := λ r, ⟨λ n, f $ _root_.pth_root R p ^[n] r,
+      λ n, by rw [← f.map_pow, function.iterate_succ_apply', pth_root_pow_p]⟩,
+    map_one' := ext $ λ n, (congr_arg f $ ring_hom.iterate_map_one _ _).trans f.map_one,
+    map_mul' := λ x y, ext $ λ n, (congr_arg f $ ring_hom.iterate_map_mul _ _ _ _).trans $
+      f.map_mul _ _,
+    map_zero' := ext $ λ n, (congr_arg f $ ring_hom.iterate_map_zero _ _).trans f.map_zero,
+    map_add' := λ x y, ext $ λ n, (congr_arg f $ ring_hom.iterate_map_add _ _ _ _).trans $
+      f.map_add _ _ },
+  inv_fun := ring_hom.comp $ coeff S p 0,
+  left_inv := λ f, ring_hom.ext $ λ r, rfl,
+  right_inv := λ f, ring_hom.ext $ λ r, ext $ λ n,
+    show coeff S p 0 (f (_root_.pth_root R p ^[n] r)) = coeff S p n (f r),
+    by rw [← coeff_iterate_frobenius _ 0 n, zero_add, ← ring_hom.map_iterate_frobenius,
+      right_inverse_pth_root_frobenius.iterate] }
+
+end perfection
+
+/-- A perfection map to a ring of characteristic `p` is a map that is isomorphic
+to its perfection. -/
+@[nolint has_inhabited_instance] structure perfection_map (p : ℕ) [fact p.prime]
+  {R : Type u₁} [comm_semiring R] [char_p R p]
+  {P : Type u₂} [comm_semiring P] [char_p P p] [perfect_ring P p] (π : P →+* R) : Prop :=
+(injective : ∀ ⦃x y : P⦄, (∀ n, π (pth_root P p ^[n] x) = π (pth_root P p ^[n] y)) → x = y)
+(surjective : ∀ f : ℕ → R, (∀ n, f (n + 1) ^ p = f n) →
+  ∃ x : P, ∀ n, π (pth_root P p ^[n] x) = f n)
+
+namespace perfection_map
+
+variables {p : ℕ} [fact p.prime]
+variables {R : Type u₁} [comm_semiring R] [char_p R p]
+variables {P : Type u₂} [comm_semiring P] [char_p P p] [perfect_ring P p]
+
+/-- Create a `perfection_map` from an isomorphism to the perfection. -/
+@[simps] lemma mk' {f : P →+* R} (g : P ≃+* ring.perfection R p)
+  (hfg : perfection.lift p P R f = g) :
+  perfection_map p f :=
+{ injective := λ x y hxy, g.injective $ (ring_hom.ext_iff.1 hfg x).symm.trans $
+    eq.symm $ (ring_hom.ext_iff.1 hfg y).symm.trans $ perfection.ext $ λ n, (hxy n).symm,
+  surjective := λ y hy, let ⟨x, hx⟩ := g.surjective ⟨y, hy⟩ in
+    ⟨x, λ n, show perfection.coeff R p n (perfection.lift p P R f x) =
+        perfection.coeff R p n ⟨y, hy⟩,
+      by rw [hfg, ← coe_fn_coe_base, hx]⟩ }
+
+variables (p R P)
+
+/-- The canonical perfection map from the perfection of a ring. -/
+lemma of : perfection_map p (perfection.coeff R p 0) :=
+mk' (ring_equiv.refl _) $ (equiv.apply_eq_iff_eq_symm_apply _).2 rfl
+
+/-- For a perfect ring, it itself is the perfection. -/
+lemma id [perfect_ring R p] : perfection_map p (ring_hom.id R) :=
+{ injective := λ x y hxy, hxy 0,
+  surjective := λ f hf, ⟨f 0, λ n, show pth_root R p ^[n] (f 0) = f n,
+    from nat.rec_on n rfl $ λ n ih, injective_pow_p p $
+      by rw [function.iterate_succ_apply', pth_root_pow_p _, ih, hf]⟩ }
+
+variables {p R P}
+/-- A perfection map induces an isomorphism to the prefection. -/
+noncomputable def equiv {π : P →+* R} (m : perfection_map p π) : P ≃+* ring.perfection R p :=
+ring_equiv.of_bijective (perfection.lift p P R π)
+⟨λ x y hxy, m.injective $ λ n, (congr_arg (perfection.coeff R p n) hxy : _),
+λ f, let ⟨x, hx⟩ := m.surjective f.1 f.2 in ⟨x, perfection.ext $ hx⟩⟩
+
+variables (p 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 →+* P`,
+where `P` is any perfection of `S`. -/
+@[simps] noncomputable def lift [perfect_ring R p] (S : Type u₂) [comm_semiring S] [char_p S p]
+  (P : Type u₃) [comm_semiring P] [char_p P p] [perfect_ring P p]
+  (π : P →+* S) (m : perfection_map p π) :
+  (R →+* S) ≃ (R →+* P) :=
+{ to_fun := λ f, ring_hom.comp ↑m.equiv.symm $ perfection.lift p R S f,
+  inv_fun := λ f, (perfection.lift p R S).symm (ring_hom.comp ↑m.equiv f),
+  left_inv := λ f, (equiv.symm_apply_eq _).2 $ ring_hom.ext $ λ x,
+    by simp_rw [ring_hom.comp_apply, ring_equiv.coe_ring_hom, ring_equiv.apply_symm_apply],
+  right_inv := λ f, ring_hom.ext $ λ x, by simp_rw [equiv.apply_symm_apply,
+      ring_hom.comp_apply, ring_equiv.coe_ring_hom, ring_equiv.symm_apply_apply] }
+
+end perfection_map
 
 section perfectoid
 
@@ -239,10 +340,13 @@ ring.perfection (mod_p K v O hv p) p
 
 namespace pre_tilt
 
+instance : comm_ring (pre_tilt K v O hv p) :=
+perfection.comm_ring p _
+
 section classical
 local attribute [instance] classical.dec
 
-open ring.perfection
+open perfection
 
 /-- The valuation `Perfection(O/(p)) → ℝ≥0` as a function.
 Given `f ∈ Perfection(O/(p))`, if `f = 0` then output `0`;
@@ -287,8 +391,8 @@ lemma val_aux_mul (f g : pre_tilt K v O hv p) :
 begin
   by_cases hf : f = 0, { rw [hf, zero_mul, val_aux_zero, zero_mul] },
   by_cases hg : g = 0, { rw [hg, mul_zero, val_aux_zero, mul_zero] },
-  replace hf : ∃ n, coeff _ _ n f ≠ 0 := not_forall.1 (λ h, hf $ ring.perfection.ext h),
-  replace hg : ∃ n, coeff _ _ n g ≠ 0 := not_forall.1 (λ h, hg $ ring.perfection.ext h),
+  replace hf : ∃ n, coeff _ _ n f ≠ 0 := not_forall.1 (λ h, hf $ perfection.ext h),
+  replace hg : ∃ n, coeff _ _ n g ≠ 0 := not_forall.1 (λ h, hg $ perfection.ext h),
   obtain ⟨m, hm⟩ := hf, obtain ⟨n, hn⟩ := hg,
   replace hm := coeff_ne_zero_of_le hm (le_max_left m n),
   replace hn := coeff_ne_zero_of_le hn (le_max_right m n),
@@ -305,9 +409,9 @@ begin
   by_cases hf : f = 0, { rw [hf, zero_add, val_aux_zero, max_eq_right], exact zero_le _ },
   by_cases hg : g = 0, { rw [hg, add_zero, val_aux_zero, max_eq_left], exact zero_le _ },
   by_cases hfg : f + g = 0, { rw [hfg, val_aux_zero], exact zero_le _ },
-  replace hf : ∃ n, coeff _ _ n f ≠ 0 := not_forall.1 (λ h, hf $ ring.perfection.ext h),
-  replace hg : ∃ n, coeff _ _ n g ≠ 0 := not_forall.1 (λ h, hg $ ring.perfection.ext h),
-  replace hfg : ∃ n, coeff _ _ n (f + g) ≠ 0 := not_forall.1 (λ h, hfg $ ring.perfection.ext h),
+  replace hf : ∃ n, coeff _ _ n f ≠ 0 := not_forall.1 (λ h, hf $ perfection.ext h),
+  replace hg : ∃ n, coeff _ _ n g ≠ 0 := not_forall.1 (λ h, hg $ perfection.ext h),
+  replace hfg : ∃ n, coeff _ _ n (f + g) ≠ 0 := not_forall.1 (λ h, hfg $ perfection.ext h),
   obtain ⟨m, hm⟩ := hf, obtain ⟨n, hn⟩ := hg, obtain ⟨k, hk⟩ := hfg,
   replace hm := coeff_ne_zero_of_le hm (le_trans (le_max_left m n) (le_max_left _ k)),
   replace hn := coeff_ne_zero_of_le hn (le_trans (le_max_right m n) (le_max_left _ k)),
@@ -334,7 +438,7 @@ variables {K v O hv p}
 lemma map_eq_zero {f : pre_tilt K v O hv p} : val K v O hv p f = 0 ↔ f = 0 :=
 begin
   by_cases hf0 : f = 0, { rw hf0, exact iff_of_true (valuation.map_zero _) rfl },
-  obtain ⟨n, hn⟩ : ∃ n, coeff _ _ n f ≠ 0 := not_forall.1 (λ h, hf0 $ ring.perfection.ext h),
+  obtain ⟨n, hn⟩ : ∃ n, coeff _ _ n f ≠ 0 := not_forall.1 (λ h, hf0 $ perfection.ext h),
   show val_aux K v O hv p f = 0 ↔ f = 0, refine iff_of_false (λ hvf, hn _) hf0,
   rw val_aux_eq hn at hvf, replace hvf := nnreal.pow_eq_zero hvf, rwa mod_p.pre_val_eq_zero at hvf
 end