The functor of points of the upper-unitriangular group

For a commutative ring R, this file identifies the convolution group of algebra-valued points of the upper-unitriangular coordinate Hopf algebra with the existing upper-unitriangular matrix group. The equivalence is natural in the commutative value algebra and therefore assembles into a natural isomorphism of group-valued functors.

The construction includes empty finite index types and zero rings. It does not yet package a group scheme.

Main declarations

• TauCeti.UpperUnitriangular.pointsMulEquiv: its convolution points are the existing TauCeti.upperUnitriangularGroup.
• TauCeti.UpperUnitriangular.pointToUpperUnitriangular_mapValue: the point identification is natural in the value algebra.
• TauCeti.UpperUnitriangular.pointsMulEquiv_mapValue: the bundled point equivalence is natural in the value algebra.
• TauCeti.UpperUnitriangular.upperUnitriangularFunctor: the group-valued matrix functor.
• TauCeti.UpperUnitriangular.pointsNatIso: the natural isomorphism between the points and matrix functors.

References

• J. C. Jantzen, Representations of Algebraic Groups, I.2.
• T. A. Springer, Linear Algebraic Groups, Section 2.4.

The layout follows GeneralLinear.FunctorOfPoints.

noncomputable def TauCeti.UpperUnitriangular.pointToUpperUnitriangular (R : Type u) [CommRing R] (m : Type v) [Fintype m] [LinearOrder m] {A : Type w} [CommRing A] [Algebra R A] (f : WithConv (↑(coordinateHopfAlgebra R m) →ₐ[R] A)) : ↥(upperUnitriangularGroup m A)

The upper-unitriangular matrix obtained by evaluating a point on the generic matrix.

Equations

• TauCeti.UpperUnitriangular.pointToUpperUnitriangular R m f = ⟨⋯.toGL, ⋯⟩

@[simp]

theorem TauCeti.UpperUnitriangular.coe_pointToUpperUnitriangular (R : Type u) [CommRing R] (m : Type v) [Fintype m] [LinearOrder m] {A : Type w} [CommRing A] [Algebra R A] (f : WithConv (↑(coordinateHopfAlgebra R m) →ₐ[R] A)) : ↑↑(pointToUpperUnitriangular R m f) = (genericMatrix R m).map ⇑(f.ofConv.comp ↑(coordinateHopfAlgebraAlgEquiv R m))

As a matrix, a point is evaluated entrywise on the generic matrix.

@[simp]

theorem TauCeti.UpperUnitriangular.pointToUpperUnitriangular_apply (R : Type u) [CommRing R] (m : Type v) [Fintype m] [LinearOrder m] {A : Type w} [CommRing A] [Algebra R A] (f : WithConv (↑(coordinateHopfAlgebra R m) →ₐ[R] A)) (i j : m) : ↑↑(pointToUpperUnitriangular R m f) i j = f.ofConv ((coordinateHopfAlgebraAlgEquiv R m) (genericMatrix R m i j))

Reading a point as an upper-unitriangular matrix evaluates it on the corresponding generic entry.

theorem TauCeti.UpperUnitriangular.pointToUpperUnitriangular_apply_of_lt (R : Type u) [CommRing R] (m : Type v) [Fintype m] [LinearOrder m] {A : Type w} [CommRing A] [Algebra R A] (f : WithConv (↑(coordinateHopfAlgebra R m) →ₐ[R] A)) {i j : m} (h : i < j) : ↑↑(pointToUpperUnitriangular R m f) i j = f.ofConv ((coordinateHopfAlgebraAlgEquiv R m) (MvPolynomial.X (have this := ⟨(i, j), h⟩; this)))

On a strict-upper entry, point evaluation is coordinate evaluation.

noncomputable def TauCeti.UpperUnitriangular.upperUnitriangularToPoint (R : Type u) [CommRing R] (m : Type v) [Fintype m] [LinearOrder m] {A : Type w} [CommRing A] [Algebra R A] (g : ↥(upperUnitriangularGroup m A)) : WithConv (↑(coordinateHopfAlgebra R m) →ₐ[R] A)

Evaluate the strict-upper polynomial coordinates at an upper-unitriangular matrix.

Equations

• One or more equations did not get rendered due to their size.

@[simp]

theorem TauCeti.UpperUnitriangular.upperUnitriangularToPoint_apply (R : Type u) [CommRing R] (m : Type v) [Fintype m] [LinearOrder m] {A : Type w} [CommRing A] [Algebra R A] (g : ↥(upperUnitriangularGroup m A)) (ij : Index m) : (upperUnitriangularToPoint R m g).ofConv ((coordinateHopfAlgebraAlgEquiv R m) (MvPolynomial.X ij)) = ↑↑g (↑ij).1 (↑ij).2

The point associated to an upper-unitriangular matrix sends each strict-upper coordinate to the corresponding entry.

