Field extensions generated by a set

Complements on IntermediateField.adjoin F s = ⊤, the statement that a set s generates a field extension E / F: three independent consequences of it, and one criterion for it.

Extensionality. An F-algebra automorphism of E fixing every element of s is the identity. This is the whole-field counterpart of Mathlib's IntermediateField.algHom_ext_of_eq_adjoin (which compares homomorphisms out of the subfield adjoin F s), obtained from it by transporting along adjoin F s ≃ₐ[F] E rather than repeating the adjoin induction. It is the extensionality step shared by the multiquadratic arguments: the splitting law shows a decomposition-group element fixes every generator √dᵢ and concludes it is trivial, and the Frobenius computation concludes the same when every Legendre symbol is 1.

Changing the base of a generated extension. For a tower K ⊆ L ⊆ M in which a set t generates M over L, the compositum of K(t) — generated over the bottom of the tower — with the image of L is already all of M. That is the shape every compositum argument over the base K needs, because Mathlib's engines (IntermediateField.fixingSubgroup_sup, IntermediateField.normal_sup, and the linear-disjointness API) all take two intermediate fields of a single extension M / K together with a hypothesis that their join is ⊤. Dually, if s generates L over K and ι : L →ₐ[K] M lands in a tower K ⊆ F ⊆ M, then over F the image of ι and the image of s generate the same field; this is how a primitive element of L / K becomes one of a base change of L. Conversely, if M is the compositum over K of the images of F and ι, then the image of ι generates M over F.

Generation from an algebra generator. If a ring S is generated as an R-algebra by a single element β, then the fraction field L of S is generated by the image of β over any field K between R and L, because every element of L is a ratio of two elements of R[β]. This is how a generator of an extension of integer rings becomes a primitive element of the extension of fraction fields.

Main results

• TauCeti.IntermediateField.algHom_ext_of_adjoin_eq_top: algebra homomorphisms into any semiring are determined by their values on a generating set.
• TauCeti.IntermediateField.algEquiv_ext_of_adjoin_eq_top: two automorphisms agreeing on a generating set are equal.
• TauCeti.IntermediateField.algEquiv_eq_one_of_adjoin_eq_top: an automorphism fixing each element of a generating set is 1.
• TauCeti.IntermediateField.adjoin_adjoinSimpleGen_eq_top: the distinguished generator of a simple adjoin generates that field.
• TauCeti.IntermediateField.adjoin_sup_fieldRange_eq_top: for a tower K ⊆ L ⊆ M in which t generates M over L, the compositum K(t) ⊔ L is ⊤ inside M.
• TauCeti.IntermediateField.adjoin_range_eq_adjoin_image: over any intermediate base, the image of a K-embedding of L generates the same field as the image of a generating set of L/K.
• TauCeti.IntermediateField.adjoin_range_eq_top_of_fieldRange_sup_fieldRange_eq_top: a compositum is generated over one factor by the other.
• TauCeti.IntermediateField.adjoin_eq_top_of_algebra_adjoin_eq_top: an algebra generator of a domain also generates its fraction field over any intermediate base field.

Generating sets

The compositum criterion allows an arbitrary set of field generators, so it applies to extensions that need several generators or contain transcendental elements. It expresses generation over a larger base as generation by the same set together with that base inside a single extension. For a cyclotomic extension, the singleton consisting of a primitive root suffices; its algebra generation hypothesis implies field generation by IntermediateField.adjoin_eq_top_of_algebra.

adjoin_sup_fieldRange_eq_top is adapted from the Birkbeck–Brasca Chebotarev density project, where the step is inlined into a larger adjoin_induction.

theorem TauCeti.IntermediateField.algHom_ext_of_adjoin_eq_top {F : Type u_1} {E : Type u_2} [Field F] [Field E] [Algebra F E] {s : Set E} {E₂ : Type u_3} [Semiring E₂] [Algebra F E₂] (htop : IntermediateField.adjoin F s = ⊤) {σ τ : E →ₐ[F] E₂} (h : ∀ x ∈ s, σ x = τ x) : σ = τ

Two algebra homomorphisms agreeing on a generating set are equal. If s generates E over F (IntermediateField.adjoin F s = ⊤) and F-algebra maps σ, τ : E →ₐ[F] E₂ (into any semiring E₂) agree on every element of s, then σ = τ. This is the whole-field, two-map counterpart of Mathlib's IntermediateField.algHom_ext_of_eq_adjoin.

