# The perfect closure of a characteristic p ring #

## Tags #

perfect ring, perfect closure

theorem PerfectClosure.r_iff (K : Type u) [] (p : ) [Fact ()] [CharP K p] :
∀ (a a_1 : × K), PerfectClosure.R K p a a_1 ∃ (n : ) (x : K), a = (n, x) a_1 = (n + 1, () x)
inductive PerfectClosure.R (K : Type u) [] (p : ) [Fact ()] [CharP K p] :
× K × KProp

PerfectClosure.R is the relation (n, x) ∼ (n + 1, x ^ p) for n : ℕ and x : K. PerfectClosure K p is the quotient by this relation.

Instances For
def PerfectClosure (K : Type u) [] (p : ) [Fact ()] [CharP K p] :

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

Equations
Instances For
def PerfectClosure.mk (K : Type u) [] (p : ) [Fact ()] [CharP K p] (x : × K) :

PerfectClosure.mk K p (n, x) for n : ℕ and x : K is an element of PerfectClosure K p, viewed as x ^ (p ^ -n). Every element of PerfectClosure K p is of this form (PerfectClosure.mk_surjective).

Equations
Instances For
theorem PerfectClosure.mk_surjective (K : Type u) [] (p : ) [Fact ()] [CharP K p] :
@[simp]
theorem PerfectClosure.mk_succ_pow (K : Type u) [] (p : ) [Fact ()] [CharP K p] (m : ) (x : K) :
PerfectClosure.mk K p (m + 1, x ^ p) = PerfectClosure.mk K p (m, x)
@[simp]
theorem PerfectClosure.quot_mk_eq_mk (K : Type u) [] (p : ) [Fact ()] [CharP K p] (x : × K) :
Quot.mk () x =
def PerfectClosure.liftOn {K : Type u} [] {p : } [Fact ()] [CharP K p] {L : Type u_1} (x : ) (f : × KL) (hf : ∀ (x y : × K), PerfectClosure.R K p x yf x = f y) :
L

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

Equations
Instances For
@[simp]
theorem PerfectClosure.liftOn_mk {K : Type u} [] {p : } [Fact ()] [CharP K p] {L : Type u_1} (f : × KL) (hf : ∀ (x y : × K), PerfectClosure.R K p x yf x = f y) (x : × K) :
().liftOn f hf = f x
theorem PerfectClosure.induction_on {K : Type u} [] {p : } [Fact ()] [CharP K p] (x : ) {q : Prop} (h : ∀ (x : × K), q ()) :
q x
instance PerfectClosure.instMul (K : Type u) [] (p : ) [Fact ()] [CharP K p] :
Mul ()
Equations
• One or more equations did not get rendered due to their size.
@[simp]
theorem PerfectClosure.mk_mul_mk (K : Type u) [] (p : ) [Fact ()] [CharP K p] (x : × K) (y : × K) :
* = PerfectClosure.mk K p (x.1 + y.1, (())^[y.1] x.2 * (())^[x.1] y.2)
instance PerfectClosure.instCommMonoid (K : Type u) [] (p : ) [Fact ()] [CharP K p] :
Equations
• = let __src := inferInstance;
theorem PerfectClosure.one_def (K : Type u) [] (p : ) [Fact ()] [CharP K p] :
1 = PerfectClosure.mk K p (0, 1)
instance PerfectClosure.instInhabited (K : Type u) [] (p : ) [Fact ()] [CharP K p] :
Equations
• = { default := 1 }
instance PerfectClosure.instAdd (K : Type u) [] (p : ) [Fact ()] [CharP K p] :
Equations
• One or more equations did not get rendered due to their size.
@[simp]
theorem PerfectClosure.mk_add_mk (K : Type u) [] (p : ) [Fact ()] [CharP K p] (x : × K) (y : × K) :
+ = PerfectClosure.mk K p (x.1 + y.1, (())^[y.1] x.2 + (())^[x.1] y.2)
instance PerfectClosure.instNeg (K : Type u) [] (p : ) [Fact ()] [CharP K p] :
Neg ()
Equations
@[simp]
theorem PerfectClosure.neg_mk (K : Type u) [] (p : ) [Fact ()] [CharP K p] (x : × K) :
- = PerfectClosure.mk K p (x.1, -x.2)
instance PerfectClosure.instZero (K : Type u) [] (p : ) [Fact ()] [CharP K p] :
Zero ()
Equations
theorem PerfectClosure.zero_def (K : Type u) [] (p : ) [Fact ()] [CharP K p] :
0 = PerfectClosure.mk K p (0, 0)
@[simp]
theorem PerfectClosure.mk_zero_zero (K : Type u) [] (p : ) [Fact ()] [CharP K p] :
PerfectClosure.mk K p (0, 0) = 0
theorem PerfectClosure.mk_zero (K : Type u) [] (p : ) [Fact ()] [CharP K p] (n : ) :
PerfectClosure.mk K p (n, 0) = 0
theorem PerfectClosure.R.sound (K : Type u) [] (p : ) [Fact ()] [CharP K p] (m : ) (n : ) (x : K) (y : K) (H : (())^[m] x = y) :
PerfectClosure.mk K p (n, x) = PerfectClosure.mk K p (m + n, y)
instance PerfectClosure.instAddCommGroup (K : Type u) [] (p : ) [Fact ()] [CharP K p] :
Equations
• = let __src := inferInstance; let __src_1 := inferInstance;
instance PerfectClosure.instCommRing (K : Type u) [] (p : ) [Fact ()] [CharP K p] :
Equations
• = let __src := ; let __src_1 := AddMonoidWithOne.unary; let __src_2 := inferInstance;
theorem PerfectClosure.mk_eq_iff (K : Type u) [] (p : ) [Fact ()] [CharP K p] (x : × K) (y : × K) :
= ∃ (z : ), (())^[y.1 + z] x.2 = (())^[x.1 + z] y.2
@[simp]
theorem PerfectClosure.mk_pow (K : Type u) [] (p : ) [Fact ()] [CharP K p] (x : × K) (n : ) :
^ n = PerfectClosure.mk K p (x.1, x.2 ^ n)
theorem PerfectClosure.natCast (K : Type u) [] (p : ) [Fact ()] [CharP K p] (n : ) (x : ) :
x = PerfectClosure.mk K p (n, x)
@[deprecated PerfectClosure.natCast]
theorem PerfectClosure.nat_cast (K : Type u) [] (p : ) [Fact ()] [CharP K p] (n : ) (x : ) :
x = PerfectClosure.mk K p (n, x)

