Isomorphisms out of the rational function field are its generators

A k-algebra homomorphism out of k(X) is determined by the image of X, because k(X) is the fraction field of k[X]. For an isomorphism k(X) ≃ L that image generates L over k, and conversely, when L / k is transcendental, every generator of L over k is the image of X under an isomorphism; such a generator is automatically transcendental. So the isomorphisms k(X) ≃ L over k correspond to the generators of L over k, and in particular the automorphisms of k(X) over k correspond to the generators of k(X) over k.

This is the computational form of Aut(k(x)/k), and the starting point for identifying it with the group of linear fractional transformations: a generator is a quotient of polynomials of degree at most one with nonzero determinant.

Main definitions

• RatFunc.algEquivOfAdjoinEqTop: the isomorphism k(X) ≃ L sending X to a given generator.
• RatFunc.algEquivEquivGenerator: the resulting bijection between the isomorphisms k(X) ≃ L over k and the generators of L over k.

Main results

• RatFunc.algHom_ext and RatFunc.algEquiv_ext: a k-algebra homomorphism, or isomorphism, out of k(X) is determined by the image of X.
• RatFunc.adjoin_apply_X_eq_top: the image of X under an isomorphism generates the target.
• RatFunc.transcendental_apply_X: the image of X under an injective homomorphism is transcendental.

Provenance

algEquivOfAdjoinEqTop composes Mathlib's RatFunc.algEquivOfTranscendental, which identifies k(X) with k⟮f⟯ for a transcendental f, with the identification of k⟮f⟯ = ⊤ with L. Mathlib's RatFunc.Luroth.algEquiv composes those same two steps for an arbitrary nontrivial intermediate field E, and RatFunc.Luroth.algEquiv_X evaluates it: it sends X to the generator of E that Lüroth's theorem produces. What is specific here is that the generator is an arbitrary given generator of all of L, so the result is an isomorphism onto L, and that the correspondence is packaged as the bijection algEquivEquivGenerator.

References

• H. Stichtenoth, Algebraic Function Fields and Codes, 2nd ed., GTM 254, Springer, 2009, Exercise 1.2.

theorem RatFunc.algHom_ext {K : Type u_1} [CommRing K] [IsDomain K] {L : Type u_2} [Semiring L] [Algebra K L] {σ τ : RatFunc K →ₐ[K] L} (h : σ X = τ X) : σ = τ

A homomorphism out of k(X) is determined by the image of X: the polynomials k[X] are generated by X, and k(X) is their fraction field.

theorem RatFunc.algHom_ext_iff {K : Type u_1} [CommRing K] [IsDomain K] {L : Type u_2} [Semiring L] [Algebra K L] {σ τ : RatFunc K →ₐ[K] L} : σ = τ ↔ σ X = τ X

theorem RatFunc.algEquiv_ext {K : Type u_1} [CommRing K] [IsDomain K] {L : Type u_2} [Semiring L] [Algebra K L] {σ τ : RatFunc K ≃ₐ[K] L} (h : σ X = τ X) : σ = τ

An isomorphism out of k(X) is determined by the image of X, the AlgEquiv form of RatFunc.algHom_ext.

theorem RatFunc.algEquiv_ext_iff {K : Type u_1} [CommRing K] [IsDomain K] {L : Type u_2} [Semiring L] [Algebra K L] {σ τ : RatFunc K ≃ₐ[K] L} : σ = τ ↔ σ X = τ X

theorem RatFunc.transcendental_apply_X {K : Type u_1} [CommRing K] [IsDomain K] {M : Type u_3} [Ring M] [Algebra K M] (σ : RatFunc K →ₐ[K] M) (hσ : Function.Injective ⇑σ) : Transcendental K (σ X)

The image of X under an injective homomorphism is transcendental.

theorem RatFunc.adjoin_apply_X_eq_top {K : Type u_1} [Field K] {L : Type u_2} [Field L] [Algebra K L] (σ : RatFunc K ≃ₐ[K] L) : K⟮σ X⟯ = ⊤

The image of X under an isomorphism generates the target: the image of k⟮X⟯ = ⊤ under a surjective map is everything.

noncomputable def RatFunc.algEquivOfAdjoinEqTop {K : Type u_1} [Field K] {L : Type u_2} [Field L] [Algebra K L] [Algebra.Transcendental K L] {f : L} (htop : K⟮f⟯ = ⊤) : RatFunc K ≃ₐ[K] L

The isomorphism k(X) ≃ L sending X to a generator f of L: the identification of k(X) with k⟮f⟯ = ⊤, which transcendence of f provides.

@[simp]

theorem RatFunc.algEquivOfAdjoinEqTop_X {K : Type u_1} [Field K] {L : Type u_2} [Field L] [Algebra K L] [Algebra.Transcendental K L] {f : L} (htop : K⟮f⟯ = ⊤) : (algEquivOfAdjoinEqTop htop) X = f

The isomorphism of a generator sends X to it, which is what identifies the isomorphisms with the generators.

noncomputable def RatFunc.algEquivEquivGenerator (K : Type u_1) [Field K] (L : Type u_2) [Field L] [Algebra K L] [Algebra.Transcendental K L] : (RatFunc K ≃ₐ[K] L) ≃ { f : L // K⟮f⟯ = ⊤ }

The isomorphisms k(X) ≃ L over k are the generators of L: an isomorphism is determined by, and determines, the image of X.

@[simp]

theorem RatFunc.algEquivEquivGenerator_apply {K : Type u_1} [Field K] {L : Type u_2} [Field L] [Algebra K L] [Algebra.Transcendental K L] (σ : RatFunc K ≃ₐ[K] L) : ↑((algEquivEquivGenerator K L) σ) = σ X

@[simp]

theorem RatFunc.algEquivEquivGenerator_symm_apply {K : Type u_1} [Field K] {L : Type u_2} [Field L] [Algebra K L] [Algebra.Transcendental K L] (f : { f : L // K⟮f⟯ = ⊤ }) : (algEquivEquivGenerator K L).symm f = algEquivOfAdjoinEqTop ⋯