Linear fractional transformations of the rational function field

Four elements a, b, c, d of an integral domain k with a d - b c ≠ 0 give the linear fractional transformation (a X + b) / (c X + d) of k(X). The inverse linear fractional formula recovers X from it. When k is a field, it is a transcendental generator of k(X) over k and therefore the image of X under an automorphism of k(X) over k.

Over a field k, the coefficients form an invertible 2 × 2 matrix, and conversely every invertible 2 × 2 matrix over k has nonzero determinant, so the construction applies to GL₂(k).

Main definitions

• RatFunc.mobiusOf: the linear fractional transformation of four coefficients, with its defining equation mobiusOf_def.
• RatFunc.mobiusAutOf: the automorphism of k(X) sending X to it.
• Matrix.GeneralLinearGroup.mobius (with Matrix.GeneralLinearGroup.mobius_def) and Matrix.GeneralLinearGroup.mobiusAut: the same for an invertible matrix.
• RatFunc.mobiusAutHom: the group homomorphism GL₂(k) →* Aut(k(X)/k).
• RatFunc.pglEquivAlgEquiv: the isomorphism PGL₂(k) ≃* Aut(k(X)/k), evaluated on a class of matrices by Matrix.GeneralLinearGroup.pglEquivAlgEquiv_mk.
• RatFunc.translationAut: the translation X ↦ X + c.
• RatFunc.branchPointAut: the homomorphism Perm (Fin 3) →* Aut(k(X)/k) of the six substitutions X, 1 - X, X / (X - 1), 1 / X, (X - 1) / X and 1 / (1 - X) permuting 0, 1, ∞, with its values at X on the five nonidentity permutations (RatFunc.branchPointAut_swap_zero_one_X and its siblings).

Main results

• RatFunc.transcendental_mobiusOf and RatFunc.adjoin_mobiusOf_eq_top: a linear fractional transformation is a transcendental generator of k(X).
• RatFunc.X_eq_div_mobiusOf: the inverse coefficient matrix recovers X.
• Matrix.GeneralLinearGroup.mobiusAut_mobius and RatFunc.mobiusAutHom: substitution composes the coefficient matrices in the opposite order, so inversion gives a group homomorphism GL₂(k) →* Aut(k(X)/k).
• RatFunc.infinite_algEquiv: over an infinite field the translations already make Aut(k(X)/k) infinite.
• RatFunc.finite_algEquiv and RatFunc.infinite_algEquiv_iff: over a finite field Aut(k(X)/k) ≅ PGL₂(k) is finite, so it is infinite exactly when k is.
• RatFunc.card_algEquiv: over a field with q elements, Aut(k(X)/k) has order q³ - q.

References

• H. Stichtenoth, Algebraic Function Fields and Codes, 2nd ed., GTM 254, Springer, 2009, Exercise 1.2.
• E. Girondo and G. González-Diez, Introduction to Compact Riemann Surfaces and Dessins d'Enfants, LMS Student Texts 79, Cambridge University Press, 2012, §4.4, and S. K. Lando and A. K. Zvonkin, Graphs on Surfaces and Their Applications, Encyclopaedia of Mathematical Sciences 141, Springer, 2004, §1.5, for the six transformations permuting 0, 1, ∞.

theorem RatFunc.mul_X_add_C_ne_zero {K : Type u_1} [CommRing K] [IsDomain K] {c d : K} (hcd : c ≠ 0 ∨ d ≠ 0) : C c * X + C d ≠ 0

A nonzero linear polynomial in X, read in k(X), is nonzero.

noncomputable def RatFunc.mobiusOf {K : Type u_1} [CommRing K] [IsDomain K] (a b c d : K) : RatFunc K

The linear fractional transformation (a X + b) / (c X + d) of k(X).

theorem RatFunc.mobiusOf_def {K : Type u_1} [CommRing K] [IsDomain K] (a b c d : K) : mobiusOf a b c d = (C a * X + C b) / (C c * X + C d)

The defining equation of mobiusOf.

theorem RatFunc.mobiusOf_den_ne_zero {K : Type u_1} [CommRing K] [IsDomain K] {a b c d : K} (hdet : a * d - b * c ≠ 0) : C c * X + C d ≠ 0

The denominator of a linear fractional transformation with invertible coefficients is nonzero.

theorem RatFunc.mobiusOf_mul_den {K : Type u_1} [CommRing K] [IsDomain K] {a b c d : K} (hdet : a * d - b * c ≠ 0) : mobiusOf a b c d * (C c * X + C d) = C a * X + C b

