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 characteristicp
(prime) is said to be perfect in the sense of Serre, if its absolute Frobenius mapx ↦ xᵖ
is bijective.PerfectField
: a fieldK
is said to be perfect if every irreducible polynomial overK
is separable.PerfectRing.toPerfectField
: a field that is perfect in the sense of Serre is a perfect field.PerfectField.toPerfectRing
: a perfect field of characteristicp
(prime) is perfect in the sense of Serre.PerfectField.ofCharZero
: all fields of characteristic zero are perfect.PerfectField.ofFinite
: all finite fields are perfect.PerfectField.separable_iff_squarefree
: a polynomial over a perfect field is separable iff it is square-free.Algebra.IsAlgebraic.isSeparable_of_perfectField
,Algebra.IsAlgebraic.perfectField
: ifL / K
is an algebraic extension,K
is a perfect field, thenL / K
is separable, andL
is also a perfect field.
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).
- bijective_frobenius : Function.Bijective ⇑(frobenius R p)
A ring is perfect if the Frobenius map is bijective.
Instances
A ring is perfect if the Frobenius map is bijective.
For a reduced ring, surjectivity of the Frobenius map is a sufficient condition for perfection.
Equations
- ⋯ = ⋯
The Frobenius automorphism for a perfect ring.
Equations
- frobeniusEquiv R p = RingEquiv.ofBijective (frobenius R p) ⋯
Instances For
The iterated Frobenius automorphism for a perfect ring.
Equations
- iterateFrobeniusEquiv R p n = RingEquiv.ofBijective (iterateFrobenius R p n) ⋯
Instances For
Equations
- ⋯ = ⋯
A perfect field.
See also PerfectRing
for a generalisation in positive characteristic.
- separable_of_irreducible : ∀ {f : Polynomial K}, Irreducible f → f.Separable
A field is perfect if every irreducible polynomial is separable.
Instances
A field is perfect if every irreducible polynomial is separable.
Equations
- ⋯ = ⋯
Equations
- ⋯ = ⋯
A perfect field of characteristic p
(prime) is a perfect ring.
Equations
- ⋯ = ⋯
If L / K
is an algebraic extension, K
is a perfect field, then L / K
is separable.
Equations
- ⋯ = ⋯
If L / K
is an algebraic extension, K
is a perfect field, then so is L
.
If f
is a polynomial over an integral domain R
of characteristic p
, then there is
a map from the set of roots of Polynomial.expand R p f
to the set of roots of f
.
It's given by x ↦ x ^ p
, see rootsExpandToRoots_apply
.
Equations
- Polynomial.rootsExpandToRoots p f = { toFun := fun (x : { x : R // x ∈ ((Polynomial.expand R p) f).roots.toFinset }) => ⟨↑x ^ p, ⋯⟩, inj' := ⋯ }
Instances For
If f
is a polynomial over an integral domain R
of characteristic p
, then there is
a map from the set of roots of Polynomial.expand R (p ^ n) f
to the set of roots of f
.
It's given by x ↦ x ^ (p ^ n)
, see rootsExpandPowToRoots_apply
.
Equations
- Polynomial.rootsExpandPowToRoots p n f = { toFun := fun (x : { x : R // x ∈ ((Polynomial.expand R (p ^ n)) f).roots.toFinset }) => ⟨↑x ^ p ^ n, ⋯⟩, inj' := ⋯ }
Instances For
If f
is a polynomial over a perfect integral domain R
of characteristic p
, then there is
a bijection from the set of roots of Polynomial.expand R p f
to the set of roots of f
.
It's given by x ↦ x ^ p
, see rootsExpandEquivRoots_apply
.
Equations
- Polynomial.rootsExpandEquivRoots p f = ((frobeniusEquiv R p).image (Membership.mem ((Polynomial.expand R p) f).roots.toFinset.val)).trans (Equiv.Set.ofEq ⋯)
Instances For
If f
is a polynomial over a perfect integral domain R
of characteristic p
, then there is
a bijection from the set of roots of Polynomial.expand R (p ^ n) f
to the set of roots of f
.
It's given by x ↦ x ^ (p ^ n)
, see rootsExpandPowEquivRoots_apply
.
Equations
- Polynomial.rootsExpandPowEquivRoots p f n = ((iterateFrobeniusEquiv R p n).image (Membership.mem ((Polynomial.expand R (p ^ n)) f).roots.toFinset.val)).trans (Equiv.Set.ofEq ⋯)