Functorial matrix points cut out by a Hopf ideal #
For a Hopf ideal I in the coordinate ring of GLₙ over a commutative ring R,
TauCeti.GeneralLinear.hopfIdealPointsSubgroup n I A is the group of A-valued points of the
corresponding closed subgroup scheme, in its matrix realization. This file assembles the existing
entrywise maps between these groups into a functor on commutative R-algebras and proves that the
quotient coordinate Hopf algebra represents this matrix-valued functor.
The construction is independent of any particular Chevalley carrier. An eventual explicit pinned
simply connected carrier can instantiate it with its defining Hopf ideal. In the integral case,
TauCeti.GeneralLinear.iterateFrobeniusHopfIdealPoints supplies the p ^ k-power Frobenius
endomorphism and its fixed-point interface.
Main declarations #
TauCeti.GeneralLinear.hopfIdealPointsSubgroupMulEquiv: the pointwise group equivalence between quotient Hopf-algebra points and the matrix subgroup cut out by the ideal.TauCeti.GeneralLinear.hopfIdealPointsSubgroupFunctor: the group-valued functor of matrix points cut out by a fixed Hopf ideal.TauCeti.GeneralLinear.hopfIdealPointsSubgroupNatIso: the representing natural isomorphism.
Roadmap #
This advances the carrier-independent infrastructure for "Points over an algebraically closed
field as a group, functorially in the field" in Layer 9 of
TauCetiRoadmap/ReductiveGroups/README.md. The consumer is the explicit pinned simply connected
Chevalley--Demazure carrier required by milestone L0 of
TauCetiRoadmap/CFSGStatement/README.md; this file does not identify any provisional carrier with
that simply connected group.
Quotient Hopf-algebra points are multiplicatively equivalent to the matrix subgroup cut out by the Hopf ideal. The equivalence first includes a quotient point among the ambient Hopf-algebra points, then reads that point as an invertible matrix.
Equations
- One or more equations did not get rendered due to their size.
Instances For
A quotient point, viewed through hopfIdealPointsSubgroupMulEquiv, is its included ambient
point read as an invertible matrix.
An equivalence from quotient points to a matrix subgroup identifies membership in the quotient-point subgroup whenever it preserves the ambient invertible matrix.
Including the ambient Hopf-algebra point underlying the inverse matrix-subgroup equivalence recovers the point corresponding to the underlying matrix.
The group-valued functor sending a commutative R-algebra to the matrix point group cut out by
a fixed Hopf ideal in the coordinate ring of GLₙ. Its values are universe-lifted so that its
codomain agrees with the generic Hopf-algebra points functor.
Equations
Instances For
The object part of the Hopf-ideal matrix-points functor is the universe lift of the subgroup cut out by the fixed Hopf ideal.
The morphism part of the Hopf-ideal matrix-points functor is the universe lift of the restricted entrywise matrix map.
The morphism part of the Hopf-ideal matrix-points functor applies the value-algebra morphism entrywise after removing the universe lift.
The matrix-subgroup equivalence is natural in the value algebra.
The quotient coordinate Hopf algebra represents the matrix point subgroup functor cut out by the Hopf ideal.
Equations
- One or more equations did not get rendered due to their size.
Instances For
After transport along hopfIdealPointsSubgroupFunctor_obj, the forward component of the
representing natural isomorphism is the pointwise matrix-subgroup equivalence.
After transport back along hopfIdealPointsSubgroupFunctor_obj, the inverse component of the
representing natural isomorphism is the inverse pointwise matrix-subgroup equivalence.