Perfect fields and rings #

In this file we define perfect fields, together with a generalisation to (commutative) rings in prime characteristic.

Main definitions / statements: #

PerfectRing: a ring of characteristic p (prime) is said to be perfect in the sense of Serre, if its absolute Frobenius map x ↦ xᵖ is bijective.
PerfectField: a field K is said to be perfect if every irreducible polynomial over K is separable.
PerfectRing.toPerfectField: a field that is perfect in the sense of Serre is a perfect field.
PerfectField.toPerfectRing: a perfect field of characteristic p (prime) is perfect in the sense of Serre.
PerfectField.ofCharZero: all fields of characteristic zero are perfect.
PerfectField.ofFinite: all finite fields are perfect.

source

class PerfectRing (R : Type u_1) (p : ℕ) [CommSemiring R] [Fact (Nat.Prime p)] [CharP R p] :

Prop

bijective_frobenius : Function.Bijective ↑(frobenius R p)
A ring is perfect if the Frobenius map is bijective.

A perfect ring of characteristic p (prime) in the sense of Serre.

NB: This is not related to the concept with the same name introduced by Bass (related to projective covers of modules).

Instances

source

theorem PerfectRing.ofSurjective (R : Type u_1) (p : ℕ) [CommRing R] [Fact (Nat.Prime p)] [CharP R p] [IsReduced R] (h : Function.Surjective ↑(frobenius R p)) :

PerfectRing R p

For a reduced ring, surjectivity of the Frobenius map is a sufficient condition for perfection.

source

instance PerfectRing.ofFiniteOfIsReduced (p : ℕ) [Fact (Nat.Prime p)] (R : Type u_1) [CommRing R] [CharP R p] [Finite R] [IsReduced R] :

PerfectRing R p

Equations

PerfectRing.ofFiniteOfIsReduced = PerfectRing.ofFiniteOfIsReduced.proof_1

source

@[simp]

theorem bijective_frobenius (R : Type u_1) (p : ℕ) [CommSemiring R] [Fact (Nat.Prime p)] [CharP R p] [PerfectRing R p] :

Function.Bijective ↑(frobenius R p)

source

@[simp]

theorem injective_frobenius (R : Type u_1) (p : ℕ) [CommSemiring R] [Fact (Nat.Prime p)] [CharP R p] [PerfectRing R p] :

Function.Injective ↑(frobenius R p)

source

@[simp]

theorem surjective_frobenius (R : Type u_1) (p : ℕ) [CommSemiring R] [Fact (Nat.Prime p)] [CharP R p] [PerfectRing R p] :

Function.Surjective ↑(frobenius R p)

source

@[simp]

theorem frobeniusEquiv_apply (R : Type u_1) (p : ℕ) [CommSemiring R] [Fact (Nat.Prime p)] [CharP R p] [PerfectRing R p] (a : R) :

↑(frobeniusEquiv R p) a = ↑(frobenius R p) a

source

noncomputable def frobeniusEquiv (R : Type u_1) (p : ℕ) [CommSemiring R] [Fact (Nat.Prime p)] [CharP R p] [PerfectRing R p] :

R ≃+* R

The Frobenius automorphism for a perfect ring.

Equations

frobeniusEquiv R p = RingEquiv.ofBijective (frobenius R p) (_ : Function.Bijective ↑(frobenius R p))

Instances For

source

@[simp]

theorem coe_frobeniusEquiv (R : Type u_1) (p : ℕ) [CommSemiring R] [Fact (Nat.Prime p)] [CharP R p] [PerfectRing R p] :

↑(frobeniusEquiv R p) = ↑(frobenius R p)

source

@[simp]

theorem frobeniusEquiv_symm_apply_frobenius (R : Type u_1) (p : ℕ) [CommSemiring R] [Fact (Nat.Prime p)] [CharP R p] [PerfectRing R p] (x : R) :

↑(RingEquiv.symm (frobeniusEquiv R p)) (↑(frobenius R p) x) = x

source

@[simp]

theorem frobenius_apply_frobeniusEquiv_symm (R : Type u_1) (p : ℕ) [CommSemiring R] [Fact (Nat.Prime p)] [CharP R p] [PerfectRing R p] (x : R) :

↑(frobenius R p) (↑(RingEquiv.symm (frobeniusEquiv R p)) x) = x

source

@[simp]

theorem frobenius_comp_frobeniusEquiv_symm (R : Type u_1) (p : ℕ) [CommSemiring R] [Fact (Nat.Prime p)] [CharP R p] [PerfectRing R p] :

RingHom.comp (frobenius R p) ↑(RingEquiv.symm (frobeniusEquiv R p)) = RingHom.id R

source

@[simp]

theorem frobeniusEquiv_symm_comp_frobenius (R : Type u_1) (p : ℕ) [CommSemiring R] [Fact (Nat.Prime p)] [CharP R p] [PerfectRing R p] :

RingHom.comp (↑(RingEquiv.symm (frobeniusEquiv R p))) (frobenius R p) = RingHom.id R

source

@[simp]

theorem frobeniusEquiv_symm_pow_p (R : Type u_1) (p : ℕ) [CommSemiring R] [Fact (Nat.Prime p)] [CharP R p] [PerfectRing R p] (x : R) :

↑(RingEquiv.symm (frobeniusEquiv R p)) x ^ p = x

source

theorem injective_pow_p (R : Type u_1) (p : ℕ) [CommSemiring R] [Fact (Nat.Prime p)] [CharP R p] [PerfectRing R p] {x : R} {y : R} (h : x ^ p = y ^ p) :

x = y

source

theorem polynomial_expand_eq (R : Type u_1) (p : ℕ) [CommSemiring R] [Fact (Nat.Prime p)] [CharP R p] [PerfectRing R p] (f : Polynomial R) :

↑(Polynomial.expand R p) f = Polynomial.map (↑(RingEquiv.symm (frobeniusEquiv R p))) f ^ p

source

@[simp]

theorem not_irreducible_expand (R : Type u_1) (p : ℕ) [CommSemiring R] [Fact (Nat.Prime p)] [CharP R p] [PerfectRing R p] (f : Polynomial R) :

¬Irreducible (↑(Polynomial.expand R p) f)

source

instance instPerfectRingProdInstCommSemiringCharPToAddMonoidWithOneToAddCommMonoidWithOneToNonAssocSemiringToSemiringToAddMonoidWithOneToAddCommMonoidWithOneToNonAssocSemiringToSemiring (R : Type u_1) (p : ℕ) [CommSemiring R] [Fact (Nat.Prime p)] [CharP R p] [PerfectRing R p] (S : Type u_2) [CommSemiring S] [CharP S p] [PerfectRing S p] :

PerfectRing (R × S) p

Equations

One or more equations did not get rendered due to their size.

source

class PerfectField (K : Type u_1) [Field K] :

Prop

separable_of_irreducible : ∀ {f : Polynomial K}, Irreducible f → Polynomial.Separable f
A field is perfect if every irreducible polynomial is separable.

A perfect field.

See also PerfectRing for a generalisation in positive characteristic.

Instances

source