# mathlib3documentation

field_theory.perfect_closure

# The perfect closure of a field #

THIS FILE IS SYNCHRONIZED WITH MATHLIB4. Any changes to this file require a corresponding PR to mathlib4.

@[class]
structure perfect_ring (R : Type u) (p : ) [fact (nat.prime p)] [ p] :
• pth_root' : R R
• frobenius_pth_root' : (x : R), p) = x
• pth_root_frobenius' : (x : R), ( p) x) = x

A perfect ring is a ring of characteristic p that has p-th root.

Instances of this typeclass
Instances of other typeclasses for perfect_ring
• perfect_ring.has_sizeof_inst
def frobenius_equiv (R : Type u) (p : ) [fact (nat.prime p)] [ p] [ p] :
R ≃+* R

Frobenius automorphism of a perfect ring.

Equations
def pth_root (R : Type u) (p : ) [fact (nat.prime p)] [ p] [ p] :
R →+* R

p-th root of an element in a perfect_ring as a ring_hom.

Equations
@[simp]
theorem coe_frobenius_equiv {R : Type u} {p : } [fact (nat.prime p)] [ p] [ p] :
p) = p)
@[simp]
theorem coe_frobenius_equiv_symm {R : Type u} {p : } [fact (nat.prime p)] [ p] [ p] :
p).symm) = (pth_root R p)
@[simp]
theorem frobenius_pth_root {R : Type u} {p : } [fact (nat.prime p)] [ p] [ p] (x : R) :
p) ((pth_root R p) x) = x
@[simp]
theorem pth_root_pow_p {R : Type u} {p : } [fact (nat.prime p)] [ p] [ p] (x : R) :
(pth_root R p) x ^ p = x
@[simp]
theorem pth_root_frobenius {R : Type u} {p : } [fact (nat.prime p)] [ p] [ p] (x : R) :
(pth_root R p) ( p) x) = x
@[simp]
theorem pth_root_pow_p' {R : Type u} {p : } [fact (nat.prime p)] [ p] [ p] (x : R) :
(pth_root R p) (x ^ p) = x
theorem left_inverse_pth_root_frobenius {R : Type u} {p : } [fact (nat.prime p)] [ p] [ p] :
p)
theorem right_inverse_pth_root_frobenius {R : Type u} {p : } [fact (nat.prime p)] [ p] [ p] :
p)
theorem commute_frobenius_pth_root {R : Type u} {p : } [fact (nat.prime p)] [ p] [ p] :
theorem eq_pth_root_iff {R : Type u} {p : } [fact (nat.prime p)] [ p] [ p] {x y : R} :
x = (pth_root R p) y p) x = y
theorem pth_root_eq_iff {R : Type u} {p : } [fact (nat.prime p)] [ p] [ p] {x y : R} :
(pth_root R p) x = y x = p) y
theorem monoid_hom.map_pth_root {R : Type u} {S : Type v} (f : R →* S) {p : } [fact (nat.prime p)] [ p] [ p] [ p] [ p] (x : R) :
f ((pth_root R p) x) = (pth_root S p) (f x)
theorem monoid_hom.map_iterate_pth_root {R : Type u} {S : Type v} (f : R →* S) {p : } [fact (nat.prime p)] [ p] [ p] [ p] [ p] (x : R) (n : ) :
f ((pth_root R p)^[n] x) = (pth_root S p)^[n] (f x)
theorem ring_hom.map_pth_root {R : Type u} {S : Type v} (g : R →+* S) {p : } [fact (nat.prime p)] [ p] [ p] [ p] [ p] (x : R) :
g ((pth_root R p) x) = (pth_root S p) (g x)
theorem ring_hom.map_iterate_pth_root {R : Type u} {S : Type v} (g : R →+* S) {p : } [fact (nat.prime p)] [ p] [ p] [ p] [ p] (x : R) (n : ) :
g ((pth_root R p)^[n] x) = (pth_root S p)^[n] (g x)
theorem injective_pow_p {R : Type u} (p : ) [fact (nat.prime p)] [ p] [ p] {x y : R} (hxy : x ^ p = y ^ p) :
x = y
theorem perfect_closure.r_iff (K : Type u) [comm_ring K] (p : ) [fact (nat.prime p)] [ p] (ᾰ ᾰ_1 : × K) :
ᾰ_1 (n : ) (x : K), = (n, x) ᾰ_1 = (n + 1, p) x)
inductive perfect_closure.r (K : Type u) [comm_ring K] (p : ) [fact (nat.prime p)] [ p] :
× K × K Prop

