Polynomial point maps for the general linear group

This file compares the generic polynomial point maps used in the dynamic-subgroup construction with the matrix description of general-linear points. Inclusion into Laurent polynomials and evaluation at zero both act entrywise on the corresponding invertible matrix.

theorem TauCeti.GeneralLinear.Dynamic.pointsMulEquiv_ofPolyPoint {R : Type u} [CommRing R] {N : ℕ} {A : Type v} [CommRing A] [Algebra R A] (F : WithConv (↑(coordinateHopfAlgebra R N) →ₐ[R] Polynomial A)) : (pointsMulEquiv N) ((Cocharacter.ofPolyPoint A) F) = (Matrix.GeneralLinearGroup.map ↑(AlgHom.restrictScalars R Polynomial.toLaurentAlg)) ((pointsMulEquiv N) F)

Applying the inclusion A[X] → A[T;T⁻¹] to a general-linear point applies that inclusion entrywise to its matrix.

theorem TauCeti.GeneralLinear.Dynamic.pointsMulEquiv_evalZeroPoint {R : Type u} [CommRing R] {N : ℕ} {A : Type v} [CommRing A] [Algebra R A] (F : WithConv (↑(coordinateHopfAlgebra R N) →ₐ[R] Polynomial A)) : (pointsMulEquiv N) ((Cocharacter.evalZeroPoint A) F) = (Matrix.GeneralLinearGroup.map ↑(AlgHom.restrictScalars R (Polynomial.aeval 0))) ((pointsMulEquiv N) F)

Evaluating a polynomial-valued general-linear point at zero evaluates every matrix entry at zero.