The perfect closure of a characteristic p ring

Main definitions

• PerfectClosure: the perfect closure of a characteristic p ring, which is the smallest extension that makes frobenius surjective.

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

• PerfectClosure.of: the structure map from K to PerfectClosure K p.

• PerfectClosure.lift: 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.

Main results

• PerfectClosure.induction_on: to prove a result for all elements of the perfect closure, one only needs to prove it for all elements of the form x ^ (p ^ -n).

• PerfectClosure.mk_mul_mk, PerfectClosure.one_def, PerfectClosure.mk_add_mk, PerfectClosure.neg_mk, PerfectClosure.zero_def, PerfectClosure.mk_zero_zero, PerfectClosure.mk_zero, PerfectClosure.mk_inv, PerfectClosure.mk_pow: how to do multiplication, addition, etc. on elements of form x ^ (p ^ -n).

• PerfectClosure.mk_eq_iff: when does x ^ (p ^ -n) equal.

• PerfectClosure.eq_iff: same as PerfectClosure.mk_eq_iff but with additional assumption that K being reduced, hence gives a simpler criterion.

• PerfectClosure.instPerfectRing: PerfectClosure K p is a perfect ring.

Tags

perfect ring, perfect closure

inductive PerfectClosure.R (K : Type u) [CommRing K] (p : ℕ) [Fact (Nat.Prime p)] [CharP K p] : ℕ × K → ℕ × K → Prop

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.

• intro {K : Type u} [CommRing K] {p : ℕ} [Fact (Nat.Prime p)] [CharP K p] (n : ℕ) (x : K) : R K p (n, x) (n + 1, (frobenius K p) x)

theorem PerfectClosure.r_iff (K : Type u) [CommRing K] (p : ℕ) [Fact (Nat.Prime p)] [CharP K p] (a✝ a✝¹ : ℕ × K) : R K p a✝ a✝¹ ↔ ∃ (n : ℕ) (x : K), a✝ = (n, x) ∧ a✝¹ = (n + 1, (frobenius K p) x)

def PerfectClosure (K : Type u) [CommRing K] (p : ℕ) [Fact (Nat.Prime p)] [CharP K p] : Type u

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

def PerfectClosure.mk (K : Type u) [CommRing K] (p : ℕ) [Fact (Nat.Prime p)] [CharP K p] (x : ℕ × K) : PerfectClosure K p

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

theorem PerfectClosure.mk_surjective (K : Type u) [CommRing K] (p : ℕ) [Fact (Nat.Prime p)] [CharP K p] : Function.Surjective (mk K p)

@[simp]

theorem PerfectClosure.mk_succ_pow (K : Type u) [CommRing K] (p : ℕ) [Fact (Nat.Prime p)] [CharP K p] (m : ℕ) (x : K) : mk K p (m + 1, x ^ p) = mk K p (m, x)

@[simp]

theorem PerfectClosure.quot_mk_eq_mk (K : Type u) [CommRing K] (p : ℕ) [Fact (Nat.Prime p)] [CharP K p] (x : ℕ × K) : Quot.mk (R K p) x = mk K p x

def PerfectClosure.liftOn {K : Type u} [CommRing K] {p : ℕ} [Fact (Nat.Prime p)] [CharP K p] {L : Type u_1} (x : PerfectClosure K p) (f : ℕ × K → L) (hf : ∀ (x y : ℕ × K), R K p x y → f x = f y) : L

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

@[simp]

theorem PerfectClosure.liftOn_mk {K : Type u} [CommRing K] {p : ℕ} [Fact (Nat.Prime p)] [CharP K p] {L : Type u_1} (f : ℕ × K → L) (hf : ∀ (x y : ℕ × K), R K p x y → f x = f y) (x : ℕ × K) : (mk K p x).liftOn f hf = f x

theorem PerfectClosure.induction_on {K : Type u} [CommRing K] {p : ℕ} [Fact (Nat.Prime p)] [CharP K p] (x : PerfectClosure K p) {q : PerfectClosure K p → Prop} (h : ∀ (x : ℕ × K), q (mk K p x)) : q x

instance PerfectClosure.instMul (K : Type u) [CommRing K] (p : ℕ) [Fact (Nat.Prime p)] [CharP K p] : Mul (PerfectClosure K p)

