Documentation

TauCeti.LinearAlgebra.Matrix.GeneralLinearGroup.PolynomialFunctions.Basic

Polynomial and rational functions on the general linear group #

Two subalgebras of the k-valued functions on GL n k: the functions given by a polynomial in the matrix entries, and those given by such a polynomial divided by a power of the determinant. They are the coordinate-level bookkeeping behind the polynomial and rational representations of GL n ℂ, where a representation is polynomial or rational exactly when all of its matrix coefficients lie in one of them.

The rational condition is stated multiplicatively, as det ^ m * f being polynomial, so that no inverse is taken and it lives over an arbitrary commutative ring, as the polynomial condition does over an arbitrary commutative semiring; TauCeti.Matrix.GeneralLinearGroup.mem_rationalFunctions_iff_inv is the equivalent (det ^ m)⁻¹ form over a field.

Over a finite field every function on the finite set GL n k is the evaluation of a polynomial in the matrix entries, so TauCeti.Matrix.GeneralLinearGroup.polynomialFunctions k n is then the whole function algebra and the distinction between the two collapses. Consumers for which the distinction is the point work over an infinite field.

Main definitions #

Main results #

source
noncomputable def TauCeti.Matrix.GeneralLinearGroup.polynomialFunctions (k : Type u) [CommSemiring k] (n : ℕ) :
Subalgebra k (GL (Fin n) k → k)

The polynomial functions on GL n k: those f : GL (Fin n) k → k obtained by evaluating a polynomial in the matrix entries, that is, the range of the algebra map sending the variable indexed by (i, j) to the (i, j) entry.

