field_theory.perfect_closure

source

@[class]

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

Type u

pth_root' : R → R
frobenius_pth_root' : ∀ (x : R), ⇑(frobenius R p) (perfect_ring.pth_root' p x) = x
pth_root_frobenius' : ∀ (x : R), perfect_ring.pth_root' p (⇑(frobenius R p) x) = x

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

Instances

source

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

frobenius_equiv R p = {to_fun := (frobenius R p).to_fun, inv_fun := perfect_ring.pth_root' p _inst_4, left_inv := _, right_inv := _, map_mul' := _, map_add' := _}

source

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

pth_root R p = ↑((frobenius_equiv R p).symm)

source

@[simp]

theorem coe_frobenius_equiv {R : Type u} [comm_semiring R] {p : ℕ} [fact (nat.prime p)] [char_p R p] [perfect_ring R p] :

⇑(frobenius_equiv R p) = ⇑(frobenius R p)

source

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

⇑((frobenius_equiv R p).symm) = ⇑(pth_root R p)

source

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

source

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

source

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

source

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

source

theorem left_inverse_pth_root_frobenius {R : Type u} [comm_semiring R] {p : ℕ} [fact (nat.prime p)] [char_p R p] [perfect_ring R p] :

function.left_inverse ⇑(pth_root R p) ⇑(frobenius R p)

source

theorem right_inverse_pth_root_frobenius {R : Type u} [comm_semiring R] {p : ℕ} [fact (nat.prime p)] [char_p R p] [perfect_ring R p] :

function.right_inverse ⇑(pth_root R p) ⇑(frobenius R p)

source

theorem commute_frobenius_pth_root {R : Type u} [comm_semiring R] {p : ℕ} [fact (nat.prime p)] [char_p R p] [perfect_ring R p] :

function.commute ⇑(frobenius R p) ⇑(pth_root R p)

source

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

source

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

source

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)

source

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)

source

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)

source

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)

source

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

source

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)

source

inductive perfect_closure.r (K : Type u) [comm_ring K] (p : ℕ) [fact (nat.prime p)] [char_p K p] :

ℕ × K → ℕ × K → Prop

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.

source

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

perfect_closure K p = quot (perfect_closure.r K p)

source

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

perfect_closure K p

Constructor for perfect_closure.

Equations

perfect_closure.mk K p x = quot.mk (perfect_closure.r K p) x

source

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

source

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

source

@[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 y → f x = f y) (x : ℕ × K) :

(perfect_closure.mk K p x).lift_on f hf = f x

source

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

source

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

Equations

perfect_closure.has_mul K p = {mul := quot.lift (λ (x : ℕ × K), quot.lift (λ (y : ℕ × K), perfect_closure.mk K p (x.fst + y.fst, (⇑(frobenius K p)^[y.fst ] x.snd) * ⇑(frobenius K p)^[x.fst ] y.snd)) _) _}

source

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

(perfect_closure.mk K p x) * perfect_closure.mk K p y = perfect_closure.mk K p (x.fst + y.fst, (⇑(frobenius K p)^[y.fst ] x.snd) * ⇑(frobenius K p)^[x.fst ] y.snd)

source

@[protected, 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 := _, npow := monoid.npow._default (perfect_closure.mk K p (0, 1)) has_mul.mul _ _, npow_zero' := _, npow_succ' := _, mul_comm := _}

source

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)

source

@[protected, 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}

source

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

Equations

perfect_closure.has_add K p = {add := quot.lift (λ (x : ℕ × K), quot.lift (λ (y : ℕ × K), perfect_closure.mk K p (x.fst + y.fst, ⇑(frobenius K p)^[y.fst ] x.snd + ⇑(frobenius K p)^[x.fst ] y.snd)) _) _}

source

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

perfect_closure.mk K p x + perfect_closure.mk K p y = perfect_closure.mk K p (x.fst + y.fst, ⇑(frobenius K p)^[y.fst ] x.snd + ⇑(frobenius K p)^[x.fst ] y.snd)

source

@[protected, 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)) _}

source

@[simp]

theorem perfect_closure.neg_mk (K : Type u) [comm_ring K] (p : ℕ) [fact (nat.prime p)] [char_p K p] (x : ℕ × K) :