@[simp]

theorem PerfectClosure.mk_mul_mk (K : Type u) [CommRing K] (p : ℕ) [Fact (Nat.Prime p)] [CharP K p] (x y : ℕ × K) : mk K p x * mk K p y = mk K p (x.1 + y.1, (⇑(frobenius K p))^[y.1] x.2 * (⇑(frobenius K p))^[x.1] y.2)

instance PerfectClosure.instCommMonoid (K : Type u) [CommRing K] (p : ℕ) [Fact (Nat.Prime p)] [CharP K p] : CommMonoid (PerfectClosure K p)

theorem PerfectClosure.one_def (K : Type u) [CommRing K] (p : ℕ) [Fact (Nat.Prime p)] [CharP K p] : 1 = mk K p (0, 1)

instance PerfectClosure.instInhabited (K : Type u) [CommRing K] (p : ℕ) [Fact (Nat.Prime p)] [CharP K p] : Inhabited (PerfectClosure K p)

instance PerfectClosure.instAdd (K : Type u) [CommRing K] (p : ℕ) [Fact (Nat.Prime p)] [CharP K p] : Add (PerfectClosure K p)

@[simp]

theorem PerfectClosure.mk_add_mk (K : Type u) [CommRing K] (p : ℕ) [Fact (Nat.Prime p)] [CharP K p] (x y : ℕ × K) : mk K p x + mk K p y = mk K p (x.1 + y.1, (⇑(frobenius K p))^[y.1] x.2 + (⇑(frobenius K p))^[x.1] y.2)

instance PerfectClosure.instNeg (K : Type u) [CommRing K] (p : ℕ) [Fact (Nat.Prime p)] [CharP K p] : Neg (PerfectClosure K p)

@[simp]

theorem PerfectClosure.neg_mk (K : Type u) [CommRing K] (p : ℕ) [Fact (Nat.Prime p)] [CharP K p] (x : ℕ × K) : -mk K p x = mk K p (x.1, -x.2)

instance PerfectClosure.instZero (K : Type u) [CommRing K] (p : ℕ) [Fact (Nat.Prime p)] [CharP K p] : Zero (PerfectClosure K p)

theorem PerfectClosure.zero_def (K : Type u) [CommRing K] (p : ℕ) [Fact (Nat.Prime p)] [CharP K p] : 0 = mk K p (0, 0)

@[simp]

theorem PerfectClosure.mk_zero (K : Type u) [CommRing K] (p : ℕ) [Fact (Nat.Prime p)] [CharP K p] : mk K p 0 = 0

Prior to https://github.com/leanprover-community/mathlib4/pull/15862, this lemma was called mk_zero_zero. See mk_zero_right for the lemma used to be called mk_zero.

@[simp]

theorem PerfectClosure.mk_zero_right (K : Type u) [CommRing K] (p : ℕ) [Fact (Nat.Prime p)] [CharP K p] (n : ℕ) : mk K p (n, 0) = 0

theorem PerfectClosure.R.sound (K : Type u) [CommRing K] (p : ℕ) [Fact (Nat.Prime p)] [CharP K p] (m n : ℕ) (x y : K) (H : (⇑(frobenius K p))^[m] x = y) : mk K p (n, x) = mk K p (m + n, y)

instance PerfectClosure.instAddCommGroup (K : Type u) [CommRing K] (p : ℕ) [Fact (Nat.Prime p)] [CharP K p] : AddCommGroup (PerfectClosure K p)

instance PerfectClosure.instCommRing (K : Type u) [CommRing K] (p : ℕ) [Fact (Nat.Prime p)] [CharP K p] : CommRing (PerfectClosure K p)

theorem PerfectClosure.mk_eq_iff (K : Type u) [CommRing K] (p : ℕ) [Fact (Nat.Prime p)] [CharP K p] (x y : ℕ × K) : mk K p x = mk K p y ↔ ∃ (z : ℕ), (⇑(frobenius K p))^[y.1 + z] x.2 = (⇑(frobenius K p))^[x.1 + z] y.2

@[simp]

theorem PerfectClosure.mk_pow (K : Type u) [CommRing K] (p : ℕ) [Fact (Nat.Prime p)] [CharP K p] (x : ℕ × K) (n : ℕ) : mk K p x ^ n = mk K p (x.1, x.2 ^ n)