perfect_closure K p is the quotient by this relation.

def perfect_closure (K : Type u) [comm_ring K] (p : ) [fact (nat.prime p)] [ p] :

The perfect closure is the smallest extension that makes frobenius surjective.

Equations
• = quot p)
Instances for perfect_closure
def perfect_closure.mk (K : Type u) [comm_ring K] (p : ) [fact (nat.prime p)] [ p] (x : × K) :

Constructor for perfect_closure.

Equations
• x = quot.mk p) x
@[simp]
theorem perfect_closure.quot_mk_eq_mk (K : Type u) [comm_ring K] (p : ) [fact (nat.prime p)] [ p] (x : × K) :
quot.mk p) x = x
def perfect_closure.lift_on {K : Type u} [comm_ring K] {p : } [fact (nat.prime p)] [ p] {L : Type u_1} (x : p) (f : × K L) (hf : (x y : × K), x y f x = f y) :
L

Lift a function ℕ × K → L to a function on perfect_closure K p.

Equations
@[simp]
theorem perfect_closure.lift_on_mk {K : Type u} [comm_ring K] {p : } [fact (nat.prime p)] [ p] {L : Type u_1} (f : × K L) (hf : (x y : × K), x y f x = f y) (x : × K) :
x).lift_on f hf = f x
theorem perfect_closure.induction_on {K : Type u} [comm_ring K] {p : } [fact (nat.prime p)] [ p] (x : p) {q : Prop} (h : (x : × K), q x)) :
q x
@[protected, instance]
def perfect_closure.has_mul (K : Type u) [comm_ring K] (p : ) [fact (nat.prime p)] [ p] :
Equations
@[simp]
theorem perfect_closure.mk_mul_mk (K : Type u) [comm_ring K] (p : ) [fact (nat.prime p)] [ p] (x y : × K) :
x * y = (x.fst + y.fst, p)^[y.fst] x.snd * p)^[x.fst] y.snd)
@[protected, instance]
def perfect_closure.comm_monoid (K : Type u) [comm_ring K] (p : ) [fact (nat.prime p)] [ p] :
Equations
theorem perfect_closure.one_def (K : Type u) [comm_ring K] (p : ) [fact (nat.prime p)] [ p] :
1 = (0, 1)
@[protected, instance]
def perfect_closure.inhabited (K : Type u) [comm_ring K] (p : ) [fact (nat.prime p)] [ p] :
Equations
@[protected, instance]
def perfect_closure.has_add (K : Type u) [comm_ring K] (p : ) [fact (nat.prime p)] [ p] :
Equations
@[simp]
theorem perfect_closure.mk_add_mk (K : Type u) [comm_ring K] (p : ) [fact (nat.prime p)] [ p] (x y : × K) :
x + y = (x.fst + y.fst, p)^[y.fst] x.snd + p)^[x.fst] y.snd)
@[protected, instance]
def perfect_closure.has_neg (K : Type u) [comm_ring K] (p : ) [fact (nat.prime p)] [ p] :
Equations
@[simp]
theorem perfect_closure.neg_mk (K : Type u) [comm_ring K] (p : ) [fact (nat.prime p)] [ p] (x : × K) :
- x = (x.fst, -x.snd)
@[protected, instance]
def perfect_closure.has_zero (K : Type u) [comm_ring K] (p : ) [fact (nat.prime p)] [ p] :
Equations
theorem perfect_closure.zero_def (K : Type u) [comm_ring K] (p : ) [fact (nat.prime p)] [ p] :
0 = (0, 0)
@[simp]
theorem perfect_closure.mk_zero_zero (K : Type u) [comm_ring K] (p : ) [fact (nat.prime p)] [ p] :
(0, 0) = 0
theorem perfect_closure.mk_zero (K : Type u) [comm_ring K] (p : ) [fact (nat.prime p)] [ p] (n : ) :
(n, 0) = 0
theorem perfect_closure.r.sound (K : Type u) [comm_ring K] (p : ) [fact (nat.prime p)] [ p] (m n : ) (x y : K) (H : p)^[m] x = y) :
(n, x) = (m + n, y)
@[protected, instance]
def perfect_closure.add_comm_group (K : Type u) [comm_ring K] (p : ) [fact (nat.prime p)] [ p] :
Equations
@[protected, instance]
def perfect_closure.comm_ring (K : Type u) [comm_ring K] (p : ) [fact (nat.prime p)] [ p] :
Equations
theorem perfect_closure.eq_iff' (K : Type u) [comm_ring K] (p : ) [fact (nat.prime p)] [ p] (x y : × K) :
x = y (z : ), p)^[y.fst + z] x.snd = p)^[x.fst + z] y.snd
theorem perfect_closure.nat_cast (K : Type u) [comm_ring K] (p : ) [fact (nat.prime p)] [ p] (n x : ) :
x = (n, x)
theorem perfect_closure.int_cast (K : Type u) [comm_ring K] (p : ) [fact (nat.prime p)] [ p] (x : ) :
x = (0, x)
theorem perfect_closure.nat_cast_eq_iff (K : Type u) [comm_ring K] (p : ) [fact (nat.prime p)] [ p] (x y : ) :
@[protected, instance]
def perfect_closure.char_p (K : Type u) [comm_ring K] (p : ) [fact (nat.prime p)] [ p] :
char_p p) p
theorem perfect_closure.frobenius_mk (K : Type u) [comm_ring K] (p : ) [fact (nat.prime p)] [ p] (x : × K) :
(frobenius p) p) x) = (x.fst, x.snd ^ p)
def perfect_closure.of (K : Type u) [comm_ring K] (p : ) [fact (nat.prime p)] [ p] :

