|
| 1 | +/- |
| 2 | +Copyright (c) 2024 Jz Pan. All rights reserved. |
| 3 | +Released under Apache 2.0 license as described in the file LICENSE. |
| 4 | +Authors: Jz Pan |
| 5 | +-/ |
| 6 | +import Mathlib.FieldTheory.PurelyInseparable.PerfectClosure |
| 7 | + |
| 8 | +/-! |
| 9 | +
|
| 10 | +# Tower law for purely inseparable extensions |
| 11 | +
|
| 12 | +This file contains results related to `Field.finIsepDegree` and the tower law. |
| 13 | +
|
| 14 | +## Main results |
| 15 | +
|
| 16 | +- `Field.lift_sepDegree_mul_lift_sepDegree_of_isAlgebraic`: the separable degrees satisfy the |
| 17 | + tower law: $[E:F]_s [K:E]_s = [K:F]_s$. |
| 18 | +
|
| 19 | +- `IntermediateField.sepDegree_adjoin_eq_of_isAlgebraic_of_isPurelyInseparable`, |
| 20 | + `IntermediateField.sepDegree_adjoin_eq_of_isAlgebraic_of_isPurelyInseparable'`: |
| 21 | + if `K / E / F` is a field extension tower, such that `E / F` is purely inseparable, then |
| 22 | + for any subset `S` of `K` such that `F(S) / F` is algebraic, the `E(S) / E` and `F(S) / F` have |
| 23 | + the same separable degree. In particular, if `S` is an intermediate field of `K / F` such that |
| 24 | + `S / F` is algebraic, the `E(S) / E` and `S / F` have the same separable degree. |
| 25 | +
|
| 26 | +- `minpoly.map_eq_of_isSeparable_of_isPurelyInseparable`: if `K / E / F` is a field extension tower, |
| 27 | + such that `E / F` is purely inseparable, then for any element `x` of `K` separable over `F`, |
| 28 | + it has the same minimal polynomials over `F` and over `E`. |
| 29 | +
|
| 30 | +- `Polynomial.Separable.map_irreducible_of_isPurelyInseparable`: if `E / F` is purely inseparable, |
| 31 | + `f` is a separable irreducible polynomial over `F`, then it is also irreducible over `E`. |
| 32 | +
|
| 33 | +## Tags |
| 34 | +
|
| 35 | +separable degree, degree, separable closure, purely inseparable |
| 36 | +
|
| 37 | +## TODO |
| 38 | +
|
| 39 | +- Restate some intermediate result in terms of linearly disjointness. |
| 40 | +
|
| 41 | +- Prove that the inseparable degrees satisfy the tower law: $[E:F]_i [K:E]_i = [K:F]_i$. |
| 42 | + Probably an argument using linearly disjointness is needed. |
| 43 | +
|
| 44 | +-/ |
| 45 | + |
| 46 | +open Polynomial IntermediateField Field |
| 47 | + |
| 48 | +noncomputable section |
| 49 | + |
| 50 | +universe u v w |
| 51 | + |
| 52 | +section TowerLaw |
| 53 | + |
| 54 | +variable (F : Type u) (E : Type v) [Field F] [Field E] [Algebra F E] |
| 55 | +variable (K : Type w) [Field K] [Algebra F K] |
| 56 | + |
| 57 | +variable [Algebra E K] [IsScalarTower F E K] |
| 58 | + |
| 59 | +variable {F K} in |
| 60 | +/-- If `K / E / F` is a field extension tower such that `E / F` is purely inseparable, |
| 61 | +if `{ u_i }` is a family of separable elements of `K` which is `F`-linearly independent, |
| 62 | +then it is also `E`-linearly independent. -/ |
| 63 | +theorem LinearIndependent.map_of_isPurelyInseparable_of_isSeparable [IsPurelyInseparable F E] |
| 64 | + {ι : Type*} {v : ι → K} (hsep : ∀ i : ι, IsSeparable F (v i)) |
| 65 | + (h : LinearIndependent F v) : LinearIndependent E v := by |
| 66 | + obtain ⟨q, _⟩ := ExpChar.exists F |
| 67 | + haveI := expChar_of_injective_algebraMap (algebraMap F K).injective q |
| 68 | + refine linearIndependent_iff.mpr fun l hl ↦ Finsupp.ext fun i ↦ ?_ |
| 69 | + choose f hf using fun i ↦ (isPurelyInseparable_iff_pow_mem F q).1 ‹_› (l i) |
| 70 | + let n := l.support.sup f |
| 71 | + have := (expChar_pow_pos F q n).ne' |
| 72 | + replace hf (i : ι) : l i ^ q ^ n ∈ (algebraMap F E).range := by |
| 73 | + by_cases hs : i ∈ l.support |
| 74 | + · convert pow_mem (hf i) (q ^ (n - f i)) using 1 |
| 75 | + rw [← pow_mul, ← pow_add, Nat.add_sub_of_le (Finset.le_sup hs)] |
| 76 | + exact ⟨0, by rw [map_zero, Finsupp.not_mem_support_iff.1 hs, zero_pow this]⟩ |
| 77 | + choose lF hlF using hf |
| 78 | + let lF₀ := Finsupp.onFinset l.support lF fun i ↦ by |
| 79 | + contrapose! |
| 80 | + refine fun hs ↦ (injective_iff_map_eq_zero _).mp (algebraMap F E).injective _ ?_ |
| 81 | + rw [hlF, Finsupp.not_mem_support_iff.1 hs, zero_pow this] |
| 82 | + replace h := linearIndependent_iff.1 (h.map_pow_expChar_pow_of_isSeparable' q n hsep) lF₀ <| by |
| 83 | + replace hl := congr($hl ^ q ^ n) |
| 84 | + rw [Finsupp.linearCombination_apply, Finsupp.sum, sum_pow_char_pow, zero_pow this] at hl |
| 85 | + rw [← hl, Finsupp.linearCombination_apply, |
| 86 | + Finsupp.onFinset_sum _ (fun _ ↦ by exact zero_smul _ _)] |
| 87 | + refine Finset.sum_congr rfl fun i _ ↦ ?_ |
| 88 | + simp_rw [Algebra.smul_def, mul_pow, IsScalarTower.algebraMap_apply F E K, hlF, map_pow] |
| 89 | + refine pow_eq_zero ((hlF _).symm.trans ?_) |
| 90 | + convert map_zero (algebraMap F E) |
| 91 | + exact congr($h i) |
| 92 | + |
| 93 | +namespace Field |
| 94 | + |
| 95 | +/-- If `K / E / F` is a field extension tower, such that `E / F` is purely inseparable and `K / E` |
| 96 | +is separable, then the separable degree of `K / F` is equal to the degree of `K / E`. |
| 97 | +It is a special case of `Field.lift_sepDegree_mul_lift_sepDegree_of_isAlgebraic`, and is an |
| 98 | +intermediate result used to prove it. -/ |
| 99 | +lemma sepDegree_eq_of_isPurelyInseparable_of_isSeparable |
| 100 | + [IsPurelyInseparable F E] [Algebra.IsSeparable E K] : sepDegree F K = Module.rank E K := by |
| 101 | + let S := separableClosure F K |
| 102 | + have h := S.adjoin_rank_le_of_isAlgebraic_right E |
| 103 | + rw [separableClosure.adjoin_eq_of_isAlgebraic_of_isSeparable K, rank_top'] at h |
| 104 | + obtain ⟨ι, ⟨b⟩⟩ := Basis.exists_basis F S |
| 105 | + exact h.antisymm' (b.mk_eq_rank'' ▸ (b.linearIndependent.map' S.val.toLinearMap |
| 106 | + (LinearMap.ker_eq_bot_of_injective S.val.injective) |
| 107 | + |>.map_of_isPurelyInseparable_of_isSeparable E (fun i ↦ |
| 108 | + by simpa only [IsSeparable, minpoly_eq] using Algebra.IsSeparable.isSeparable F (b i)) |
| 109 | + |>.cardinal_le_rank)) |
| 110 | + |
| 111 | +/-- If `K / E / F` is a field extension tower, such that `E / F` is separable, |
| 112 | +then $[E:F] [K:E]_s = [K:F]_s$. |
| 113 | +It is a special case of `Field.lift_sepDegree_mul_lift_sepDegree_of_isAlgebraic`, and is an |
| 114 | +intermediate result used to prove it. -/ |
| 115 | +lemma lift_rank_mul_lift_sepDegree_of_isSeparable [Algebra.IsSeparable F E] : |
| 116 | + Cardinal.lift.{w} (Module.rank F E) * Cardinal.lift.{v} (sepDegree E K) = |
| 117 | + Cardinal.lift.{v} (sepDegree F K) := by |
| 118 | + rw [sepDegree, sepDegree, separableClosure.eq_restrictScalars_of_isSeparable F E K] |
| 119 | + exact lift_rank_mul_lift_rank F E (separableClosure E K) |
| 120 | + |
| 121 | +/-- The same-universe version of `Field.lift_rank_mul_lift_sepDegree_of_isSeparable`. -/ |
| 122 | +lemma rank_mul_sepDegree_of_isSeparable (K : Type v) [Field K] [Algebra F K] |
| 123 | + [Algebra E K] [IsScalarTower F E K] [Algebra.IsSeparable F E] : |
| 124 | + Module.rank F E * sepDegree E K = sepDegree F K := by |
| 125 | + simpa only [Cardinal.lift_id] using lift_rank_mul_lift_sepDegree_of_isSeparable F E K |
| 126 | + |
| 127 | +/-- If `K / E / F` is a field extension tower, such that `E / F` is purely inseparable, |
| 128 | +then $[K:F]_s = [K:E]_s$. |
| 129 | +It is a special case of `Field.lift_sepDegree_mul_lift_sepDegree_of_isAlgebraic`, and is an |
| 130 | +intermediate result used to prove it. -/ |
| 131 | +lemma sepDegree_eq_of_isPurelyInseparable [IsPurelyInseparable F E] : |
| 132 | + sepDegree F K = sepDegree E K := by |
| 133 | + convert sepDegree_eq_of_isPurelyInseparable_of_isSeparable F E (separableClosure E K) |
| 134 | + haveI : IsScalarTower F (separableClosure E K) K := IsScalarTower.of_algebraMap_eq (congrFun rfl) |
| 135 | + rw [sepDegree, ← separableClosure.map_eq_of_separableClosure_eq_bot F |
| 136 | + (separableClosure.separableClosure_eq_bot E K)] |
| 137 | + exact (separableClosure F (separableClosure E K)).equivMap |
| 138 | + (IsScalarTower.toAlgHom F (separableClosure E K) K) |>.symm.toLinearEquiv.rank_eq |
| 139 | + |
| 140 | +/-- If `K / E / F` is a field extension tower, such that `E / F` is algebraic, then their |
| 141 | +separable degrees satisfy the tower law: $[E:F]_s [K:E]_s = [K:F]_s$. -/ |
| 142 | +theorem lift_sepDegree_mul_lift_sepDegree_of_isAlgebraic [Algebra.IsAlgebraic F E] : |
| 143 | + Cardinal.lift.{w} (sepDegree F E) * Cardinal.lift.{v} (sepDegree E K) = |
| 144 | + Cardinal.lift.{v} (sepDegree F K) := by |
| 145 | + have h := lift_rank_mul_lift_sepDegree_of_isSeparable F (separableClosure F E) K |
| 146 | + haveI := separableClosure.isPurelyInseparable F E |
| 147 | + rwa [sepDegree_eq_of_isPurelyInseparable (separableClosure F E) E K] at h |
| 148 | + |
| 149 | +/-- The same-universe version of `Field.lift_sepDegree_mul_lift_sepDegree_of_isAlgebraic`. -/ |
| 150 | +@[stacks 09HK "Part 1"] |
| 151 | +theorem sepDegree_mul_sepDegree_of_isAlgebraic (K : Type v) [Field K] [Algebra F K] |
| 152 | + [Algebra E K] [IsScalarTower F E K] [Algebra.IsAlgebraic F E] : |
| 153 | + sepDegree F E * sepDegree E K = sepDegree F K := by |
| 154 | + simpa only [Cardinal.lift_id] using lift_sepDegree_mul_lift_sepDegree_of_isAlgebraic F E K |
| 155 | + |
| 156 | +end Field |
| 157 | + |
| 158 | +variable {F K} in |
| 159 | +/-- If `K / E / F` is a field extension tower, such that `E / F` is purely inseparable, then |
| 160 | +for any subset `S` of `K` such that `F(S) / F` is algebraic, the `E(S) / E` and `F(S) / F` have |
| 161 | +the same separable degree. -/ |
| 162 | +theorem IntermediateField.sepDegree_adjoin_eq_of_isAlgebraic_of_isPurelyInseparable |
| 163 | + (S : Set K) [Algebra.IsAlgebraic F (adjoin F S)] [IsPurelyInseparable F E] : |
| 164 | + sepDegree E (adjoin E S) = sepDegree F (adjoin F S) := by |
| 165 | + set M := adjoin F S |
| 166 | + set L := adjoin E S |
| 167 | + let E' := (IsScalarTower.toAlgHom F E K).fieldRange |
| 168 | + let j : E ≃ₐ[F] E' := AlgEquiv.ofInjectiveField (IsScalarTower.toAlgHom F E K) |
| 169 | + have hi : M ≤ L.restrictScalars F := by |
| 170 | + rw [restrictScalars_adjoin_of_algEquiv (E := K) j rfl, restrictScalars_adjoin] |
| 171 | + exact adjoin.mono _ _ _ Set.subset_union_right |
| 172 | + let i : M →+* L := Subsemiring.inclusion hi |
| 173 | + letI : Algebra M L := i.toAlgebra |
| 174 | + letI : SMul M L := Algebra.toSMul |
| 175 | + haveI : IsScalarTower F M L := IsScalarTower.of_algebraMap_eq (congrFun rfl) |
| 176 | + haveI : IsPurelyInseparable M L := by |
| 177 | + change IsPurelyInseparable M (extendScalars hi) |
| 178 | + obtain ⟨q, _⟩ := ExpChar.exists F |
| 179 | + have : extendScalars hi = adjoin M (E' : Set K) := restrictScalars_injective F <| by |
| 180 | + conv_lhs => rw [extendScalars_restrictScalars, restrictScalars_adjoin_of_algEquiv |
| 181 | + (E := K) j rfl, ← adjoin_self F E', adjoin_adjoin_comm] |
| 182 | + rw [this, isPurelyInseparable_adjoin_iff_pow_mem _ _ q] |
| 183 | + rintro x ⟨y, hy⟩ |
| 184 | + obtain ⟨n, z, hz⟩ := IsPurelyInseparable.pow_mem F q y |
| 185 | + refine ⟨n, algebraMap F M z, ?_⟩ |
| 186 | + rw [← IsScalarTower.algebraMap_apply, IsScalarTower.algebraMap_apply F E K, hz, ← hy, map_pow, |
| 187 | + AlgHom.toRingHom_eq_coe, IsScalarTower.coe_toAlgHom] |
| 188 | + have h := lift_sepDegree_mul_lift_sepDegree_of_isAlgebraic F E L |
| 189 | + rw [IsPurelyInseparable.sepDegree_eq_one F E, Cardinal.lift_one, one_mul] at h |
| 190 | + rw [Cardinal.lift_injective h, ← sepDegree_mul_sepDegree_of_isAlgebraic F M L, |
| 191 | + IsPurelyInseparable.sepDegree_eq_one M L, mul_one] |
| 192 | + |
| 193 | +variable {F K} in |
| 194 | +/-- If `K / E / F` is a field extension tower, such that `E / F` is purely inseparable, then |
| 195 | +for any intermediate field `S` of `K / F` such that `S / F` is algebraic, the `E(S) / E` and |
| 196 | +`S / F` have the same separable degree. -/ |
| 197 | +theorem IntermediateField.sepDegree_adjoin_eq_of_isAlgebraic_of_isPurelyInseparable' |
| 198 | + (S : IntermediateField F K) [Algebra.IsAlgebraic F S] [IsPurelyInseparable F E] : |
| 199 | + sepDegree E (adjoin E (S : Set K)) = sepDegree F S := by |
| 200 | + have : Algebra.IsAlgebraic F (adjoin F (S : Set K)) := by rwa [adjoin_self] |
| 201 | + have := sepDegree_adjoin_eq_of_isAlgebraic_of_isPurelyInseparable (F := F) E (S : Set K) |
| 202 | + rwa [adjoin_self] at this |
| 203 | + |
| 204 | +variable {F K} in |
| 205 | +/-- If `K / E / F` is a field extension tower, such that `E / F` is purely inseparable, then |
| 206 | +for any element `x` of `K` separable over `F`, it has the same minimal polynomials over `F` and |
| 207 | +over `E`. -/ |
| 208 | +theorem minpoly.map_eq_of_isSeparable_of_isPurelyInseparable (x : K) |
| 209 | + (hsep : IsSeparable F x) [IsPurelyInseparable F E] : |
| 210 | + (minpoly F x).map (algebraMap F E) = minpoly E x := by |
| 211 | + have hi := IsSeparable.isIntegral hsep |
| 212 | + have hi' : IsIntegral E x := IsIntegral.tower_top hi |
| 213 | + refine eq_of_monic_of_dvd_of_natDegree_le (monic hi') ((monic hi).map (algebraMap F E)) |
| 214 | + (dvd_map_of_isScalarTower F E x) (le_of_eq ?_) |
| 215 | + have hsep' := IsSeparable.tower_top E hsep |
| 216 | + haveI := (isSeparable_adjoin_simple_iff_isSeparable _ _).2 hsep |
| 217 | + haveI := (isSeparable_adjoin_simple_iff_isSeparable _ _).2 hsep' |
| 218 | + have := Algebra.IsSeparable.isAlgebraic F F⟮x⟯ |
| 219 | + have := Algebra.IsSeparable.isAlgebraic E E⟮x⟯ |
| 220 | + rw [Polynomial.natDegree_map, ← adjoin.finrank hi, ← adjoin.finrank hi', |
| 221 | + ← finSepDegree_eq_finrank_of_isSeparable F _, ← finSepDegree_eq_finrank_of_isSeparable E _, |
| 222 | + finSepDegree_eq, finSepDegree_eq, |
| 223 | + sepDegree_adjoin_eq_of_isAlgebraic_of_isPurelyInseparable (F := F) E] |
| 224 | + |
| 225 | +variable {F} in |
| 226 | +/-- If `E / F` is a purely inseparable field extension, `f` is a separable irreducible polynomial |
| 227 | +over `F`, then it is also irreducible over `E`. -/ |
| 228 | +theorem Polynomial.Separable.map_irreducible_of_isPurelyInseparable {f : F[X]} (hsep : f.Separable) |
| 229 | + (hirr : Irreducible f) [IsPurelyInseparable F E] : Irreducible (f.map (algebraMap F E)) := by |
| 230 | + let K := AlgebraicClosure E |
| 231 | + obtain ⟨x, hx⟩ := IsAlgClosed.exists_aeval_eq_zero K f |
| 232 | + (natDegree_pos_iff_degree_pos.1 hirr.natDegree_pos).ne' |
| 233 | + have ha : Associated f (minpoly F x) := by |
| 234 | + have := isUnit_C.2 (leadingCoeff_ne_zero.2 hirr.ne_zero).isUnit.inv |
| 235 | + exact ⟨this.unit, by rw [IsUnit.unit_spec, minpoly.eq_of_irreducible hirr hx]⟩ |
| 236 | + have ha' : Associated (f.map (algebraMap F E)) ((minpoly F x).map (algebraMap F E)) := |
| 237 | + ha.map (mapRingHom (algebraMap F E)).toMonoidHom |
| 238 | + have heq := minpoly.map_eq_of_isSeparable_of_isPurelyInseparable E x (ha.separable hsep) |
| 239 | + rw [ha'.irreducible_iff, heq] |
| 240 | + exact minpoly.irreducible (Algebra.IsIntegral.isIntegral x) |
| 241 | + |
| 242 | +end TowerLaw |
0 commit comments