theorem PerfectClosure.natCast (K : Type u) [CommRing K] (p : ℕ) [Fact (Nat.Prime p)] [CharP K p] (n x : ℕ) : ↑x = mk K p (n, ↑x)

theorem PerfectClosure.intCast (K : Type u) [CommRing K] (p : ℕ) [Fact (Nat.Prime p)] [CharP K p] (x : ℤ) : ↑x = mk K p (0, ↑x)

theorem PerfectClosure.natCast_eq_iff (K : Type u) [CommRing K] (p : ℕ) [Fact (Nat.Prime p)] [CharP K p] (x y : ℕ) : ↑x = ↑y ↔ ↑x = ↑y

instance PerfectClosure.instCharP (K : Type u) [CommRing K] (p : ℕ) [Fact (Nat.Prime p)] [CharP K p] : CharP (PerfectClosure K p) p

theorem PerfectClosure.frobenius_mk (K : Type u) [CommRing K] (p : ℕ) [Fact (Nat.Prime p)] [CharP K p] (x : ℕ × K) : (frobenius (PerfectClosure K p) p) (mk K p x) = mk K p (x.1, x.2 ^ p)

def PerfectClosure.of (K : Type u) [CommRing K] (p : ℕ) [Fact (Nat.Prime p)] [CharP K p] : K →+* PerfectClosure K p

Embedding of K into PerfectClosure K p

theorem PerfectClosure.of_apply (K : Type u) [CommRing K] (p : ℕ) [Fact (Nat.Prime p)] [CharP K p] (x : K) : (of K p) x = mk K p (0, x)

instance PerfectClosure.instReduced (K : Type u) [CommRing K] (p : ℕ) [Fact (Nat.Prime p)] [CharP K p] : IsReduced (PerfectClosure K p)

instance PerfectClosure.instPerfectRing (K : Type u) [CommRing K] (p : ℕ) [Fact (Nat.Prime p)] [CharP K p] : PerfectRing (PerfectClosure K p) p

@[simp]

theorem PerfectClosure.iterate_frobenius_mk (K : Type u) [CommRing K] (p : ℕ) [Fact (Nat.Prime p)] [CharP K p] (n : ℕ) (x : K) : (⇑(frobenius (PerfectClosure K p) p))^[n] (mk K p (n, x)) = (of K p) x

noncomputable def PerfectClosure.lift (K : Type u) [CommRing K] (p : ℕ) [Fact (Nat.Prime p)] [CharP K p] (L : Type v) [CommSemiring L] [CharP L p] [PerfectRing L p] : (K →+* L) ≃ (PerfectClosure K p →+* 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.

theorem PerfectClosure.eq_iff (K : Type u) [CommRing K] [IsReduced K] (p : ℕ) [Fact (Nat.Prime p)] [CharP K p] (x y : ℕ × K) : mk K p x = mk K p y ↔ (⇑(frobenius K p))^[y.1] x.2 = (⇑(frobenius K p))^[x.1] y.2

instance PerfectClosure.instNontrivialOfIsReduced (K : Type u) [CommRing K] [IsReduced K] (p : ℕ) [Fact (Nat.Prime p)] [CharP K p] [Nontrivial K] : Nontrivial (PerfectClosure K p)

instance PerfectClosure.instInv (K : Type u) [Field K] (p : ℕ) [Fact (Nat.Prime p)] [CharP K p] : Inv (PerfectClosure K p)

@[simp]

theorem PerfectClosure.mk_inv (K : Type u) [Field K] (p : ℕ) [Fact (Nat.Prime p)] [CharP K p] (x : ℕ × K) : (mk K p x)⁻¹ = mk K p (x.1, x.2⁻¹)

instance PerfectClosure.instDivisionRing (K : Type u) [Field K] (p : ℕ) [Fact (Nat.Prime p)] [CharP K p] : DivisionRing (PerfectClosure K p)

instance PerfectClosure.instField (K : Type u) [Field K] (p : ℕ) [Fact (Nat.Prime p)] [CharP K p] : Field (PerfectClosure K p)

instance PerfectClosure.instPerfectField (K : Type u) [Field K] (p : ℕ) [Fact (Nat.Prime p)] [CharP K p] : PerfectField (PerfectClosure K p)