@[simp]

theorem TauCeti.UpperUnitriangular.pointToUpperUnitriangular_upperUnitriangularToPoint (R : Type u) [CommRing R] (m : Type v) [Fintype m] [LinearOrder m] {A : Type w} [CommRing A] [Algebra R A] (g : ↥(upperUnitriangularGroup m A)) : pointToUpperUnitriangular R m (upperUnitriangularToPoint R m g) = g

Evaluating the point associated to an upper-unitriangular matrix recovers that matrix.

@[simp]

theorem TauCeti.UpperUnitriangular.upperUnitriangularToPoint_pointToUpperUnitriangular (R : Type u) [CommRing R] (m : Type v) [Fintype m] [LinearOrder m] {A : Type w} [CommRing A] [Algebra R A] (f : WithConv (↑(coordinateHopfAlgebra R m) →ₐ[R] A)) : upperUnitriangularToPoint R m (pointToUpperUnitriangular R m f) = f

Forming a point from the matrix read off a point recovers the original point.

@[simp]

theorem TauCeti.UpperUnitriangular.pointToUpperUnitriangular_mul (R : Type u) [CommRing R] (m : Type v) [Fintype m] [LinearOrder m] {A : Type w} [CommRing A] [Algebra R A] (f g : WithConv (↑(coordinateHopfAlgebra R m) →ₐ[R] A)) : pointToUpperUnitriangular R m (f * g) = pointToUpperUnitriangular R m f * pointToUpperUnitriangular R m g

Evaluation on the generic matrix carries convolution to matrix multiplication.

noncomputable def TauCeti.UpperUnitriangular.pointsMulEquiv (R : Type u) [CommRing R] (m : Type v) [Fintype m] [LinearOrder m] {A : Type w} [CommRing A] [Algebra R A] : WithConv (↑(coordinateHopfAlgebra R m) →ₐ[R] A) ≃* ↥(upperUnitriangularGroup m A)

The convolution group of points of the coordinate Hopf algebra is the ordinary upper-unitriangular matrix group.

Equations

• One or more equations did not get rendered due to their size.

@[simp]

theorem TauCeti.UpperUnitriangular.pointsMulEquiv_apply (R : Type u) [CommRing R] (m : Type v) [Fintype m] [LinearOrder m] {A : Type w} [CommRing A] [Algebra R A] (f : WithConv (↑(coordinateHopfAlgebra R m) →ₐ[R] A)) : (pointsMulEquiv R m) f = pointToUpperUnitriangular R m f

The forward map of pointsMulEquiv is evaluation on the generic matrix.

@[simp]

theorem TauCeti.UpperUnitriangular.pointsMulEquiv_symm_apply (R : Type u) [CommRing R] (m : Type v) [Fintype m] [LinearOrder m] {A : Type w} [CommRing A] [Algebra R A] (g : ↥(upperUnitriangularGroup m A)) : (pointsMulEquiv R m).symm g = upperUnitriangularToPoint R m g

The inverse map of pointsMulEquiv is polynomial evaluation on strict-upper entries.

theorem TauCeti.UpperUnitriangular.pointToUpperUnitriangular_mapValue (R : Type u) [CommRing R] (m : Type v) [Fintype m] [LinearOrder m] {A : Type w} [CommRing A] [Algebra R A] {B : Type u_1} [CommRing B] [Algebra R B] (φ : A →ₐ[R] B) (f : WithConv (↑(coordinateHopfAlgebra R m) →ₐ[R] A)) : pointToUpperUnitriangular R m ((AlgHom.mapValue φ) f) = (UpperUnitriangularGroup.map φ.toRingHom) (pointToUpperUnitriangular R m f)

Reading a point as an upper-unitriangular matrix commutes with maps of value algebras.

theorem TauCeti.UpperUnitriangular.pointsMulEquiv_mapValue (R : Type u) [CommRing R] (m : Type v) [Fintype m] [LinearOrder m] {A : Type w} [CommRing A] [Algebra R A] {B : Type u_1} [CommRing B] [Algebra R B] (φ : A →ₐ[R] B) (f : WithConv (↑(coordinateHopfAlgebra R m) →ₐ[R] A)) : (pointsMulEquiv R m) ((AlgHom.mapValue φ) f) = (UpperUnitriangularGroup.map φ.toRingHom) ((pointsMulEquiv R m) f)

The pointwise group equivalence is natural in the value algebra.

theorem TauCeti.UpperUnitriangular.mapValue_pointsMulEquiv_symm_apply (R : Type u) [CommRing R] (m : Type v) [Fintype m] [LinearOrder m] {A : Type w} [CommRing A] [Algebra R A] {B : Type u_1} [CommRing B] [Algebra R B] (φ : A →ₐ[R] B) (g : ↥(upperUnitriangularGroup m A)) : (AlgHom.mapValue φ) ((pointsMulEquiv R m).symm g) = (pointsMulEquiv R m).symm ((UpperUnitriangularGroup.map φ.toRingHom) g)

