|
| 1 | +/- |
| 2 | +Copyright (c) 2023 Oliver Nash. All rights reserved. |
| 3 | +Released under Apache 2.0 license as described in the file LICENSE. |
| 4 | +Authors: Oliver Nash |
| 5 | +-/ |
| 6 | +import Mathlib.FieldTheory.Separable |
| 7 | +import Mathlib.FieldTheory.SplittingField.Construction |
| 8 | + |
| 9 | +/-! |
| 10 | +
|
| 11 | +# Perfect fields and rings |
| 12 | +
|
| 13 | +In this file we define perfect fields, together with a generalisation to (commutative) rings in |
| 14 | +prime characteristic. |
| 15 | +
|
| 16 | +## Main definitions / statements: |
| 17 | + * `PerfectRing`: a ring of characteristic `p` (prime) is said to be perfect in the sense of Serre, |
| 18 | + if its absolute Frobenius map `x ↦ xᵖ` is bijective. |
| 19 | + * `PerfectField`: a field `K` is said to be perfect if every irreducible polynomial over `K` is |
| 20 | + separable. |
| 21 | + * `PerfectRing.toPerfectField`: a field that is perfect in the sense of Serre is a perfect field. |
| 22 | + * `PerfectField.toPerfectRing`: a perfect field of characteristic `p` (prime) is perfect in the |
| 23 | + sense of Serre. |
| 24 | + * `PerfectField.ofCharZero`: all fields of characteristic zero are perfect. |
| 25 | + * `PerfectField.ofFinite`: all finite fields are perfect. |
| 26 | +
|
| 27 | +-/ |
| 28 | + |
| 29 | +open Function Polynomial |
| 30 | + |
| 31 | +/-- A perfect ring of characteristic `p` (prime) in the sense of Serre. |
| 32 | +
|
| 33 | +NB: This is not related to the concept with the same name introduced by Bass (related to projective |
| 34 | +covers of modules). -/ |
| 35 | +class PerfectRing (R : Type _) (p : ℕ) [CommSemiring R] [Fact p.Prime] [CharP R p] : Prop where |
| 36 | + /-- A ring is perfect if the Frobenius map is bijective. -/ |
| 37 | + bijective_frobenius : Bijective $ frobenius R p |
| 38 | + |
| 39 | +section PerfectRing |
| 40 | + |
| 41 | +variable (R : Type _) (p : ℕ) [CommSemiring R] [Fact p.Prime] [CharP R p] |
| 42 | + |
| 43 | +/-- For a reduced ring, surjectivity of the Frobenius map is a sufficient condition for perfection. |
| 44 | +-/ |
| 45 | +lemma PerfectRing.ofSurjective (R : Type _) (p : ℕ) [CommRing R] [Fact p.Prime] [CharP R p] |
| 46 | + [IsReduced R] (h : Surjective $ frobenius R p) : PerfectRing R p := |
| 47 | + ⟨frobenius_inj R p, h⟩ |
| 48 | +#align perfect_ring.of_surjective PerfectRing.ofSurjective |
| 49 | + |
| 50 | +instance PerfectRing.ofFiniteOfIsReduced (R : Type _) [CommRing R] [CharP R p] |
| 51 | + [Finite R] [IsReduced R] : PerfectRing R p := |
| 52 | + ofSurjective _ _ $ Finite.surjective_of_injective (frobenius_inj R p) |
| 53 | + |
| 54 | +variable [PerfectRing R p] |
| 55 | + |
| 56 | +@[simp] |
| 57 | +theorem bijective_frobenius : Bijective (frobenius R p) := PerfectRing.bijective_frobenius |
| 58 | + |
| 59 | +@[simp] |
| 60 | +theorem injective_frobenius : Injective (frobenius R p) := (bijective_frobenius R p).1 |
| 61 | + |
| 62 | +@[simp] |
| 63 | +theorem surjective_frobenius : Surjective (frobenius R p) := (bijective_frobenius R p).2 |
| 64 | + |
| 65 | +/-- The Frobenius automorphism for a perfect ring. -/ |
| 66 | +@[simps! apply] |
| 67 | +noncomputable def frobeniusEquiv : R ≃+* R := |
| 68 | + RingEquiv.ofBijective (frobenius R p) PerfectRing.bijective_frobenius |
| 69 | +#align frobenius_equiv frobeniusEquiv |
| 70 | + |
| 71 | +@[simp] |
| 72 | +theorem coe_frobeniusEquiv : ⇑(frobeniusEquiv R p) = frobenius R p := rfl |
| 73 | +#align coe_frobenius_equiv coe_frobeniusEquiv |
| 74 | + |
| 75 | +@[simp] |
| 76 | +theorem frobeniusEquiv_symm_apply_frobenius (x : R) : |
| 77 | + (frobeniusEquiv R p).symm (frobenius R p x) = x := |
| 78 | + leftInverse_surjInv PerfectRing.bijective_frobenius x |
| 79 | + |
| 80 | +@[simp] |
| 81 | +theorem frobenius_apply_frobeniusEquiv_symm (x : R) : |
| 82 | + frobenius R p ((frobeniusEquiv R p).symm x) = x := |
| 83 | + surjInv_eq _ _ |
| 84 | + |
| 85 | +@[simp] |
| 86 | +theorem frobenius_comp_frobeniusEquiv_symm : |
| 87 | + (frobenius R p).comp (frobeniusEquiv R p).symm = RingHom.id R := by |
| 88 | + ext; simp |
| 89 | + |
| 90 | +@[simp] |
| 91 | +theorem frobeniusEquiv_symm_comp_frobenius : |
| 92 | + ((frobeniusEquiv R p).symm : R →+* R).comp (frobenius R p) = RingHom.id R := by |
| 93 | + ext; simp |
| 94 | + |
| 95 | +@[simp] |
| 96 | +theorem frobeniusEquiv_symm_pow_p (x : R) : ((frobeniusEquiv R p).symm x) ^ p = x := |
| 97 | + frobenius_apply_frobeniusEquiv_symm R p x |
| 98 | + |
| 99 | +theorem injective_pow_p {x y : R} (h : x ^ p = y ^ p) : x = y := (frobeniusEquiv R p).injective h |
| 100 | +#align injective_pow_p injective_pow_p |
| 101 | + |
| 102 | +lemma polynomial_expand_eq (f : R[X]) : |
| 103 | + expand R p f = (f.map (frobeniusEquiv R p).symm) ^ p := by |
| 104 | + rw [← (f.map (S := R) (frobeniusEquiv R p).symm).expand_char p, map_expand, map_map, |
| 105 | + frobenius_comp_frobeniusEquiv_symm, map_id] |
| 106 | + |
| 107 | +@[simp] |
| 108 | +theorem not_irreducible_expand (f : R[X]) : ¬ Irreducible (expand R p f) := by |
| 109 | + have hp : Fact p.Prime := inferInstance |
| 110 | + rw [polynomial_expand_eq] |
| 111 | + exact fun hf ↦ hf.not_unit $ (of_irreducible_pow hp.out.ne_one hf).pow p |
| 112 | + |
| 113 | +instance (S : Type _) [CommSemiring S] [CharP S p] [PerfectRing S p] : |
| 114 | + PerfectRing (R × S) p := by |
| 115 | + constructor |
| 116 | + have : frobenius (R × S) p = Prod.map (frobenius R p) (frobenius S p) := by |
| 117 | + ext <;> simp [frobenius_def] |
| 118 | + rw [this] |
| 119 | + exact Bijective.Prod_map (bijective_frobenius R p) (bijective_frobenius S p) |
| 120 | + |
| 121 | +end PerfectRing |
| 122 | + |
| 123 | +/-- A perfect field. |
| 124 | +
|
| 125 | +See also `PerfectRing` for a generalisation in positive characteristic. -/ |
| 126 | +class PerfectField (K : Type _) [Field K] : Prop where |
| 127 | + /-- A field is perfect if every irreducible polynomial is separable. -/ |
| 128 | + separable_of_irreducible : ∀ {f : K[X]}, Irreducible f → f.Separable |
| 129 | + |
| 130 | +lemma PerfectRing.toPerfectField (K : Type _) (p : ℕ) |
| 131 | + [Field K] [hp : Fact p.Prime] [CharP K p] [PerfectRing K p] : PerfectField K := by |
| 132 | + refine' PerfectField.mk $ fun hf ↦ _ |
| 133 | + rcases separable_or p hf with h | ⟨-, g, -, rfl⟩ |
| 134 | + · assumption |
| 135 | + · exfalso; revert hf; simp |
| 136 | + |
| 137 | +namespace PerfectField |
| 138 | + |
| 139 | +variable (K : Type _) [Field K] |
| 140 | + |
| 141 | +instance ofCharZero [CharZero K] : PerfectField K := ⟨Irreducible.separable⟩ |
| 142 | + |
| 143 | +instance ofFinite [Finite K] : PerfectField K := by |
| 144 | + obtain ⟨p, _instP⟩ := CharP.exists K |
| 145 | + have : Fact p.Prime := ⟨CharP.char_is_prime K p⟩ |
| 146 | + exact PerfectRing.toPerfectField K p |
| 147 | + |
| 148 | +variable [PerfectField K] |
| 149 | + |
| 150 | +/-- A perfect field of characteristic `p` (prime) is a perfect ring. -/ |
| 151 | +instance toPerfectRing (p : ℕ) [hp : Fact p.Prime] [CharP K p] : PerfectRing K p := by |
| 152 | + refine' PerfectRing.ofSurjective _ _ $ fun y ↦ _ |
| 153 | + let f : K[X] := X ^ p - C y |
| 154 | + let L := f.SplittingField |
| 155 | + let ι := algebraMap K L |
| 156 | + have hf_deg : f.degree ≠ 0 := by |
| 157 | + rw [degree_X_pow_sub_C hp.out.pos y, p.cast_ne_zero]; exact hp.out.ne_zero |
| 158 | + let a : L := f.rootOfSplits ι (SplittingField.splits f) hf_deg |
| 159 | + have hfa : aeval a f = 0 := by rw [aeval_def, map_rootOfSplits _ (SplittingField.splits f) hf_deg] |
| 160 | + have ha_pow : a ^ p = ι y := by rwa [AlgHom.map_sub, aeval_X_pow, aeval_C, sub_eq_zero] at hfa |
| 161 | + let g : K[X] := minpoly K a |
| 162 | + suffices : (g.map ι).natDegree = 1 |
| 163 | + · rw [g.natDegree_map, ← degree_eq_iff_natDegree_eq_of_pos Nat.one_pos] at this |
| 164 | + obtain ⟨a' : K, ha' : ι a' = a⟩ := minpoly.mem_range_of_degree_eq_one K a this |
| 165 | + refine' ⟨a', NoZeroSMulDivisors.algebraMap_injective K L _⟩ |
| 166 | + rw [RingHom.map_frobenius, ha', frobenius_def, ha_pow] |
| 167 | + have hg_dvd : g.map ι ∣ (X - C a) ^ p := by |
| 168 | + convert Polynomial.map_dvd ι (minpoly.dvd K a hfa) |
| 169 | + rw [sub_pow_char, Polynomial.map_sub, Polynomial.map_pow, map_X, map_C, ← ha_pow, map_pow] |
| 170 | + have ha : IsIntegral K a := isIntegral_of_finite K a |
| 171 | + have hg_pow : g.map ι = (X - C a) ^ (g.map ι).natDegree := by |
| 172 | + obtain ⟨q, -, hq⟩ := (dvd_prime_pow (prime_X_sub_C a) p).mp hg_dvd |
| 173 | + rw [eq_of_monic_of_associated ((minpoly.monic ha).map ι) ((monic_X_sub_C a).pow q) hq, |
| 174 | + natDegree_pow, natDegree_X_sub_C, mul_one] |
| 175 | + have hg_sep : (g.map ι).Separable := (separable_of_irreducible $ minpoly.irreducible ha).map |
| 176 | + rw [hg_pow] at hg_sep |
| 177 | + refine' (Separable.of_pow (not_isUnit_X_sub_C a) _ hg_sep).2 |
| 178 | + rw [g.natDegree_map ι, ← Nat.pos_iff_ne_zero, natDegree_pos_iff_degree_pos] |
| 179 | + exact minpoly.degree_pos ha |
| 180 | + |
| 181 | +end PerfectField |
0 commit comments