Instances For
    source
    theorem TauCeti.Matrix.GeneralLinearGroup.mem_polynomialFunctions {k : Type u} [CommSemiring k] {n : ℕ} {f : GL (Fin n) k → k} :
    f ∈ polynomialFunctions k n ↔ ∃ (P : MvPolynomial (Fin n × Fin n) k), ∀ (g : GL (Fin n) k), f g = (MvPolynomial.eval fun (p : Fin n × Fin n) => ↑g p.1 p.2) P

    Membership in the polynomial functions: f is polynomial exactly when some polynomial in the matrix entries evaluates to f g at every g.

    source
    @[simp]
    theorem TauCeti.Matrix.GeneralLinearGroup.entry_mem_polynomialFunctions {k : Type u} [CommSemiring k] {n : ℕ} (i j : Fin n) :
    (fun (g : GL (Fin n) k) => ↑g i j) ∈ polynomialFunctions k n

    The matrix entries themselves are polynomial functions.

    source
    @[simp]
    theorem TauCeti.Matrix.GeneralLinearGroup.eval_entries_det_mvPolynomialX {k : Type u} [CommRing k] {n : ℕ} (g : GL (Fin n) k) :
    (MvPolynomial.eval fun (p : Fin n × Fin n) => ↑g p.1 p.2) (Matrix.mvPolynomialX (Fin n) (Fin n) k).det = (↑g).det

    Evaluating the generic determinant at the entries of g gives det g.

    source
    noncomputable def TauCeti.Matrix.GeneralLinearGroup.rationalFunctions (k : Type u) [CommRing k] (n : ℕ) :
    Subalgebra k (GL (Fin n) k → k)

    The rational functions on GL n k: those f : GL (Fin n) k → k some determinant power of which is polynomial in the matrix entries. Stated multiplicatively, as det ^ m * f being polynomial, so that no inverse is taken and the definition makes sense over a commutative ring; TauCeti.Matrix.GeneralLinearGroup.mem_rationalFunctions_iff_inv is the form with (det ^ m)⁻¹ over a field.

    Instances For
      source
      theorem TauCeti.Matrix.GeneralLinearGroup.mem_rationalFunctions {k : Type u} [CommRing k] {n : ℕ} {f : GL (Fin n) k → k} :
      f ∈ rationalFunctions k n ↔ ∃ (P : MvPolynomial (Fin n × Fin n) k) (m : ℕ), ∀ (g : GL (Fin n) k), (↑g).det ^ m * f g = (MvPolynomial.eval fun (p : Fin n × Fin n) => ↑g p.1 p.2) P

      Membership in the rational functions: f is rational exactly when some determinant power det ^ m makes det ^ m * f the evaluation of a polynomial in the matrix entries.

      source
      theorem TauCeti.Matrix.GeneralLinearGroup.polynomialFunctions_le_rationalFunctions {k : Type u} [CommRing k] {n : ℕ} :
      polynomialFunctions k n ≤ rationalFunctions k n

      A polynomial function is rational.

      source
      @[simp]
      theorem TauCeti.Matrix.GeneralLinearGroup.det_mem_polynomialFunctions {k : Type u} [CommRing k] {n : ℕ} :
      (fun (g : GL (Fin n) k) => (↑g).det) ∈ polynomialFunctions k n

      The determinant is a polynomial function.

      source
      @[simp]
      theorem TauCeti.Matrix.GeneralLinearGroup.det_zpow_mem_rationalFunctions {k : Type u} [CommRing k] {n : ℕ} (m : ℤ) :
      (fun (g : GL (Fin n) k) => ↑(Matrix.GeneralLinearGroup.det g ^ m)) ∈ rationalFunctions k n

      Every integral determinant power is a rational function. For 0 ≤ m it is even a polynomial function, by TauCeti.Matrix.GeneralLinearGroup.det_mem_polynomialFunctions.

      source
      theorem TauCeti.Matrix.GeneralLinearGroup.entry_inv_mem_rationalFunctions {k : Type u} [CommRing k] {n : ℕ} (i j : Fin n) :
      (fun (g : GL (Fin n) k) => ↑g⁻¹ i j) ∈ rationalFunctions k n

      The entries of the inverse matrix are rational functions: det g times an entry of g⁻¹ is the corresponding entry of the adjugate of g, a polynomial in the entries of g.

      source
      theorem TauCeti.Matrix.GeneralLinearGroup.exists_forall_det_pow_mul_eq_of_forall_mem_rationalFunctions {k : Type u} [CommRing k] {n : ℕ} {ι : Type w} [Finite ι] {f : ι → GL (Fin n) k → k} (hf : ∀ (i : ι), f i ∈ rationalFunctions k n) :
      ∃ (P : ι → MvPolynomial (Fin n × Fin n) k) (m : ℕ), ∀ (i : ι) (g : GL (Fin n) k), (↑g).det ^ m * f i g = (MvPolynomial.eval fun (p : Fin n × Fin n) => ↑g p.1 p.2) (P i)

      A finite family of rational functions has a common denominator: a single determinant power and a family of numerator polynomials express every member of the family.

      source
      theorem TauCeti.Matrix.GeneralLinearGroup.mem_rationalFunctions_iff_inv {k : Type u} [Field k] {n : ℕ} {f : GL (Fin n) k → k} :
      f ∈ rationalFunctions k n ↔ ∃ (P : MvPolynomial (Fin n × Fin n) k) (m : ℕ), ∀ (g : GL (Fin n) k), f g = ((↑g).det ^ m)⁻¹ * (MvPolynomial.eval fun (p : Fin n × Fin n) => ↑g p.1 p.2) P

      Over a field, membership in the rational functions is the expected statement that f is a polynomial in the matrix entries divided by a power of the determinant.

      source
      theorem TauCeti.Matrix.GeneralLinearGroup.exists_forall_eq_inv_mul_of_forall_mem_rationalFunctions {k : Type u} [Field k] {n : ℕ} {ι : Type w} [Finite ι] {f : ι → GL (Fin n) k → k} (hf : ∀ (i : ι), f i ∈ rationalFunctions k n) :
      ∃ (P : ι → MvPolynomial (Fin n × Fin n) k) (m : ℕ), ∀ (i : ι) (g : GL (Fin n) k), f i g = ((↑g).det ^ m)⁻¹ * (MvPolynomial.eval fun (p : Fin n × Fin n) => ↑g p.1 p.2) (P i)

      A finite family of rational functions has a common denominator, in the form with the determinant power inverted. This is what lets the coordinate form of rationality carry a single exponent for the whole matrix.