mathlib documentation

field_theory.perfect_closure

The perfect closure of a field

@[class]
structure perfect_field (K : Type u) [field K] (p : ) [fact (nat.prime p)] [char_p K p] :
Type u

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

Instances
def frobenius_equiv (K : Type u) [field K] (p : ) [fact (nat.prime p)] [char_p K p] [perfect_field K p] :
K ≃+* K

Frobenius automorphism of a perfect field.

Equations
def pth_root (K : Type u) [field K] (p : ) [fact (nat.prime p)] [char_p K p] [perfect_field K p] :
K →+* K

p-th root of a number in a perfect_field as a ring_hom.

Equations
@[simp]
theorem coe_frobenius_equiv {K : Type u} [field K] {p : } [fact (nat.prime p)] [char_p K p] [perfect_field K p] :

@[simp]
theorem coe_frobenius_equiv_symm {K : Type u} [field K] {p : } [fact (nat.prime p)] [char_p K p] [perfect_field K p] :

@[simp]
theorem frobenius_pth_root {K : Type u} [field K] {p : } [fact (nat.prime p)] [char_p K p] [perfect_field K p] (x : K) :
(frobenius K p) ((pth_root K p) x) = x

@[simp]
theorem pth_root_frobenius {K : Type u} [field K] {p : } [fact (nat.prime p)] [char_p K p] [perfect_field K p] (x : K) :
(pth_root K p) ((frobenius K p) x) = x

theorem eq_pth_root_iff {K : Type u} [field K] {p : } [fact (nat.prime p)] [char_p K p] [perfect_field K p] {x y : K} :
x = (pth_root K p) y (frobenius K p) x = y

theorem pth_root_eq_iff {K : Type u} [field K] {p : } [fact (nat.prime p)] [char_p K p] [perfect_field K p] {x y : K} :
(pth_root K p) x = y x = (frobenius K p) y

theorem monoid_hom.map_pth_root {K : Type u} [field K] {L : Type v} [field L] (f : K →* L) {p : } [fact (nat.prime p)] [char_p K p] [perfect_field K p] [char_p L p] [perfect_field L p] (x : K) :
f ((pth_root K p) x) = (pth_root L p) (f x)

theorem monoid_hom.map_iterate_pth_root {K : Type u} [field K] {L : Type v} [field L] (f : K →* L) {p : } [fact (nat.prime p)] [char_p K p] [perfect_field K p] [char_p L p] [perfect_field L p] (x : K) (n : ) :
f ((pth_root K p)^[n] x) = (pth_root L p)^[n] (f x)

theorem ring_hom.map_pth_root {K : Type u} [field K] {L : Type v} [field L] (g : K →+* L) {p : } [fact (nat.prime p)] [char_p K p] [perfect_field K p] [char_p L p] [perfect_field L p] (x : K) :
g ((pth_root K p) x) = (pth_root L p) (g x)

theorem ring_hom.map_iterate_pth_root {K : Type u} [field K] {L : Type v} [field L] (g : K →+* L) {p : } [fact (nat.prime p)] [char_p K p] [perfect_field K p] [char_p L p] [perfect_field L p] (x : K) (n : ) :
g ((pth_root K p)^[n] x) = (pth_root L p)^[n] (g 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.

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)

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] :

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) :
(∀ (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} :
(∀ (x : × K), q (perfect_closure.mk K p x))q x

@[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) :

@[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)

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

Equations
@[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) :

@[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) :

@[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) :
(frobenius K p)^[m] x = yperfect_closure.mk K p (n, x) = perfect_closure.mk K p (m + n, y)

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 : ) :

@[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) [integral_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

@[instance]
def perfect_closure.has_inv (K : Type u) [field K] (p : ) [fact (nat.prime p)] [char_p K p] :

Equations
@[instance]
def perfect_closure.perfect_field (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) [field L] [char_p L p] [perfect_field L p] :

Given a field K of characteristic p and a perfect field L of the same characteristic, any homomorphism K →+* L can be lifted to perfect_closure K p.

Equations