Tower law for purely inseparable extensions

This file contains results related to Field.finIsepDegree and the tower law.

Main results

• Field.lift_sepDegree_mul_lift_sepDegree_of_isAlgebraic: the separable degrees satisfy the tower law: $[E:F]_s [K:E]_s = [K:F]_s$.

• IntermediateField.sepDegree_adjoin_eq_of_isAlgebraic_of_isPurelyInseparable, IntermediateField.sepDegree_adjoin_eq_of_isAlgebraic_of_isPurelyInseparable': if K / E / F is a field extension tower, such that E / F is purely inseparable, then for any subset S of K such that F(S) / F is algebraic, the E(S) / E and F(S) / F have the same separable degree. In particular, if S is an intermediate field of K / F such that S / F is algebraic, the E(S) / E and S / F have the same separable degree.

• minpoly.map_eq_of_isSeparable_of_isPurelyInseparable: if K / E / F is a field extension tower, such that E / F is purely inseparable, then for any element x of K separable over F, it has the same minimal polynomials over F and over E.

• Polynomial.Separable.map_irreducible_of_isPurelyInseparable: if E / F is purely inseparable, f is a separable irreducible polynomial over F, then it is also irreducible over E.

Tags

separable degree, degree, separable closure, purely inseparable

TODO

• Restate some intermediate result in terms of linearly disjointness.

• Prove that the inseparable degrees satisfy the tower law: $[E:F]_i [K:E]_i = [K:F]_i$. Probably an argument using linearly disjointness is needed.

theorem LinearIndependent.map_of_isPurelyInseparable_of_isSeparable {F : Type u} (E : Type v) [Field F] [Field E] [Algebra F E] {K : Type w} [Field K] [Algebra F K] [Algebra E K] [IsScalarTower F E K] [IsPurelyInseparable F E] {ι : Type u_1} {v : ι → K} (hsep : ∀ (i : ι), IsSeparable F (v i)) (h : LinearIndependent F v) : LinearIndependent E v

If K / E / F is a field extension tower such that E / F is purely inseparable, if { u_i } is a family of separable elements of K which is F-linearly independent, then it is also E-linearly independent.

theorem Field.sepDegree_eq_of_isPurelyInseparable_of_isSeparable (F : Type u) (E : Type v) [Field F] [Field E] [Algebra F E] (K : Type w) [Field K] [Algebra F K] [Algebra E K] [IsScalarTower F E K] [IsPurelyInseparable F E] [Algebra.IsSeparable E K] : sepDegree F K = Module.rank E K

If K / E / F is a field extension tower, such that E / F is purely inseparable and K / E is separable, then the separable degree of K / F is equal to the degree of K / E. It is a special case of Field.lift_sepDegree_mul_lift_sepDegree_of_isAlgebraic, and is an intermediate result used to prove it.

theorem Field.lift_rank_mul_lift_sepDegree_of_isSeparable (F : Type u) (E : Type v) [Field F] [Field E] [Algebra F E] (K : Type w) [Field K] [Algebra F K] [Algebra E K] [IsScalarTower F E K] [Algebra.IsSeparable F E] : Cardinal.lift.{w, v} (Module.rank F E) * Cardinal.lift.{v, w} (sepDegree E K) = Cardinal.lift.{v, w} (sepDegree F K)

If K / E / F is a field extension tower, such that E / F is separable, then $[E:F] [K:E]_s = [K:F]_s$. It is a special case of Field.lift_sepDegree_mul_lift_sepDegree_of_isAlgebraic, and is an intermediate result used to prove it.

theorem Field.rank_mul_sepDegree_of_isSeparable (F : Type u) (E : Type v) [Field F] [Field E] [Algebra F E] (K : Type v) [Field K] [Algebra F K] [Algebra E K] [IsScalarTower F E K] [Algebra.IsSeparable F E] : Module.rank F E * sepDegree E K = sepDegree F K

The same-universe version of Field.lift_rank_mul_lift_sepDegree_of_isSeparable.

