The perfect closure of a field
@[class]
- pth_root' : K → K
- frobenius_pth_root' : ∀ (x : K), ⇑(frobenius K p) (perfect_field.pth_root' p x) = x
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.
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
- pth_root K p = (frobenius_equiv K p).symm.to_ring_hom
@[simp]
theorem
coe_frobenius_equiv
{K : Type u}
[field K]
{p : ℕ}
[fact (nat.prime p)]
[char_p K p]
[perfect_field K p] :
⇑(frobenius_equiv K p) = ⇑(frobenius 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] :
theorem
left_inverse_pth_root_frobenius
{K : Type u}
[field K]
{p : ℕ}
[fact (nat.prime p)]
[char_p K p]
[perfect_field K p] :
function.left_inverse ⇑(pth_root K p) ⇑(frobenius K p)
- intro : ∀ (K : Type u) [_inst_1 : comm_ring K] (p : ℕ) [_inst_2 : fact (nat.prime p)] [_inst_3 : char_p K p] (n : ℕ) (x : K), perfect_closure.r K p (n, x) (n + 1, ⇑(frobenius K p) x)
perfect_closure K p is the quotient by this relation.
The perfect closure is the smallest extension that makes frobenius surjective.
Equations
- perfect_closure K p = quot (perfect_closure.r K p)
def
perfect_closure.mk
(K : Type u)
[comm_ring K]
(p : ℕ)
[fact (nat.prime p)]
[char_p K p] :
ℕ × K → perfect_closure K p
Constructor for perfect_closure.
Equations
- perfect_closure.mk K p x = quot.mk (perfect_closure.r K p) x
@[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 y → f x = f y) → L
Lift a function ℕ × K → L to a function on perfect_closure K p.
Equations
- x.lift_on f hf = quot.lift_on x f hf
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] :
has_mul (perfect_closure K p)
@[instance]
def
perfect_closure.comm_monoid
(K : Type u)
[comm_ring K]
(p : ℕ)
[fact (nat.prime p)]
[char_p K p] :
comm_monoid (perfect_closure K p)
Equations
- perfect_closure.comm_monoid K p = {mul := has_mul.mul infer_instance, mul_assoc := _, one := perfect_closure.mk K p (0, 1), one_mul := _, mul_one := _, mul_comm := _}
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] :
inhabited (perfect_closure K p)
Equations
- perfect_closure.inhabited K p = {default := 1}
@[instance]
def
perfect_closure.has_add
(K : Type u)
[comm_ring K]
(p : ℕ)
[fact (nat.prime p)]
[char_p K p] :
has_add (perfect_closure K p)
@[instance]
def
perfect_closure.has_neg
(K : Type u)
[comm_ring K]
(p : ℕ)
[fact (nat.prime p)]
[char_p K p] :
has_neg (perfect_closure K p)
Equations
- perfect_closure.has_neg K p = {neg := quot.lift (λ (x : ℕ × K), perfect_closure.mk K p (x.fst, -x.snd)) _}
@[instance]
def
perfect_closure.has_zero
(K : Type u)
[comm_ring K]
(p : ℕ)
[fact (nat.prime p)]
[char_p K p] :
has_zero (perfect_closure K p)
Equations
- perfect_closure.has_zero K p = {zero := perfect_closure.mk K p (0, 0)}
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
@[instance]
def
perfect_closure.comm_ring
(K : Type u)
[comm_ring K]
(p : ℕ)
[fact (nat.prime p)]
[char_p K p] :
comm_ring (perfect_closure K p)
Equations
- perfect_closure.comm_ring K p = {add := has_add.add infer_instance, add_assoc := _, zero := 0, zero_add := _, add_zero := _, neg := has_neg.neg infer_instance, add_left_neg := _, add_comm := _, mul := comm_monoid.mul infer_instance, mul_assoc := _, one := comm_monoid.one infer_instance, one_mul := _, mul_one := _, left_distrib := _, right_distrib := _, mul_comm := _}
@[instance]
def
perfect_closure.char_p
(K : Type u)
[comm_ring K]
(p : ℕ)
[fact (nat.prime p)]
[char_p K p] :
char_p (perfect_closure K p) p
Equations
- _ = _
theorem
perfect_closure.frobenius_mk
(K : Type u)
[comm_ring K]
(p : ℕ)
[fact (nat.prime p)]
[char_p K p]
(x : ℕ × K) :
⇑(frobenius (perfect_closure K p) p) (perfect_closure.mk K p x) = perfect_closure.mk K p (x.fst, x.snd ^ p)
def
perfect_closure.of
(K : Type u)
[comm_ring K]
(p : ℕ)
[fact (nat.prime p)]
[char_p K p] :
K →+* perfect_closure K p
Embedding of K into perfect_closure K p
Equations
- perfect_closure.of K p = {to_fun := λ (x : K), perfect_closure.mk K p (0, x), map_one' := _, map_mul' := _, map_zero' := _, map_add' := _}
theorem
perfect_closure.of_apply
(K : Type u)
[comm_ring K]
(p : ℕ)
[fact (nat.prime p)]
[char_p K p]
(x : K) :
⇑(perfect_closure.of K p) x = perfect_closure.mk K p (0, x)
@[instance]
def
perfect_closure.has_inv
(K : Type u)
[field K]
(p : ℕ)
[fact (nat.prime p)]
[char_p K p] :
has_inv (perfect_closure K p)
Equations
- perfect_closure.has_inv K p = {inv := quot.lift (λ (x : ℕ × K), quot.mk (perfect_closure.r K p) (x.fst, (x.snd)⁻¹)) _}
@[instance]
def
perfect_closure.field
(K : Type u)
[field K]
(p : ℕ)
[fact (nat.prime p)]
[char_p K p] :
field (perfect_closure K p)
Equations
- perfect_closure.field K p = {add := comm_ring.add infer_instance, add_assoc := _, zero := comm_ring.zero infer_instance, zero_add := _, add_zero := _, neg := comm_ring.neg infer_instance, add_left_neg := _, add_comm := _, mul := comm_ring.mul infer_instance, mul_assoc := _, one := comm_ring.one infer_instance, one_mul := _, mul_one := _, left_distrib := _, right_distrib := _, mul_comm := _, inv := has_inv.inv infer_instance, exists_pair_ne := _, mul_inv_cancel := _, inv_zero := _}
@[instance]
def
perfect_closure.perfect_field
(K : Type u)
[field K]
(p : ℕ)
[fact (nat.prime p)]
[char_p K p] :
perfect_field (perfect_closure K p) p
Equations
- perfect_closure.perfect_field K p = {pth_root' := λ (e : perfect_closure K p), e.lift_on (λ (x : ℕ × K), perfect_closure.mk K p (x.fst + 1, x.snd)) _, frobenius_pth_root' := _}
theorem
perfect_closure.eq_pth_root
(K : Type u)
[field K]
(p : ℕ)
[fact (nat.prime p)]
[char_p K p]
(x : ℕ × K) :
perfect_closure.mk K p x = ⇑(pth_root (perfect_closure K p) p)^[x.fst] (⇑(perfect_closure.of K p) x.snd)
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] :
(K →+* L) ≃ (perfect_closure K p →+* L)
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
- perfect_closure.lift K p L = {to_fun := λ (f : K →+* L), {to_fun := λ (e : perfect_closure K p), e.lift_on (λ (x : ℕ × K), ⇑(pth_root L p)^[x.fst] (⇑f x.snd)) _, map_one' := _, map_mul' := _, map_zero' := _, map_add' := _}, inv_fun := λ (f : perfect_closure K p →+* L), f.comp (perfect_closure.of K p), left_inv := _, right_inv := _}