Naturality of the inverse pointwise equivalence in the value algebra.

noncomputable def TauCeti.UpperUnitriangular.upperUnitriangularFunctor (R : Type u) [CommRing R] (m : Type v) [Fintype m] [LinearOrder m] : CategoryTheory.Functor (CommAlgCat R) GrpCat

The group-valued functor sending a commutative R-algebra to its upper-unitriangular 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

• TauCeti.UpperUnitriangular.upperUnitriangularFunctor R m = (TauCeti.UpperUnitriangular.upperUnitriangularFunctorUnlifted✝ R m).comp GrpCat.uliftFunctor

theorem TauCeti.UpperUnitriangular.upperUnitriangularFunctor_obj (R : Type u) [CommRing R] (m : Type v) [Fintype m] [LinearOrder m] (A : CommAlgCat R) : (upperUnitriangularFunctor R m).obj A = ↧(ULift.{u, max v w} ↥(upperUnitriangularGroup m ↑A))

The object part of upperUnitriangularFunctor is the universe lift of the ordinary upper-unitriangular group.

theorem TauCeti.UpperUnitriangular.upperUnitriangularFunctor_map (R : Type u) [CommRing R] (m : Type v) [Fintype m] [LinearOrder m] {A B : CommAlgCat R} (φ : A ⟶ B) : (upperUnitriangularFunctor R m).map φ = CategoryTheory.CategoryStruct.comp (CategoryTheory.eqToHom ⋯) (CategoryTheory.CategoryStruct.comp (GrpCat.ofHom (MulEquiv.ulift.symm.toMonoidHom.comp ((UpperUnitriangularGroup.map (CommAlgCat.Hom.hom φ).toRingHom).comp MulEquiv.ulift.toMonoidHom))) (CategoryTheory.eqToHom ⋯))

The morphism part of upperUnitriangularFunctor applies the value-algebra map entrywise.

@[simp]

theorem TauCeti.UpperUnitriangular.upperUnitriangularFunctor_map_apply_apply (R : Type u) [CommRing R] (m : Type v) [Fintype m] [LinearOrder m] {A B : CommAlgCat R} (φ : A ⟶ B) (g : ULift.{u, max v w} ↥(upperUnitriangularGroup m ↑A)) (i j : m) : ↑↑((CategoryTheory.ConcreteCategory.hom (CategoryTheory.eqToHom ⋯)) ((CategoryTheory.ConcreteCategory.hom ((upperUnitriangularFunctor R m).map φ)) ((CategoryTheory.ConcreteCategory.hom (CategoryTheory.eqToHom ⋯)) g))).down i j = (CommAlgCat.Hom.hom φ) (↑↑g.down i j)

Entrywise computation of a value-algebra map on the upper-unitriangular functor.

noncomputable def TauCeti.UpperUnitriangular.pointsNatIso (R : Type u) [CommRing R] (m : Type v) [Fintype m] [LinearOrder m] : HopfAlgebra.pointsFunctor ≅ upperUnitriangularFunctor R m

The convolution-points functor of the upper-unitriangular coordinate Hopf algebra is naturally isomorphic to the ordinary upper-unitriangular group functor.

Equations

• One or more equations did not get rendered due to their size.

@[simp]

theorem TauCeti.UpperUnitriangular.pointsNatIso_hom_app_apply (R : Type u) [CommRing R] (m : Type v) [Fintype m] [LinearOrder m] (A : CommAlgCat R) (f : ↑(HopfAlgebra.points A)) : ((CategoryTheory.ConcreteCategory.hom (CategoryTheory.eqToHom ⋯)) ((CategoryTheory.ConcreteCategory.hom ((pointsNatIso R m).hom.app A)) f)).down = (pointsMulEquiv R m) f

After transport along upperUnitriangularFunctor_obj, the forward component of pointsNatIso is the pointwise upper-unitriangular equivalence.

@[simp]

theorem TauCeti.UpperUnitriangular.pointsNatIso_inv_app_apply (R : Type u) [CommRing R] (m : Type v) [Fintype m] [LinearOrder m] (A : CommAlgCat R) (g : ULift.{u, max v w} ↥(upperUnitriangularGroup m ↑A)) : (CategoryTheory.ConcreteCategory.hom ((pointsNatIso R m).inv.app A)) ((CategoryTheory.ConcreteCategory.hom (CategoryTheory.eqToHom ⋯)) g) = (pointsMulEquiv R m).symm g.down

After transport back along upperUnitriangularFunctor_obj, the inverse component of pointsNatIso is polynomial evaluation on strict-upper entries.