Embedding of K into perfect_closure K p

Equations
theorem perfect_closure.of_apply (K : Type u) [comm_ring K] (p : ) [fact (nat.prime p)] [ p] (x : K) :
p) x = (0, x)
theorem perfect_closure.eq_iff (K : Type u) [comm_ring K] [is_domain K] (p : ) [fact (nat.prime p)] [ p] (x y : × K) :
quot.mk p) x = quot.mk p) y p)^[y.fst] x.snd = p)^[x.fst] y.snd
@[protected, instance]
def perfect_closure.has_inv (K : Type u) [field K] (p : ) [fact (nat.prime p)] [ p] :
Equations
@[protected, instance]
def perfect_closure.field (K : Type u) [field K] (p : ) [fact (nat.prime p)] [ p] :
Equations
@[protected, instance]
def perfect_closure.perfect_ring (K : Type u) [field K] (p : ) [fact (nat.prime p)] [ p] :
p
Equations
theorem perfect_closure.eq_pth_root (K : Type u) [field K] (p : ) [fact (nat.prime p)] [ p] (x : × K) :
x = (pth_root p) p)^[x.fst] ( p) x.snd)
def perfect_closure.lift (K : Type u) [field K] (p : ) [fact (nat.prime p)] [ p] (L : Type v) [ p] [ p] :
(K →+* L) p →+* L)

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.

Equations
noncomputable def perfect_ring.of_surjective (k : Type u_1) [comm_ring k] [is_reduced k] (p : ) [fact (nat.prime p)] [ p] (h : function.surjective p)) :
p

A reduced ring with prime characteristic and surjective frobenius map is perfect.

Equations