Minimal polynomials over a relatively algebraically closed base field

Let F / k be a field extension in which k is relatively algebraically closed, that is, IsIntegrallyClosedIn k F — equivalently algebraicClosure k F = ⊥ — and let E be a further commutative F-algebra. An element x of E algebraic over k then has the same minimal polynomial over F as over k: the coefficients of minpoly F x are integral over k, because that polynomial divides the monic polynomial (minpoly k x).map (algebraMap k F), and relative algebraic closedness puts them back into k.

Consequently, for E a field, F⟮x⟯ / F and k⟮x⟯ / k have the same degree. This is the mechanism behind the degree behaviour of a constant field extension: adjoining constants to F costs exactly what adjoining them to k costs. More strongly, every separable extension of k inside E is linearly disjoint from F, and a linearly independent family of separable constants over k stays linearly independent over F. Linear disjointness also shows that the compositum F · k' with a separable extension k' of k acquires no new separable constants: an element of F · k' separable over k' already lies in k'.

Main results

• TauCeti.minpoly.map_algebraMap_of_isIntegrallyClosedIn: minpoly F x is the image of minpoly k x.
• TauCeti.IntermediateField.finrank_adjoin_simple_eq_finrank_adjoin_simple_of_isIntegrallyClosedIn : [F⟮x⟯ : F] = [k⟮x⟯ : k].
• TauCeti.linearDisjoint_fieldRange_of_isIntegrallyClosedIn: a separable extension of k inside a common overfield is linearly disjoint from F.
• TauCeti.linearIndependent_algebraMap_comp_of_isIntegrallyClosedIn: a linearly independent family of separable elements stays linearly independent after extending scalars from k to F.
• TauCeti.linearIndependent_algebraMap_comp_of_isIntegrallyClosedIn_of_isSeparable: a linearly independent family in F stays linearly independent after extending scalars from k to a separable extension k'.
• TauCeti.relfinrank_sup_adjoin_simple_eq_relfinrank_adjoin_simple_of_isIntegrallyClosedIn: [F · k' : k'(x)] = [F : k(x)] for x ∈ F and finite separable k'/k.
• TauCeti.IntermediateField.eq_of_le_of_adjoin_le_of_isIntegrallyClosedIn: a finite separable extension of k inside E is determined by its compositum with F.
• TauCeti.mem_range_algebraMap_of_mem_adjoin_of_isSeparable_of_isIntegrallyClosedIn: an element of the compositum F · k' separable over k' lies in k'.

References

• H. Stichtenoth, Algebraic Function Fields and Codes, 2nd ed., GTM 254, Springer, 2009, Section III.6. This is the field theory behind the persistence of linear independence under a constant field extension (Proposition 3.6.1(b)) and behind the determination of the constant field of a constant field extension (Proposition 3.6.1(a)) and the degree identity (Proposition 3.6.1(c)); it is stated here for an arbitrary extension F / k with k relatively algebraically closed, with no function field involved.

theorem TauCeti.minpoly.map_algebraMap_of_isIntegrallyClosedIn {k : Type u} {F : Type v} {E : Type w} [Field k] [Field F] [Algebra k F] [CommRing E] [Algebra k E] [Algebra F E] [IsScalarTower k F E] (hex : IsIntegrallyClosedIn k F) {x : E} (hx : IsIntegral k x) : Polynomial.map (algebraMap k F) (minpoly k x) = minpoly F x

If k is relatively algebraically closed in F, then an element of an extension of F that is algebraic over k has the same minimal polynomial over F as over k.

Without the hypothesis only the divisibility minpoly F x ∣ (minpoly k x).map (algebraMap k F) holds; the content is that the coefficients of the left-hand factor, being integral over k and lying in F, are constants.

theorem TauCeti.IntermediateField.finrank_adjoin_simple_eq_finrank_adjoin_simple_of_isIntegrallyClosedIn {k : Type u} {F : Type v} {E : Type w} [Field k] [Field F] [Algebra k F] [Field E] [Algebra k E] [Algebra F E] [IsScalarTower k F E] (hex : IsIntegrallyClosedIn k F) {x : E} (hx : IsIntegral k x) : Module.finrank F ↥F⟮x⟯ = Module.finrank k ↥k⟮x⟯

If k is relatively algebraically closed in F, then adjoining an element algebraic over k to F raises the degree by exactly as much as adjoining it to k does.

Linear disjointness from a separable extension

theorem TauCeti.linearDisjoint_fieldRange_of_isIntegrallyClosedIn {k : Type u} {F : Type v} {E : Type w} [Field k] [Field F] [Algebra k F] [Field E] [Algebra k E] [Algebra F E] [IsScalarTower k F E] {k' : Type u_1} [Field k'] [Algebra k k'] [Algebra k' E] [IsScalarTower k k' E] (hex : IsIntegrallyClosedIn k F) [Algebra.IsSeparable k k'] : (IsScalarTower.toAlgHom k k' E).fieldRange.LinearDisjoint F

A separable extension k' of a relatively algebraically closed field k is linearly disjoint from F inside any common overfield E.

Consequently the compositum of F and k' inside E behaves like F ⊗[k] k': for finite k' / k it has degree [k' : k] over F. This is the field-theoretic content of Stichtenoth, Proposition 3.6.1(b), for separable constant field extensions.