Clearing the denominator of a linear fractional transformation.

theorem RatFunc.sub_mul_mobiusOf_mul_den {K : Type u_1} [CommRing K] [IsDomain K] {a b c d : K} (hdet : a * d - b * c ≠ 0) : (C a - C c * mobiusOf a b c d) * (C c * X + C d) = C (a * d - b * c)

The coefficient a - c · m scaled by the denominator is the determinant.

theorem RatFunc.sub_mul_mobiusOf_ne_zero {K : Type u_1} [CommRing K] [IsDomain K] {a b c d : K} (hdet : a * d - b * c ≠ 0) : C a - C c * mobiusOf a b c d ≠ 0

The coefficient a - c · m is nonzero, being the determinant over the denominator.

theorem RatFunc.X_mul_sub_mul_mobiusOf {K : Type u_1} [CommRing K] [IsDomain K] {a b c d : K} (hdet : a * d - b * c ≠ 0) : X * (C a - C c * mobiusOf a b c d) = C d * mobiusOf a b c d - C b

The inverse coefficient matrix recovers X: X · (a - c · m) = d · m - b, both sides being the determinant times X over the denominator.

theorem RatFunc.X_eq_div_mobiusOf {K : Type u_1} [CommRing K] [IsDomain K] {a b c d : K} (hdet : a * d - b * c ≠ 0) : X = (C d * mobiusOf a b c d - C b) / (C a - C c * mobiusOf a b c d)

X is a linear fractional transformation of m, by the inverse coefficient matrix.

theorem RatFunc.transcendental_mobiusOf {K : Type u_1} [CommRing K] [IsDomain K] {a b c d : K} (hdet : a * d - b * c ≠ 0) : Transcendental K (mobiusOf a b c d)

A linear fractional transformation is transcendental: its inverse formula expresses X in terms of it and the constants.

