Algebraic elements lie in a common number field

Two elements of a field of characteristic zero that are algebraic over ℚ generate a finite extension ℚ⟮x, y⟯ of ℚ, which is a number field; more generally, so do the coordinates of a finite tuple of algebraic elements. This reduces statements about pairs and tuples of algebraic numbers in an arbitrary characteristic-zero field to the number-field API. The generated fields are transported along field homomorphisms by TauCeti.adjoinRangeMapEquiv.

Main results

• TauCeti.exists_numberField_mem: two algebraic elements of F lie in a common intermediate number field.
• TauCeti.exists_numberField_comp: a finite tuple of algebraic elements of F is the image of a tuple in an intermediate number field.
• TauCeti.adjoinRangeMapEquiv: transport of a tuple's generated field along a homomorphism of characteristic-zero fields.

noncomputable def TauCeti.adjoinRangeMapEquiv {F : Type u_1} {F' : Type u_2} {ι : Type u_3} [Field F] [CharZero F] [Field F'] [CharZero F'] (x : ι → F) (f : F →+* F') : ↥(IntermediateField.adjoin ℚ (Set.range x)) ≃ₐ[ℚ] ↥(IntermediateField.adjoin ℚ (Set.range (⇑f ∘ x)))

A field homomorphism restricts to a ℚ-algebra isomorphism between the fields generated by a tuple and its image. No finiteness or algebraicity assumption on the tuple is needed.

@[simp]

theorem TauCeti.coe_adjoinRangeMapEquiv_apply {F : Type u_1} {F' : Type u_2} {ι : Type u_3} [Field F] [CharZero F] [Field F'] [CharZero F'] (x : ι → F) (f : F →+* F') (y : ↥(IntermediateField.adjoin ℚ (Set.range x))) : ↑((adjoinRangeMapEquiv x f) y) = f ↑y

The restricted isomorphism acts on elements by the original field homomorphism.

theorem TauCeti.exists_numberField_mem {F : Type u_1} [Field F] [CharZero F] {x y : F} (hx : IsAlgebraic ℚ x) (hy : IsAlgebraic ℚ y) : ∃ (K : IntermediateField ℚ F) (_ : NumberField ↥K) (a : ↥K) (b : ↥K), ↑a = x ∧ ↑b = y

Two algebraic elements of F lie in a common intermediate number field.

theorem TauCeti.exists_numberField_comp {F : Type u_1} [Field F] [CharZero F] {ι : Type u_2} [Finite ι] {x : ι → F} (hx : ∀ (i : ι), IsAlgebraic ℚ (x i)) : ∃ (E : IntermediateField ℚ F) (_ : NumberField ↥E) (y : ι → ↥E), ⇑(algebraMap (↥E) F) ∘ y = x

A finite tuple of algebraic elements of F is the image of a tuple in an intermediate number field, namely the field generated by its coordinates.