theorem TauCeti.IntermediateField.algEquiv_ext_of_adjoin_eq_top {F : Type u_1} {E : Type u_2} [Field F] [Field E] [Algebra F E] {s : Set E} (htop : IntermediateField.adjoin F s = ⊤) {σ τ : Gal(E/F)} (h : ∀ x ∈ s, σ x = τ x) : σ = τ

Two F-algebra automorphisms of E agreeing on a generating set are equal.

theorem TauCeti.IntermediateField.algEquiv_eq_one_of_adjoin_eq_top {F : Type u_1} {E : Type u_2} [Field F] [Field E] [Algebra F E] {s : Set E} (htop : IntermediateField.adjoin F s = ⊤) {σ : Gal(E/F)} (hfix : ∀ x ∈ s, σ x = x) : σ = 1

An F-algebra automorphism of E that fixes every element of a set generating E over F is the identity. This is TauCeti.IntermediateField.algEquiv_ext_of_adjoin_eq_top against the identity.

theorem TauCeti.IntermediateField.adjoin_adjoinSimpleGen_eq_top {F : Type u_1} {E : Type u_2} [Field F] [Field E] [Algebra F E] (x : E) : F⟮IntermediateField.AdjoinSimple.gen F x⟯ = ⊤

The distinguished generator of F⟮x⟯, viewed as an element of that field, generates F⟮x⟯ over F.

theorem TauCeti.IntermediateField.adjoin_sup_fieldRange_eq_top (K : Type u_3) (L : Type u_4) (M : Type u_5) [Field K] [Field L] [Field M] [Algebra K L] [Algebra K M] [Algebra L M] [IsScalarTower K L M] {t : Set M} (hadj : IntermediateField.adjoin L t = ⊤) : IntermediateField.adjoin K t ⊔ (IsScalarTower.toAlgHom K L M).fieldRange = ⊤

The compositum step. If a set t generates M over L, then inside M the compositum of K(t) with the image of L is all of M, for any base field K of the tower. This is the input to Mathlib's compositum engines (IntermediateField.fixingSubgroup_sup, IntermediateField.normal_sup). The single-generator case t = {ζ} is the one the cyclotomic compositum uses; it is obtained by specialisation.

theorem TauCeti.IntermediateField.adjoin_range_eq_adjoin_image {K : Type u_3} {L : Type u_4} {F : Type u_5} {M : Type u_6} [Field K] [Field L] [Field F] [Field M] [Algebra K L] [Algebra K F] [Algebra F M] [Algebra K M] [IsScalarTower K F M] (ι : L →ₐ[K] M) {s : Set L} (hs : IntermediateField.adjoin K s = ⊤) : IntermediateField.adjoin F (Set.range ⇑ι) = IntermediateField.adjoin F (⇑ι '' s)

Generators of a base-changed image. If s generates L over K, then for any tower K ⊆ F ⊆ M and K-embedding ι : L →ₐ[K] M, the field generated over F by the image of ι is already generated by the image of s.

theorem TauCeti.IntermediateField.adjoin_range_eq_top_of_fieldRange_sup_fieldRange_eq_top {K : Type u_3} {E : Type u_4} {L : Type u_5} {M : Type u_6} [Field K] [Field E] [Field L] [Field M] [Algebra K E] [Algebra K L] [Algebra E M] [Algebra K M] [IsScalarTower K E M] (ι : L →ₐ[K] M) (h : (IsScalarTower.toAlgHom K E M).fieldRange ⊔ ι.fieldRange = ⊤) : IntermediateField.adjoin E (Set.range ⇑ι) = ⊤

A compositum is generated over one factor by the other. For a tower K ⊆ E ⊆ M and a K-embedding ι : L →ₐ[K] M, if M is the compositum over K of the images of E and L, then M is generated over E by the image of ι.

theorem TauCeti.IntermediateField.adjoin_eq_top_of_algebra_adjoin_eq_top {R : Type u_3} {S : Type u_4} {K : Type u_5} {L : Type u_6} [CommSemiring R] [CommRing S] [Field K] [Field L] [Algebra R S] [Algebra R K] [Algebra R L] [Algebra S L] [Algebra K L] [IsScalarTower R S L] [IsScalarTower R K L] [IsFractionRing S L] {β : S} (h : R[β] = ⊤) : K⟮(algebraMap S L) β⟯ = ⊤

If S is generated as an R-algebra by a single element β, then the fraction field L of S is generated by the image of β over any field K sitting between R and L: every element of L is a ratio of two elements of R[β].