theorem Field.sepDegree_eq_of_isPurelyInseparable (F : Type u) (E : Type v) [Field F] [Field E] [Algebra F E] (K : Type w) [Field K] [Algebra F K] [Algebra E K] [IsScalarTower F E K] [IsPurelyInseparable F E] : sepDegree F K = sepDegree E K

If K / E / F is a field extension tower, such that E / F is purely inseparable, then $[K:F]_s = [K:E]_s$. It is a special case of Field.lift_sepDegree_mul_lift_sepDegree_of_isAlgebraic, and is an intermediate result used to prove it.

theorem Field.lift_sepDegree_mul_lift_sepDegree_of_isAlgebraic (F : Type u) (E : Type v) [Field F] [Field E] [Algebra F E] (K : Type w) [Field K] [Algebra F K] [Algebra E K] [IsScalarTower F E K] [Algebra.IsAlgebraic F E] : Cardinal.lift.{w, v} (sepDegree F E) * Cardinal.lift.{v, w} (sepDegree E K) = Cardinal.lift.{v, w} (sepDegree F K)

If K / E / F is a field extension tower, such that E / F is algebraic, then their separable degrees satisfy the tower law: $[E:F]_s [K:E]_s = [K:F]_s$.

theorem Field.sepDegree_mul_sepDegree_of_isAlgebraic (F : Type u) (E : Type v) [Field F] [Field E] [Algebra F E] (K : Type v) [Field K] [Algebra F K] [Algebra E K] [IsScalarTower F E K] [Algebra.IsAlgebraic F E] : sepDegree F E * sepDegree E K = sepDegree F K

The same-universe version of Field.lift_sepDegree_mul_lift_sepDegree_of_isAlgebraic.

Stacks Tag 09HK (Part 1)

theorem IntermediateField.sepDegree_adjoin_eq_of_isAlgebraic_of_isPurelyInseparable {F : Type u} (E : Type v) [Field F] [Field E] [Algebra F E] {K : Type w} [Field K] [Algebra F K] [Algebra E K] [IsScalarTower F E K] (S : Set K) [Algebra.IsAlgebraic F ↥(adjoin F S)] [IsPurelyInseparable F E] : Field.sepDegree E ↥(adjoin E S) = Field.sepDegree F ↥(adjoin F S)

If K / E / F is a field extension tower, such that E / F is purely inseparable, then for any subset S of K such that F(S) / F is algebraic, the E(S) / E and F(S) / F have the same separable degree.

theorem IntermediateField.sepDegree_adjoin_eq_of_isAlgebraic_of_isPurelyInseparable' {F : Type u} (E : Type v) [Field F] [Field E] [Algebra F E] {K : Type w} [Field K] [Algebra F K] [Algebra E K] [IsScalarTower F E K] (S : IntermediateField F K) [Algebra.IsAlgebraic F ↥S] [IsPurelyInseparable F E] : Field.sepDegree E ↥(adjoin E ↑S) = Field.sepDegree F ↥S

If K / E / F is a field extension tower, such that E / F is purely inseparable, then for any intermediate field S of K / F such that S / F is algebraic, the E(S) / E and S / F have the same separable degree.

theorem minpoly.map_eq_of_isSeparable_of_isPurelyInseparable {F : Type u} (E : Type v) [Field F] [Field E] [Algebra F E] {K : Type w} [Field K] [Algebra F K] [Algebra E K] [IsScalarTower F E K] (x : K) (hsep : IsSeparable F x) [IsPurelyInseparable F E] : Polynomial.map (algebraMap F E) (minpoly F x) = minpoly E x

If K / E / F is a field extension tower, such that E / F is purely inseparable, then for any element x of K separable over F, it has the same minimal polynomials over F and over E.

theorem Polynomial.Separable.map_irreducible_of_isPurelyInseparable {F : Type u} (E : Type v) [Field F] [Field E] [Algebra F E] {f : Polynomial F} (hsep : f.Separable) (hirr : Irreducible f) [IsPurelyInseparable F E] : Irreducible (Polynomial.map (algebraMap F E) f)

If E / F is a purely inseparable field extension, f is a separable irreducible polynomial over F, then it is also irreducible over E.