theorem RatFunc.mul_mobiusOf_add_ne_zero {K : Type u_1} [CommRing K] [IsDomain K] {a b c d : K} (hdet : a * d - b * c ≠ 0) (c' d' : K) (hcd' : c' ≠ 0 ∨ d' ≠ 0) : C c' * mobiusOf a b c d + C d' ≠ 0

A nonzero linear expression in a Möbius transformation is nonzero.

theorem RatFunc.mobiusOf_eq_X_iff {K : Type u_1} [CommRing K] [IsDomain K] {a b c d : K} (hdet : a * d - b * c ≠ 0) : mobiusOf a b c d = X ↔ b = 0 ∧ c = 0 ∧ a = d

A linear fractional transformation is the identity exactly for a scalar coefficient matrix: (a X + b) / (c X + d) = X if and only if b = 0, c = 0 and a = d.

theorem RatFunc.mul_mobiusOf_add_mul_den {K : Type u_1} [CommRing K] [IsDomain K] {a b c d : K} (hdet : a * d - b * c ≠ 0) (c' d' : K) : (C c' * mobiusOf a b c d + C d') * (C c * X + C d) = C (c' * a + d' * c) * X + C (c' * b + d' * d)

Multiplying a linear expression in a Möbius transformation by its denominator multiplies its coefficient row by the coefficient matrix.

@[simp]

theorem RatFunc.mobiusOf_one_right {K : Type u_1} [CommRing K] [IsDomain K] (c : K) : mobiusOf 1 c 0 1 = X + C c

A translation X + c is a linear fractional transformation.

noncomputable def Matrix.GeneralLinearGroup.mobius {K : Type u_1} [CommRing K] [IsDomain K] (A : GL (Fin 2) K) : RatFunc K

The linear fractional transformation of an invertible matrix A = !![a, b; c, d].

theorem Matrix.GeneralLinearGroup.mobius_def {K : Type u_1} [CommRing K] [IsDomain K] (A : GL (Fin 2) K) : A.mobius = RatFunc.mobiusOf (↑A 0 0) (↑A 0 1) (↑A 1 0) (↑A 1 1)

The defining equation of mobius.

@[simp]

theorem Matrix.GeneralLinearGroup.mobius_one {K : Type u_1} [CommRing K] [IsDomain K] : mobius 1 = RatFunc.X

The identity matrix gives the identity transformation.

theorem RatFunc.adjoin_mobiusOf_eq_top {K : Type u_1} [Field K] {a b c d : K} (hdet : a * d - b * c ≠ 0) : K⟮mobiusOf a b c d⟯ = ⊤

A linear fractional transformation generates k(X), since X is a linear fractional transformation of it.

noncomputable def RatFunc.mobiusAutOf {K : Type u_1} [Field K] {a b c d : K} (hdet : a * d - b * c ≠ 0) : Gal(RatFunc K/K)

The automorphism of k(X) given by a linear fractional transformation: the automorphism sending X to (a X + b) / (c X + d).

@[simp]

theorem RatFunc.mobiusAutOf_X {K : Type u_1} [Field K] {a b c d : K} (hdet : a * d - b * c ≠ 0) : (mobiusAutOf hdet) X = mobiusOf a b c d

theorem RatFunc.mobiusAutOf_eq_one_iff {K : Type u_1} [Field K] {a b c d : K} (hdet : a * d - b * c ≠ 0) : mobiusAutOf hdet = 1 ↔ b = 0 ∧ c = 0 ∧ a = d

A linear fractional transformation gives the identity automorphism exactly for a scalar coefficient matrix.

theorem RatFunc.mobiusAutOf_mobiusOf {K : Type u_1} [Field K] {a b c d : K} (hdet : a * d - b * c ≠ 0) (a' b' c' d' : K) : (mobiusAutOf hdet) (mobiusOf a' b' c' d') = mobiusOf (a' * a + b' * c) (a' * b + b' * d) (c' * a + d' * c) (c' * b + d' * d)

Substitution composes linear fractional transformations by multiplying their coefficient matrices in the opposite order. Only the inner transformation needs an invertible coefficient matrix; the outer coefficients may be arbitrary.

noncomputable def Matrix.GeneralLinearGroup.mobiusAut {K : Type u_1} [Field K] (A : GL (Fin 2) K) : Gal(RatFunc K/K)

The automorphism of k(X) given by an invertible matrix.

@[simp]

theorem Matrix.GeneralLinearGroup.mobiusAut_X {K : Type u_1} [Field K] (A : GL (Fin 2) K) : A.mobiusAut RatFunc.X = A.mobius

theorem Matrix.GeneralLinearGroup.mobiusAut_mobius {K : Type u_1} [Field K] (A B : GL (Fin 2) K) : A.mobiusAut B.mobius = (B * A).mobius

Substituting one linear fractional transformation into another multiplies the matrices in the opposite order.

theorem Matrix.GeneralLinearGroup.mobiusAut_eq_one_iff {K : Type u_1} [Field K] (A : GL (Fin 2) K) : A.mobiusAut = 1 ↔ A ∈ Subgroup.center (GL (Fin 2) K)

The identity automorphism comes exactly from the central matrices.

noncomputable def RatFunc.mobiusAutHom {K : Type u_1} [Field K] : GL (Fin 2) K →* Gal(RatFunc K/K)

The linear fractional transformations as a group of automorphisms: the homomorphism GL₂(k) →* Aut(k(X)/k) sending A to the automorphism X ↦ (a X + b) / (c X + d) of the inverse matrix. Inversion is what makes it a homomorphism rather than an antihomomorphism, since substitution composes the matrices in the opposite order.

@[simp]

theorem Matrix.GeneralLinearGroup.mobiusAutHom_apply_X {K : Type u_1} [Field K] (A : GL (Fin 2) K) : (RatFunc.mobiusAutHom A) RatFunc.X = A⁻¹.mobius

theorem RatFunc.ker_mobiusAutHom {K : Type u_1} [Field K] : mobiusAutHom.ker = Subgroup.center (GL (Fin 2) K)

The kernel of the linear fractional action is the centre of GL₂(k): the scalar matrices. So PGL₂(k) acts faithfully on k(X).

theorem RatFunc.exists_mobiusOf_eq_of_adjoin_eq_top {K : Type u_1} [Field K] {f : RatFunc K} (htop : K⟮f⟯ = ⊤) : ∃ (a : K) (b : K) (c : K) (d : K), a * d - b * c ≠ 0 ∧ mobiusOf a b c d = f

Every generator of k(X) over k is a linear fractional transformation: its numerator and denominator have degree at most one, and the determinant of their coefficients is nonzero.

theorem RatFunc.mobiusAutHom_surjective {K : Type u_1} [Field K] : Function.Surjective ⇑mobiusAutHom

Every automorphism of k(X) over k is a linear fractional transformation.

noncomputable def RatFunc.pglEquivAlgEquiv {K : Type u_1} [Field K] : Matrix.ProjGenLinGroup (Fin 2) K ≃* Gal(RatFunc K/K)

PGL₂(k) is the automorphism group of the rational function field (Stichtenoth, Exercise 1.2): the linear fractional transformations exhaust the automorphisms of k(X) over k, and two matrices give the same automorphism exactly when they differ by a scalar.

@[simp]

theorem Matrix.GeneralLinearGroup.pglEquivAlgEquiv_mk {K : Type u_1} [Field K] (A : GL (Fin 2) K) : RatFunc.pglEquivAlgEquiv (ProjGenLinGroup.mk A) = RatFunc.mobiusAutHom A

The isomorphism PGL₂(k) ≃* Aut(k(X)/k) sends the class of a matrix to its linear fractional transformation; with Matrix.GeneralLinearGroup.mobiusAutHom_apply_X this evaluates it at X.

noncomputable def RatFunc.translationAut {K : Type u_1} [Field K] (b : K) : Gal(RatFunc K/K)

The translation automorphism X ↦ X + c of k(X).

@[simp]

theorem RatFunc.translationAut_X {K : Type u_1} [Field K] (b : K) : (translationAut b) X = X + C b

theorem RatFunc.translationAut_injective {K : Type u_1} [Field K] : Function.Injective translationAut

Distinct scalars give distinct translations.

theorem RatFunc.infinite_algEquiv {K : Type u_1} [Field K] [Infinite K] : Infinite Gal(RatFunc K/K)

The automorphism group of k(X) over an infinite field is infinite, witnessed by the translations. This is why the finiteness of the automorphism group of a function field needs genus at least two.

instance RatFunc.finite_algEquiv {K : Type u_1} [Field K] [Finite K] : Finite Gal(RatFunc K/K)

The automorphism group of k(X) over a finite field is finite, because it is PGL₂(k).

theorem RatFunc.infinite_algEquiv_iff {K : Type u_1} [Field K] : Infinite Gal(RatFunc K/K) ↔ Infinite K

The automorphism group of k(X) is infinite exactly when k is infinite: the translations make it infinite over an infinite field, and over a finite field it is the finite group PGL₂(k).

theorem RatFunc.card_algEquiv {K : Type u_1} [Field K] [Fintype K] : Nat.card Gal(RatFunc K/K) = Fintype.card K ^ 3 - Fintype.card K

The order of the automorphism group of 𝔽_q(X) is q³ - q, the order of PGL₂(𝔽_q).

noncomputable def RatFunc.branchPointAut (K : Type u_1) [Field K] : Equiv.Perm (Fin 3) →* Gal(RatFunc K/K)

The automorphisms of k(t) permuting the branch points 0, 1, ∞: for ρ : Perm (Fin 3), the substitution t ↦ m(t) by the linear fractional transformation m that sends the point numbered ρ i to the point numbered i, where 0, 1, 2 number 0, 1, ∞. The five nonidentity substitutions are 1 - t, t / (t - 1), 1 / t, (t - 1) / t and 1 / (1 - t) (RatFunc.branchPointAut_swap_zero_one_X and its siblings, the last one for the inverse of finRotate 3), and they act on the marked places through ρ (TauCeti.Place.map_branchPointAut_markedPlace).

@[simp]

theorem RatFunc.branchPointAut_swap_zero_one_X {K : Type u_1} [Field K] : ((branchPointAut K) (Equiv.swap 0 1)) X = 1 - X

The substitution exchanging 0 and 1 is t ↦ 1 - t.

@[simp]

theorem RatFunc.branchPointAut_swap_one_two_X {K : Type u_1} [Field K] : ((branchPointAut K) (Equiv.swap 1 2)) X = X / (X - 1)

The substitution exchanging 1 and ∞ is t ↦ t / (t - 1).

@[simp]

theorem RatFunc.branchPointAut_swap_zero_two_X {K : Type u_1} [Field K] : ((branchPointAut K) (Equiv.swap 0 2)) X = X⁻¹

The substitution exchanging 0 and ∞ is t ↦ 1 / t.

@[simp]

theorem RatFunc.branchPointAut_finRotate_X {K : Type u_1} [Field K] : ((branchPointAut K) (finRotate 3)) X = (X - 1) / X

The substitution reordering the branch points along 0 → 1 → ∞ → 0 is t ↦ (t - 1) / t.

@[simp]

theorem RatFunc.branchPointAut_finRotate_symm_X {K : Type u_1} [Field K] : ((branchPointAut K) (finRotate 3)).symm X = (1 - X)⁻¹

The substitution reordering the branch points along 0 → ∞ → 1 → 0, the inverse of RatFunc.branchPointAut (finRotate 3), is t ↦ 1 / (1 - t). It is stated for the inverse automorphism, the simp-normal form of branchPointAut K (finRotate 3)⁻¹.