The functor of points of the general linear group #
For a commutative ring R and n : ℕ, this file identifies the convolution group of
algebra-valued points of the coordinate Hopf algebra
R[Xᵢⱼ][det(X)⁻¹]
with Mathlib's general linear group. A point is sent to the matrix of its values on the localized generic entries. Conversely, an invertible matrix defines polynomial evaluation, which extends uniquely across the determinant localization. The matrix-multiplication comultiplication makes this equivalence multiplicative in the ordinary, rather than opposite, order.
The equivalences are natural in the commutative value algebra. They therefore assemble into a
natural isomorphism from HopfAlgebra.pointsFunctor for coordinateHopfAlgebra to the functor
of invertible matrices. The construction includes rank zero and zero rings, without a
nontriviality or positive-rank assumption.
Main declarations #
TauCeti.GeneralLinear.pointToGeneralLinear: the invertible matrix read from a point, withTauCeti.GeneralLinear.map_genericMatrix_eq_coe_pointToGeneralLinearidentifying it with the transported generic matrix.TauCeti.GeneralLinear.generalLinearToPoint: the point obtained by matrix evaluation.TauCeti.GeneralLinear.pointsMulEquiv: the group equivalence between convolution points and invertible matrices.TauCeti.GeneralLinear.generalLinearFunctor: the group-valued functor of invertible matrices.TauCeti.GeneralLinear.pointsNatIso: the natural isomorphism between the two functors.
References #
Reading a point as an invertible matrix evaluates it on the corresponding bundled coordinate.
The generic matrix transported along an algebra morphism out of the coordinate Hopf algebra is the matrix of the point that morphism is.
The point of the bundled general linear coordinate Hopf algebra obtained by evaluating the generic matrix at an invertible matrix.
Equations
- One or more equations did not get rendered due to their size.
Instances For
Evaluation at an invertible matrix sends a polynomial in the bundled coordinate ring to its multivariable polynomial evaluation at the matrix entries.
The point obtained from an invertible matrix sends a bundled generic coordinate to the corresponding matrix entry.
Reading points as invertible matrices carries convolution to ordinary matrix multiplication, with the tensor-factor order unchanged.
The convolution group of points of the general linear coordinate Hopf algebra is the ordinary general linear group. Multiplication has the same order on both sides.
Equations
- One or more equations did not get rendered due to their size.
Instances For
The forward map of pointsMulEquiv is evaluation on the localized generic matrix.
The inverse map of pointsMulEquiv is the extension of matrix evaluation across the
determinant localization.
Reading a point as an invertible matrix commutes with maps of value algebras.
The pointwise group equivalence is natural in the value algebra.
Naturality of the inverse pointwise equivalence in the value algebra.
The group-valued functor sending a commutative R-algebra to its general linear group and
a value-algebra morphism to entrywise application. Its values are universe-lifted so that its
codomain agrees with the generic Hopf-algebra points functor.
Equations
Instances For
The object part of generalLinearFunctor is the universe lift of the ordinary general
linear group.
The morphism part of generalLinearFunctor applies the value-algebra map entrywise. The
equality transports along generalLinearFunctor_obj because the functor's implementation is
opaque.
Entrywise computation of the value-algebra map on the general linear functor.
The convolution-points functor of the general linear coordinate Hopf algebra is naturally isomorphic to the ordinary general linear group functor.
Equations
Instances For
After transport along generalLinearFunctor_obj, the forward component of pointsNatIso is
the pointwise general-linear equivalence.
After transport back along generalLinearFunctor_obj, the inverse component of pointsNatIso
is evaluation at an invertible matrix.