Coordinate functions on GLₙ and their values at points

Evaluating at the points of GL n k turns an element of the coordinate Hopf algebra O(GLₙ) over a field k into a function GL n k → k. This file compares the two descriptions of regular functions on GLₙ.

• The functions obtained this way are exactly the rational functions TauCeti.Matrix.GeneralLinearGroup.rationalFunctions k n, those of the form g ↦ P(g) / det(g)ᵐ for a polynomial P in the matrix entries.
• Over an infinite field the evaluation is injective: the points of GL n k separate the elements of O(GLₙ), and pairs of points separate the elements of O(GLₙ) ⊗ O(GLₙ). This is the Zariski density of the invertible matrices, MvPolynomial.eq_of_eval_eq_on_gl, read through the determinant localization.

Together these let identities between coordinate functions, such as the comultiplication of the matrix coefficients of a representation, be checked on matrices.

Main results

• TauCeti.GeneralLinear.mem_rationalFunctions_iff_exists_generalLinearToPoint_apply_eq: the rational functions on GL n k are the evaluations of coordinate functions.
• TauCeti.GeneralLinear.eq_of_forall_generalLinearToPoint_apply_eq: over an infinite field, points of GL n k separate coordinate functions.
• TauCeti.GeneralLinear.tensor_eq_of_forall_lift_generalLinearToPoint_eq: over an infinite field, pairs of points of GL n k separate the tensor square of O(GLₙ).

theorem TauCeti.GeneralLinear.mem_rationalFunctions_iff_exists_generalLinearToPoint_apply_eq {k : Type u_1} [Field k] {n : ℕ} {f : GL (Fin n) k → k} : f ∈ Matrix.GeneralLinearGroup.rationalFunctions k n ↔ ∃ (x : ↑(coordinateHopfAlgebra k n)), ∀ (g : GL (Fin n) k), (generalLinearToPoint n g).ofConv x = f g

The rational functions on GL n k are the coordinate functions: a function f : GL n k → k is a polynomial in the matrix entries divided by a power of the determinant exactly when it is evaluation at the points of GL n k of an element of O(GLₙ).

theorem TauCeti.GeneralLinear.eq_of_forall_generalLinearToPoint_apply_eq {k : Type u_1} [Field k] {n : ℕ} [Infinite k] {x y : ↑(coordinateHopfAlgebra k n)} (h : ∀ (g : GL (Fin n) k), (generalLinearToPoint n g).ofConv x = (generalLinearToPoint n g).ofConv y) : x = y

Points of GL n k separate coordinate functions over an infinite field: two elements of O(GLₙ) with the same value at every invertible matrix are equal. This is the Zariski density of GL n k in GLₙ.

theorem TauCeti.GeneralLinear.tensor_eq_of_forall_lift_generalLinearToPoint_eq {k : Type u_1} [Field k] {n : ℕ} [Infinite k] {s t : TensorProduct k ↑(coordinateHopfAlgebra k n) ↑(coordinateHopfAlgebra k n)} (h : ∀ (g g' : GL (Fin n) k), (Algebra.TensorProduct.lift (generalLinearToPoint n g).ofConv (generalLinearToPoint n g').ofConv ⋯) s = (Algebra.TensorProduct.lift (generalLinearToPoint n g).ofConv (generalLinearToPoint n g').ofConv ⋯) t) : s = t

Pairs of points of GL n k separate the tensor square of O(GLₙ) over an infinite field: two tensors are equal when the pair (g, g') of invertible matrices, sending x ⊗ y to x(g) y(g'), takes the same value on both, for every such pair.