Alias of PerfectClosure.natCast.

theorem PerfectClosure.intCast (K : Type u) [] (p : ) [Fact ()] [CharP K p] (x : ) :
x = PerfectClosure.mk K p (0, x)
@[deprecated PerfectClosure.intCast]
theorem PerfectClosure.int_cast (K : Type u) [] (p : ) [Fact ()] [CharP K p] (x : ) :
x = PerfectClosure.mk K p (0, x)

Alias of PerfectClosure.intCast.

theorem PerfectClosure.natCast_eq_iff (K : Type u) [] (p : ) [Fact ()] [CharP K p] (x : ) (y : ) :
x = y x = y
@[deprecated PerfectClosure.natCast_eq_iff]
theorem PerfectClosure.nat_cast_eq_iff (K : Type u) [] (p : ) [Fact ()] [CharP K p] (x : ) (y : ) :
x = y x = y

Alias of PerfectClosure.natCast_eq_iff.

instance PerfectClosure.instCharP (K : Type u) [] (p : ) [Fact ()] [CharP K p] :
CharP () p
Equations
• =
theorem PerfectClosure.frobenius_mk (K : Type u) [] (p : ) [Fact ()] [CharP K p] (x : × K) :
(frobenius () p) () = PerfectClosure.mk K p (x.1, x.2 ^ p)
def PerfectClosure.of (K : Type u) [] (p : ) [Fact ()] [CharP K p] :

Embedding of K into PerfectClosure K p

Equations
• = { toFun := fun (x : K) => PerfectClosure.mk K p (0, x), map_one' := , map_mul' := , map_zero' := , map_add' := }
Instances For
theorem PerfectClosure.of_apply (K : Type u) [] (p : ) [Fact ()] [CharP K p] (x : K) :
() x = PerfectClosure.mk K p (0, x)
instance PerfectClosure.instReduced (K : Type u) [] (p : ) [Fact ()] [CharP K p] :
Equations
• =
instance PerfectClosure.instPerfectRing (K : Type u) [] (p : ) [Fact ()] [CharP K p] :
Equations
• =
@[simp]
theorem PerfectClosure.iterate_frobenius_mk (K : Type u) [] (p : ) [Fact ()] [CharP K p] (n : ) (x : K) :
((frobenius () p))^[n] (PerfectClosure.mk K p (n, x)) = () x
noncomputable def PerfectClosure.lift (K : Type u) [] (p : ) [Fact ()] [CharP K p] (L : Type v) [] [CharP L p] [] :
(K →+* L) ( →+* L)

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

Equations
• One or more equations did not get rendered due to their size.
Instances For
theorem PerfectClosure.eq_iff (K : Type u) [] [] (p : ) [Fact ()] [CharP K p] (x : × K) (y : × K) :
= (())^[y.1] x.2 = (())^[x.1] y.2
instance PerfectClosure.instInv (K : Type u) [] (p : ) [Fact ()] [CharP K p] :
Inv ()
Equations
@[simp]
theorem PerfectClosure.mk_inv (K : Type u) [] (p : ) [Fact ()] [CharP K p] (x : × K) :
()⁻¹ = PerfectClosure.mk K p (x.1, x.2⁻¹)
instance PerfectClosure.instDivisionRing (K : Type u) [] (p : ) [Fact ()] [CharP K p] :
Equations
instance PerfectClosure.instField (K : Type u) [] (p : ) [Fact ()] [CharP K p] :
Equations
• = let __src := inferInstance; let __src_1 := inferInstance; Field.mk DivisionRing.zpow DivisionRing.nnqsmul DivisionRing.qsmul
instance PerfectClosure.instPerfectField (K : Type u) [] (p : ) [Fact ()] [CharP K p] :
Equations
• =