-perfect_closure.mk K p x = perfect_closure.mk K p (x.fst, -x.snd)

source

@[protected, 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)}

source

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)

source

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

source

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)

source

@[protected, 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 := _, nsmul := ring.nsmul._default 0 has_add.add _ _, nsmul_zero' := _, nsmul_succ' := _, neg := has_neg.neg infer_instance, sub := ring.sub._default has_add.add _ 0 _ _ (ring.nsmul._default 0 has_add.add _ _) _ _ has_neg.neg, sub_eq_add_neg := _, zsmul := ring.zsmul._default has_add.add _ 0 _ _ (ring.nsmul._default 0 has_add.add _ _) _ _ has_neg.neg, zsmul_zero' := _, zsmul_succ' := _, zsmul_neg' := _, add_left_neg := _, add_comm := _, mul := comm_monoid.mul infer_instance, mul_assoc := _, one := comm_monoid.one infer_instance, one_mul := _, mul_one := _, npow := comm_monoid.npow infer_instance, npow_zero' := _, npow_succ' := _, left_distrib := _, right_distrib := _, mul_comm := _}

source

theorem perfect_closure.eq_iff' (K : Type u) [comm_ring K] (p : ℕ) [fact (nat.prime p)] [char_p K p] (x y : ℕ × K) :

perfect_closure.mk K p x = perfect_closure.mk K p y ↔ ∃ (z : ℕ), ⇑(frobenius K p)^[y.fst + z] x.snd = ⇑(frobenius K p)^[x.fst + z] y.snd

source

theorem perfect_closure.nat_cast (K : Type u) [comm_ring K] (p : ℕ) [fact (nat.prime p)] [char_p K p] (n x : ℕ) :

↑x = perfect_closure.mk K p (n, ↑x)

source

theorem perfect_closure.int_cast (K : Type u) [comm_ring K] (p : ℕ) [fact (nat.prime p)] [char_p K p] (x : ℤ) :

↑x = perfect_closure.mk K p (0, ↑x)

source

theorem perfect_closure.nat_cast_eq_iff (K : Type u) [comm_ring K] (p : ℕ) [fact (nat.prime p)] [char_p K p] (x y : ℕ) :

↑x = ↑y ↔ ↑x = ↑y

source

@[protected, 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

source

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)

source

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' := _}

source

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)

source

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

source

@[protected, 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)⁻¹)) _}

source

@[protected, 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 := _, nsmul := comm_ring.nsmul infer_instance, nsmul_zero' := _, nsmul_succ' := _, neg := comm_ring.neg infer_instance, sub := comm_ring.sub infer_instance, sub_eq_add_neg := _, zsmul := comm_ring.zsmul infer_instance, zsmul_zero' := _, zsmul_succ' := _, zsmul_neg' := _, add_left_neg := _, add_comm := _, mul := comm_ring.mul infer_instance, mul_assoc := _, one := comm_ring.one infer_instance, one_mul := _, mul_one := _, npow := comm_ring.npow infer_instance, npow_zero' := _, npow_succ' := _, left_distrib := _, right_distrib := _, mul_comm := _, inv := has_inv.inv infer_instance, div := div_inv_monoid.div._default comm_ring.mul _ comm_ring.one _ _ comm_ring.npow _ _ has_inv.inv, div_eq_mul_inv := _, zpow := div_inv_monoid.zpow._default comm_ring.mul _ comm_ring.one _ _ comm_ring.npow _ _ has_inv.inv, zpow_zero' := _, zpow_succ' := _, zpow_neg' := _, exists_pair_ne := _, mul_inv_cancel := _, inv_zero := _}

source

@[protected, instance]

def perfect_closure.perfect_ring (K : Type u) [field K] (p : ℕ) [fact (nat.prime p)] [char_p K p] :

perfect_ring (perfect_closure K p) p

Equations

perfect_closure.perfect_ring 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' := _, pth_root_frobenius' := _}

source

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)

source

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

(K →+* L) ≃ (perfect_closure K 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

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 := _}

source

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

perfect_ring k p

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

Equations

perfect_ring.of_surjective k p h = {pth_root' := function.surj_inv h, frobenius_pth_root' := _, pth_root_frobenius' := _}

mathlib documentation

The perfect closure of a field #