mathlib documentation

field_theory.perfect_closure

The perfect closure of a field #

@[class]
structure perfect_ring (R : Type u) [comm_semiring R] (p : ) [fact (nat.prime p)] [char_p R p] :
Type u

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

Instances
def frobenius_equiv (R : Type u) [comm_semiring R] (p : ) [fact (nat.prime p)] [char_p R p] [perfect_ring R p] :
R ≃+* R

Frobenius automorphism of a perfect ring.

Equations
def pth_root (R : Type u) [comm_semiring R] (p : ) [fact (nat.prime p)] [char_p R p] [perfect_ring R 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} [comm_semiring R] {p : } [fact (nat.prime p)] [char_p R p] [perfect_ring R p] :
@[simp]
theorem coe_frobenius_equiv_symm {R : Type u} [comm_semiring R] {p : } [fact (nat.prime p)] [char_p R p] [perfect_ring R p] :
@[simp]
theorem frobenius_pth_root {R : Type u} [comm_semiring R] {p : } [fact (nat.prime p)] [char_p R p] [perfect_ring R p] (x : R) :
(frobenius R p) ((pth_root R p) x) = x
@[simp]
theorem pth_root_pow_p {R : Type u} [comm_semiring R] {p : } [fact (nat.prime p)] [char_p R p] [perfect_ring R p] (x : R) :
(pth_root R p) x ^ p = x
@[simp]
theorem pth_root_frobenius {R : Type u} [comm_semiring R] {p : } [fact (nat.prime p)] [char_p R p] [perfect_ring R p] (x : R) :
(pth_root R p) ((frobenius R p) x) = x
@[simp]
theorem pth_root_pow_p' {R : Type u} [comm_semiring R] {p : } [fact (nat.prime p)] [char_p R p] [perfect_ring R p] (x : R) :
(pth_root R p) (x ^ p) = x
theorem eq_pth_root_iff {R : Type u} [comm_semiring R] {p : } [fact (nat.prime p)] [char_p R p] [perfect_ring R p] {x y : R} :
x = (pth_root R p) y (frobenius R p) x = y
theorem pth_root_eq_iff {R : Type u} [comm_semiring R] {p : } [fact (nat.prime p)] [char_p R p] [perfect_ring R p] {x y : R} :
(pth_root R p) x = y x = (frobenius R p) y
theorem monoid_hom.map_pth_root {R : Type u} [comm_semiring R] {S : Type v} [comm_semiring S] (f : R →* S) {p : } [fact (nat.prime p)] [char_p R p] [perfect_ring R p] [char_p S p] [perfect_ring S 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} [comm_semiring R] {S : Type v} [comm_semiring S] (f : R →* S) {p : } [fact (nat.prime p)] [char_p R p] [perfect_ring R p] [char_p S p] [perfect_ring S 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} [comm_semiring R] {S : Type v} [comm_semiring S] (g : R →+* S) {p : } [fact (nat.prime p)] [char_p R p] [perfect_ring R p] [char_p S p] [perfect_ring S 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} [comm_semiring R] {S : Type v} [comm_semiring S] (g : R →+* S) {p : } [fact (nat.prime p)] [char_p R p] [perfect_ring R p] [char_p S p] [perfect_ring S 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} [comm_semiring R] (p : ) [fact (nat.prime p)] [char_p R p] [perfect_ring R 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)] [char_p K p] (ᾰ ᾰ_1 : × K) :
perfect_closure.r K p ᾰ_1 ∃ (n : ) (x : K), = (n, x) ᾰ_1 = (n + 1, (frobenius K p) x)
inductive perfect_closure.r (K : Type u) [comm_ring K] (p : ) [fact (nat.prime p)] [char_p K 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)] [char_p K p] :
Type u

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

Equations
def perfect_closure.mk (K : Type u) [comm_ring K] (p : ) [fact (nat.prime p)] [char_p K p] (x : × K) :

Constructor for perfect_closure.

