The upper-unitriangular group is unipotent

For a natural number n, corestricting the standard O(GL_n)-comodule along O(GL_n) → O(U_n) gives the standard comodule of O(U_n) on R^n. Its coaction is given by the generic upper-unitriangular matrix. Its coordinate morphism is the closed immersion U_n → GL_n, so this comodule is faithful. At every point its action is the corresponding upper-unitriangular matrix, hence is unipotent. The faithful-representation criterion then proves that every geometric point of U_n is unipotent.

The coordinate ring is a polynomial algebra in the entries strictly above the diagonal. It is therefore smooth; over a field this makes U_n a smooth unipotent affine group.

Main declarations

• TauCeti.UpperUnitriangular.standardComodule: the standard faithful comodule of O(U_n).
• TauCeti.UpperUnitriangular.isUnipotentPoint: every point of U_n valued in a perfect field extension is unipotent.
• TauCeti.UpperUnitriangular.smoothUnipotentCommHopfAlgProperty_coordinateHopfAlgebra: U_n over a field is smooth unipotent.

References

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

noncomputable def TauCeti.UpperUnitriangular.standardCoact (R : Type u) [CommRing R] (n : ℕ) : (Fin n → R) →ₗ[R] TensorProduct R (Fin n → R) ↑(coordinateHopfAlgebra R (Fin n))

The standard coaction of O(U_n) on column vectors. On the j-th basis vector it is the j-th column of the generic upper-unitriangular matrix.

Equations

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

@[simp]

theorem TauCeti.UpperUnitriangular.standardCoact_apply_basisFun (R : Type u) [CommRing R] (n : ℕ) (j : Fin n) : (standardCoact R n) (Pi.single j 1) = ∑ i : Fin n, Pi.single i 1 ⊗ₜ[R] (coordinateHopfAlgebraAlgEquiv R (Fin n)) (genericMatrix R (Fin n) i j)

The standard coaction on a basis vector is the corresponding column of the generic matrix.

@[instance_reducible]

noncomputable def TauCeti.UpperUnitriangular.standardComodule (R : Type u) [CommRing R] (n : ℕ) : Comodule R (↑(coordinateHopfAlgebra R (Fin n))) (Fin n → R)

The standard right comodule of the upper-unitriangular coordinate Hopf algebra, obtained by corestricting the standard general-linear comodule along O(GL_n) → O(U_n).

Equations

• TauCeti.UpperUnitriangular.standardComodule R n = TauCeti.Comodule.Corestrict (CommHopfAlgCat.Hom.hom (TauCeti.UpperUnitriangular.coordinateMap R n)).toCoalgHom

theorem TauCeti.UpperUnitriangular.standardComodule_coact (R : Type u) [CommRing R] (n : ℕ) : Comodule.coact = standardCoact R n

The coaction of the standard comodule is standardCoact.

theorem TauCeti.UpperUnitriangular.coefficientMatrix_basisFun (R : Type u) [CommRing R] (n : ℕ) : Comodule.coefficientMatrix (Pi.basisFun R (Fin n)) = fun (i j : Fin n) => (coordinateHopfAlgebraAlgEquiv R (Fin n)) (genericMatrix R (Fin n) i j)

The coefficient matrix of the standard comodule is the generic upper-unitriangular matrix.

theorem TauCeti.UpperUnitriangular.coordinateBialgHom_basisFun (R : Type u) [CommRing R] (n : ℕ) : Comodule.coordinateBialgHom (Pi.basisFun R (Fin n)) = CommHopfAlgCat.Hom.hom (coordinateMap R n)

The coordinate morphism of the standard comodule is the coordinate morphism of the closed immersion U_n → GL_n.

theorem TauCeti.UpperUnitriangular.isFaithful_standardComodule (R : Type u) [CommRing R] (n : ℕ) : Comodule.IsFaithful

The standard comodule of U_n is faithful.

@[reducible, inline]

noncomputable abbrev TauCeti.UpperUnitriangular.standardScalarExtensionEquiv (R : Type u) [CommRing R] (n : ℕ) {A : Type w} [CommRing A] [Algebra R A] : TensorProduct R A (Fin n → R) ≃ₗ[A] Fin n → A

The canonical identification of the scalar extension of the standard module with A^n.

Equations

• TauCeti.UpperUnitriangular.standardScalarExtensionEquiv R n = TensorProduct.piScalarRight R A A (Fin n)

theorem TauCeti.UpperUnitriangular.standardScalarExtensionEquiv_comp_endOfPoint (R : Type u) [CommRing R] (n : ℕ) {A : Type w} [CommRing A] [Algebra R A] (g : WithConv (↑(coordinateHopfAlgebra R (Fin n)) →ₐ[R] A)) : ↑(standardScalarExtensionEquiv R n) ∘ₗ Comodule.endOfPoint (Fin n → R) g.ofConv = ↑(Matrix.GeneralLinearGroup.toLin ↑(pointToUpperUnitriangular R (Fin n) g)) ∘ₗ ↑(standardScalarExtensionEquiv R n)

Under the canonical scalar-extension equivalence, a point acts through its associated upper-unitriangular matrix.

theorem TauCeti.UpperUnitriangular.congrLinearEquiv_pointsAction_eq_toLin (R : Type u) [CommRing R] (n : ℕ) {A : Type w} [CommRing A] [Algebra R A] (g : WithConv (↑(coordinateHopfAlgebra R (Fin n)) →ₐ[R] A)) : LinearMap.GeneralLinearGroup.ofLinearEquiv ((standardScalarExtensionEquiv R n).symm ≪≫ₗ ((LinearMap.GeneralLinearGroup.ofLinearEquiv ((Comodule.pointsAction (Fin n → R)) g)).toLinearEquiv ≪≫ₗ standardScalarExtensionEquiv R n)) = Matrix.GeneralLinearGroup.toLin ↑(pointToUpperUnitriangular R (Fin n) g)

Transporting the standard point action to A^n gives the natural linear action of the associated upper-unitriangular matrix.

theorem TauCeti.UpperUnitriangular.isUnipotent_pointsAction (R : Type u) [CommRing R] (n : ℕ) {A : Type w} [CommRing A] [Algebra R A] (g : WithConv (↑(coordinateHopfAlgebra R (Fin n)) →ₐ[R] A)) : (LinearMap.GeneralLinearGroup.ofLinearEquiv ((Comodule.pointsAction (Fin n → R)) g)).IsUnipotent

The standard representation sends every point of U_n to a unipotent automorphism.

theorem TauCeti.UpperUnitriangular.isUnipotentPoint (n : ℕ) {k K : Type u} [Field k] [Field K] [Algebra k K] [PerfectField K] (g : WithConv (↑(coordinateHopfAlgebra k (Fin n)) →ₐ[k] K)) : HopfAlgebra.IsUnipotentPoint g

Every point of the upper-unitriangular coordinate Hopf algebra over a perfect field is unipotent.

theorem TauCeti.UpperUnitriangular.geometricallyUnipotentPointsCommHopfAlgProperty_coordinateHopfAlgebra (n : ℕ) (k : Type u) [Field k] : geometricallyUnipotentPointsCommHopfAlgProperty k (coordinateHopfAlgebra k (Fin n))

The upper-unitriangular group has only unipotent geometric points.

theorem TauCeti.UpperUnitriangular.smoothUnipotentCommHopfAlgProperty_coordinateHopfAlgebra (n : ℕ) (k : Type u) [Field k] : smoothUnipotentCommHopfAlgProperty k (finiteTypeCoordinateHopfAlgebra k (Fin n))

The upper-unitriangular group is a smooth unipotent affine group.