theorem TauCeti.linearIndependent_algebraMap_comp_of_isIntegrallyClosedIn {k : Type u} {F : Type v} {E : Type w} [Field k] [Field F] [Algebra k F] [Field E] [Algebra k E] [Algebra F E] [IsScalarTower k F E] {k' : Type u_1} [Field k'] [Algebra k k'] [Algebra k' E] [IsScalarTower k k' E] (hex : IsIntegrallyClosedIn k F) {ι : Type u_2} {v : ι → k'} (hsep : ∀ (i : ι), IsSeparable k (v i)) (hv : LinearIndependent k v) : LinearIndependent F (⇑(algebraMap k' E) ∘ v)

A linearly independent family of separable elements over a relatively algebraically closed field k remains linearly independent after extending scalars to F inside a common overfield.

For an algebraic function field and a separable constant field extension, this is Stichtenoth, Proposition 3.6.1(b).

theorem TauCeti.linearIndependent_algebraMap_comp_of_isIntegrallyClosedIn_of_isSeparable {k : Type u} {F : Type v} {E : Type w} [Field k] [Field F] [Algebra k F] [Field E] [Algebra k E] [Algebra F E] [IsScalarTower k F E] {k' : Type u_1} [Field k'] [Algebra k k'] [Algebra k' E] [IsScalarTower k k' E] (hex : IsIntegrallyClosedIn k F) [Algebra.IsSeparable k k'] {ι : Type u_2} {v : ι → F} (hv : LinearIndependent k v) : LinearIndependent k' (⇑(algebraMap F E) ∘ v)

Linear independence over k persists over a separable extension k' (Stichtenoth, Proposition 3.6.1(b)): if k is relatively algebraically closed in F and k' / k is separable, then a family of elements of F linearly independent over k stays linearly independent over k' inside a common overfield E.

This is the companion of TauCeti.linearIndependent_algebraMap_comp_of_isIntegrallyClosedIn, which extends scalars on the other side of the linearly disjoint pair F, k'.

Constants of the compositum

theorem TauCeti.IntermediateField.eq_of_le_of_adjoin_le_of_isIntegrallyClosedIn {k : Type u} {F : Type v} {E : Type w} [Field k] [Field F] [Algebra k F] [Field E] [Algebra k E] [Algebra F E] [IsScalarTower k F E] (hex : IsIntegrallyClosedIn k F) {K₀ K₁ : IntermediateField k E} [FiniteDimensional k ↥K₁] [Algebra.IsSeparable k ↥K₁] (hle : K₀ ≤ K₁) (h : IntermediateField.adjoin F ↑K₁ ≤ IntermediateField.adjoin F ↑K₀) : K₀ = K₁

A finite separable extension of a relatively algebraically closed field is determined by its compositum with F: if K₀ ≤ K₁ are finite separable extensions of k inside E and the compositum F · K₁ is contained in F · K₀, then K₀ = K₁.

Linear disjointness gives [F · Kᵢ : F] = [Kᵢ : k], so the two composita being equal forces the two degrees over k to agree.

theorem TauCeti.mem_range_algebraMap_of_mem_adjoin_of_isSeparable_of_isIntegrallyClosedIn {k : Type u} {F : Type v} {E : Type w} [Field k] [Field F] [Algebra k F] [Field E] [Algebra k E] [Algebra F E] [IsScalarTower k F E] {k' : Type u_1} [Field k'] [Algebra k k'] [Algebra k' E] [IsScalarTower k k' E] (hex : IsIntegrallyClosedIn k F) [Algebra.IsSeparable k k'] {z : E} (hz : z ∈ IntermediateField.adjoin F (Set.range ⇑(algebraMap k' E))) (hsep : IsSeparable k' z) : z ∈ Set.range ⇑(algebraMap k' E)

A separable constant of the compositum F · k' is a constant of k': if k is relatively algebraically closed in F and k' / k is separable algebraic, then every element of the compositum of F and k' inside a common overfield E that is separable over k' already lies in k'.

For an algebraic function field and a separable constant field extension, this is the content of Stichtenoth, Proposition 3.6.1(a), stated with separability of the constant in place of perfectness of k; over a perfect k every constant is separable.

theorem TauCeti.relfinrank_sup_adjoin_simple_eq_relfinrank_adjoin_simple_of_isIntegrallyClosedIn {k : Type u} {F : Type v} {E : Type w} [Field k] [Field F] [Algebra k F] [Field E] [Algebra k E] [Algebra F E] [IsScalarTower k F E] (hex : IsIntegrallyClosedIn k F) (A : IntermediateField k E) [FiniteDimensional k ↥A] [Algebra.IsSeparable k ↥A] (h : A ⊔ (IsScalarTower.toAlgHom k F E).fieldRange = ⊤) (x : F) : (A ⊔ k⟮(algebraMap F E) x⟯).relfinrank ⊤ = k⟮x⟯.relfinrank ⊤

For k relatively algebraically closed in F, A/k finite separable, and E = A · F (inside E), the degrees satisfy [E : A(x)] = [F : k(x)] for every x ∈ F. This is the finite separable case of Stichtenoth, Algebraic Function Fields and Codes, second edition, Proposition 3.6.1(c).

For the scalar-tower formulation with constantCompositum, see TauCeti.finrank_over_adjoin_simple_eq_of_constantCompositum_eq_top in TauCeti.FieldTheory.FunctionField.ConstantExtension.Degree.