Equations
@[simp]
theorem perfect_closure.quot_mk_eq_mk (K : Type u) [comm_ring K] (p : ) [fact (nat.prime p)] [char_p K p] (x : × K) :
quot.mk (perfect_closure.r K p) x = perfect_closure.mk K p x
def perfect_closure.lift_on {K : Type u} [comm_ring K] {p : } [fact (nat.prime p)] [char_p K p] {L : Type u_1} (x : perfect_closure K p) (f : × K → L) (hf : ∀ (x y : × K), perfect_closure.r K p x yf 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)] [char_p K p] {L : Type u_1} (f : × K → L) (hf : ∀ (x y : × K), perfect_closure.r K p x yf x = f y) (x : × K) :
(perfect_closure.mk K p x).lift_on f hf = f x
theorem perfect_closure.induction_on {K : Type u} [comm_ring K] {p : } [fact (nat.prime p)] [char_p K p] (x : perfect_closure K p) {q : perfect_closure K p → Prop} (h : ∀ (x : × K), q (perfect_closure.mk K p x)) :
q x
@[protected, instance]
def perfect_closure.has_mul (K : Type u) [comm_ring K] (p : ) [fact (nat.prime p)] [char_p K p] :
Equations
@[simp]
theorem perfect_closure.mk_mul_mk (K : Type u) [comm_ring K] (p : ) [fact (nat.prime p)] [char_p K p] (x y : × K) :
@[protected, instance]
def perfect_closure.comm_monoid (K : Type u) [comm_ring K] (p : ) [fact (nat.prime p)] [char_p K p] :
Equations
theorem perfect_closure.one_def (K : Type u) [comm_ring K] (p : ) [fact (nat.prime p)] [char_p K p] :
1 = perfect_closure.mk K p (0, 1)
@[protected, instance]
def perfect_closure.inhabited (K : Type u) [comm_ring K] (p : ) [fact (nat.prime p)] [char_p K p] :
Equations
@[protected, instance]
def perfect_closure.has_add (K : Type u) [comm_ring K] (p : ) [fact (nat.prime p)] [char_p K p] :
Equations
@[simp]
theorem perfect_closure.mk_add_mk (K : Type u) [comm_ring K] (p : ) [fact (nat.prime p)] [char_p K p] (x y : × K) :
@[protected, instance]
def perfect_closure.has_neg (K : Type u) [comm_ring K] (p : ) [fact (nat.prime p)] [char_p K p] :
Equations
@[simp]
theorem perfect_closure.neg_mk (K : Type u) [comm_ring K] (p : ) [fact (nat.prime p)] [char_p K p] (x : × K) :
@[protected, instance]
def perfect_closure.has_zero (K : Type u) [comm_ring K] (p : ) [fact (nat.prime p)] [char_p K p] :
Equations
theorem perfect_closure.zero_def (K : Type u) [comm_ring K] (p : ) [fact (nat.prime p)] [char_p K p] :
0 = perfect_closure.mk K p (0, 0)
theorem perfect_closure.mk_zero (K : Type u) [comm_ring K] (p : ) [fact (nat.prime p)] [char_p K p] (n : ) :
perfect_closure.mk K p (n, 0) = 0
theorem perfect_closure.r.sound (K : Type u) [comm_ring K] (p : ) [fact (nat.prime p)] [char_p K p] (m n : ) (x y : K) (H : (frobenius K p)^[m] x = y) :
perfect_closure.mk K p (n, x) = perfect_closure.mk K p (m + n, y)
@[protected, instance]
def perfect_closure.comm_ring (K : Type u) [comm_ring K] (p : ) [fact (nat.prime p)] [char_p K p] :
Equations
theorem perfect_closure.eq_iff' (K : Type u) [comm_ring K] (p : ) [fact (nat.prime p)] [char_p K p] (x y : × K) :
theorem perfect_closure.nat_cast (K : Type u) [comm_ring K] (p : ) [fact (nat.prime p)] [char_p K p] (n x : ) :
theorem perfect_closure.int_cast (K : Type u) [comm_ring K] (p : ) [fact (nat.prime p)] [char_p K p] (x : ) :
theorem perfect_closure.nat_cast_eq_iff (K : Type u) [comm_ring K] (p : ) [fact (nat.prime p)] [char_p K p] (x y : ) :
@[protected, instance]
def perfect_closure.char_p (K : Type u) [comm_ring K] (p : ) [fact (nat.prime p)] [char_p K p] :
theorem perfect_closure.frobenius_mk (K : Type u) [comm_ring K] (p : ) [fact (nat.prime p)] [char_p K p] (x : × K) :
def perfect_closure.of (K : Type u) [comm_ring K] (p : ) [fact (nat.prime p)] [char_p K 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)] [char_p K p] (x : K) :
theorem perfect_closure.eq_iff (K : Type u) [comm_ring K] [is_domain K] (p : ) [fact (nat.prime p)] [char_p K p] (x y : × K) :
quot.mk (perfect_closure.r K p) x = quot.mk (perfect_closure.r K p) y (frobenius K p)^[y.fst] x.snd = (frobenius K p)^[x.fst] y.snd
@[protected, instance]
def perfect_closure.has_inv (K : Type u) [field K] (p : ) [fact (nat.prime p)] [char_p K p] :
Equations
@[protected, instance]
def perfect_closure.perfect_ring (K : Type u) [field K] (p : ) [fact (nat.prime p)] [char_p K p] :
Equations
theorem perfect_closure.eq_pth_root (K : Type u) [field K] (p : ) [fact (nat.prime p)] [char_p K p] (x : × K) :
def perfect_closure.lift (K : Type u) [field K] (p : ) [fact (nat.prime p)] [char_p K p] (L : Type v) [comm_semiring L] [char_p L p] [perfect_ring L p] :

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)] [char_p k p] (h : function.surjective (frobenius k p)) :

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

Equations