A primitive element that is a linear combination of given generators

A field-theoretic tool for the local parametrization theorem ([GR84, Chapter 3, §1]; the second alternative of [Fre17, Ch. I, 8.2]). The classical primitive element theorem (Mathlib's Field.exists_primitive_element) returns some generator of a finite separable extension; the parametrization needs the generator to be a linear combination ∑ c_j • β_j of the given generators β_j (the classes of the fibre coordinates) with constant coefficients c_j ∈ ℂ, not elements of the function field Frac 𝒪_d, and coefficient 1 on a chosen one, because it is realised as a coordinate after a linear change of coordinates of ℂⁿ. The coefficients are therefore drawn from an infinite subfield C given by a ring map ϕ : C →+* F.

The argument is the one Mathlib uses for extensions with finitely many intermediate fields (Field.primitive_element_inf_aux_of_finite_intermediateField, private): over an infinite field F, among the fields F⟮α + x • β⟯ (x : F) two coincide, and then β, hence α, lies in that field. Finitely many intermediate fields is Artin's theorem for a finite separable extension (Field.finite_intermediateField_of_exists_primitive_element), applied to the subfield generated by the β_j. Routine field theory, recorded so that the parametrization theorem rests only on Mathlib and the Weierstrass theory.

theorem Analytic.exists_adjoin_pair_eq_adjoin_add_smul {F : Type u_1} {E : Type u_2} [Field F] [Field E] [Algebra F E] {C : Type u_3} [Field C] [Infinite C] (ϕ : C →+* F) [Finite (IntermediateField F E)] (α β : E) : ∃ (x : C), F⟮α, β⟯ = F⟮α + ϕ x • β⟯

The argument of Mathlib's private Field.primitive_element_inf_aux_of_finite_intermediateField, with the generator α + ϕ x • β exposed and the coefficient drawn from a subfield: if E / F has finitely many intermediate fields and ϕ : C →+* F is a ring map from an infinite field C (the constants ℂ inside the function field Frac 𝒪_d), then for all α β : E some x : C has F⟮α, β⟯ = F⟮α + ϕ x • β⟯.

theorem Analytic.exists_linear_primitive_aux {F : Type u_1} {E : Type u_2} [Field F] [Field E] [Algebra F E] {C : Type u_3} [Field C] [Infinite C] (ϕ : C →+* F) [Finite (IntermediateField F E)] {ι : Type u_4} [DecidableEq ι] (β : ι → E) (i₀ : ι) (t : Finset ι) (hi₀ : i₀ ∉ t) : ∃ (c : ι → C), c i₀ = 1 ∧ (∀ i ∉ insert i₀ t, c i = 0) ∧ ∀ i ∈ insert i₀ t, β i ∈ F⟮∑ j ∈ insert i₀ t, ϕ (c j) • β j⟯

Iterating exists_adjoin_pair_eq_adjoin_add_smul over a finite family β indexed by insert i₀ t (i₀ ∉ t): a linear combination ∑ ϕ (c j) • β_j with coefficients c in the subfield C, c i₀ = 1 and c = 0 off the index set, generates a field containing every β_i, i ∈ insert i₀ t.

theorem Analytic.exists_linear_primitive_of_isIntegral {F : Type u_1} {E : Type u_2} [Field F] [Field E] [Algebra F E] [CharZero F] {C : Type u_3} [Field C] (ϕ : C →+* F) {ι : Type u_4} (s : Finset ι) (β : ι → E) (hβ : ∀ i ∈ s, IsIntegral F (β i)) {i₀ : ι} (hi₀ : i₀ ∈ s) : ∃ (c : ι → C), c i₀ = 1 ∧ (∀ i ∉ s, c i = 0) ∧ ∀ i ∈ s, β i ∈ F⟮∑ j ∈ s, ϕ (c j) • β j⟯

In characteristic zero, a finite family β of elements of E integral over F, indexed by a finset s with a distinguished i₀ ∈ s, admits coefficients c : ι → C in a subfield C (given by ϕ : C →+* F) with c i₀ = 1, c = 0 off s, such that every β_i (i ∈ s) lies in F⟮∑ j ∈ s, ϕ (c j) • β j⟯: a primitive element of F(β_i : i ∈ s) that is a C-linear combination of the generators. The primitive element theorem (Artin) gives finitely many intermediate fields of F(β_i : i ∈ s) / F, and the pair lemma is iterated inside that field.