The upper-unitriangular coordinate bialgebra

For a commutative semiring R, the coordinate ring of the upper-unitriangular matrix monoid U_m is the polynomial algebra on entries strictly above the diagonal. Its generic matrix has ones on the diagonal and zeros below it. Matrix multiplication and the identity matrix give its comultiplication and counit.

This is the semiring-level dependency layer for the upper-unitriangular coordinate Hopf algebra; the antipode and finite-type Hopf package are constructed separately over commutative rings.

Main declarations

• TauCeti.UpperUnitriangular.CoordinateRing: the polynomial coordinate ring of U_m.
• TauCeti.UpperUnitriangular.genericMatrix: the generic upper-unitriangular matrix.
• TauCeti.UpperUnitriangular.comul and TauCeti.UpperUnitriangular.counit: the raw structure maps.
• TauCeti.UpperUnitriangular.comul_coassoc: the comultiplication is coassociative.
• TauCeti.UpperUnitriangular.comul_rTensor_counit and TauCeti.UpperUnitriangular.comul_lTensor_counit: the two counit laws.

References

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

The construction follows the coordinate-bialgebra layout of TauCeti.MatrixMonoid in GeneralLinear.Coordinate.Bialgebra.

@[reducible, inline]

abbrev TauCeti.UpperUnitriangular.Index (m : Type u_1) [LT m] : Type u_1

Pairs indexing the entries strictly above the diagonal of a square matrix.

Equations

• TauCeti.UpperUnitriangular.Index m = { ij : m × m // ij.1 < ij.2 }

@[reducible, inline]

abbrev TauCeti.UpperUnitriangular.CoordinateRing (R : Type u) [CommSemiring R] (m : Type u_1) [LT m] : Type (max u u_1)

The polynomial coordinate ring of the upper-unitriangular matrix monoid.

Equations

• TauCeti.UpperUnitriangular.CoordinateRing R m = MvPolynomial (TauCeti.UpperUnitriangular.Index m) R

noncomputable def TauCeti.UpperUnitriangular.genericMatrix (R : Type u) [CommSemiring R] (m : Type v) [LinearOrder m] : Matrix m m (CoordinateRing R m)

The generic upper-unitriangular matrix.

Equations

• TauCeti.UpperUnitriangular.genericMatrix R m i j = if h : i < j then MvPolynomial.X (have this := ⟨(i, j), h⟩; this) else if i = j then 1 else 0

@[simp]

theorem TauCeti.UpperUnitriangular.genericMatrix_apply_of_lt (R : Type u) [CommSemiring R] (m : Type v) [LinearOrder m] {i j : m} (h : i < j) : genericMatrix R m i j = MvPolynomial.X (have this := ⟨(i, j), h⟩; this)

Above the diagonal, the generic matrix is the corresponding polynomial coordinate.

@[simp]

theorem TauCeti.UpperUnitriangular.genericMatrix_apply_diag (R : Type u) [CommSemiring R] (m : Type v) [LinearOrder m] (i : m) : genericMatrix R m i i = 1

The generic matrix has ones on the diagonal.

@[simp]

theorem TauCeti.UpperUnitriangular.genericMatrix_apply_eq_zero_of_gt (R : Type u) [CommSemiring R] (m : Type v) [LinearOrder m] {i j : m} (h : j < i) : genericMatrix R m i j = 0

The generic matrix vanishes below the diagonal.

theorem TauCeti.UpperUnitriangular.isUpperUnitriangular_genericMatrix (R : Type u) [CommSemiring R] (m : Type v) [LinearOrder m] : (genericMatrix R m).IsUpperUnitriangular

The generic matrix is upper unitriangular.

theorem TauCeti.UpperUnitriangular.map_aeval_genericMatrix (R : Type u) [CommSemiring R] (m : Type v) [LinearOrder m] {A : Type w} [CommSemiring A] [Algebra R A] (M : Matrix m m A) (hM : M.IsUpperUnitriangular) : (genericMatrix R m).map ⇑(MvPolynomial.aeval fun (ij : Index m) => M (↑ij).1 (↑ij).2) = M

Evaluating the strict-upper coordinates of the generic matrix at an upper-unitriangular matrix recovers that matrix.

noncomputable def TauCeti.UpperUnitriangular.comul (R : Type u) [CommSemiring R] (m : Type v) [LinearOrder m] [Fintype m] : CoordinateRing R m →ₐ[R] TensorProduct R (CoordinateRing R m) (CoordinateRing R m)

Matrix-multiplication comultiplication on the coordinate ring of U_m.

Equations

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

noncomputable def TauCeti.UpperUnitriangular.counit (R : Type u) [CommSemiring R] (m : Type v) [LinearOrder m] : CoordinateRing R m →ₐ[R] R

Identity-matrix counit on the coordinate ring of U_m.

Equations

• TauCeti.UpperUnitriangular.counit R m = MvPolynomial.aeval fun (ij : TauCeti.UpperUnitriangular.Index m) => 1 (↑ij).1 (↑ij).2

@[simp]

theorem TauCeti.UpperUnitriangular.map_comul_genericMatrix (R : Type u) [CommSemiring R] (m : Type v) [LinearOrder m] [Fintype m] : (genericMatrix R m).map ⇑(comul R m) = (genericMatrix R m).map ⇑Algebra.TensorProduct.includeLeft * (genericMatrix R m).map ⇑Algebra.TensorProduct.includeRight

Comultiplication evaluates the generic matrix at the product of its two tensor-factor copies.

@[simp]

theorem TauCeti.UpperUnitriangular.map_counit_genericMatrix (R : Type u) [CommSemiring R] (m : Type v) [LinearOrder m] : (genericMatrix R m).map ⇑(counit R m) = 1

The counit evaluates the generic matrix at the identity.

@[simp]

theorem TauCeti.UpperUnitriangular.comul_genericMatrix_apply (R : Type u) [CommSemiring R] (m : Type v) [LinearOrder m] [Fintype m] (i j : m) : (comul R m) (genericMatrix R m i j) = ∑ k : m, genericMatrix R m i k ⊗ₜ[R] genericMatrix R m k j

Comultiplication on every generic matrix entry is matrix multiplication.

@[simp]

theorem TauCeti.UpperUnitriangular.counit_genericMatrix_apply (R : Type u) [CommSemiring R] (m : Type v) [LinearOrder m] (i j : m) : (counit R m) (genericMatrix R m i j) = if i = j then 1 else 0

The counit on every generic matrix entry is the corresponding identity-matrix entry.

@[simp]

theorem TauCeti.UpperUnitriangular.comul_X (R : Type u) [CommSemiring R] (m : Type v) [LinearOrder m] [Fintype m] (ij : Index m) : (comul R m) (MvPolynomial.X ij) = ∑ k : m, genericMatrix R m (↑ij).1 k ⊗ₜ[R] genericMatrix R m k (↑ij).2

Comultiplication on a strict-upper coordinate is the corresponding entry of the product of the two generic matrices.

@[simp]

theorem TauCeti.UpperUnitriangular.counit_X (R : Type u) [CommSemiring R] (m : Type v) [LinearOrder m] (ij : Index m) : (counit R m) (MvPolynomial.X ij) = 0

The counit vanishes on every strict-upper coordinate.

theorem TauCeti.UpperUnitriangular.comul_coassoc (R : Type u) [CommSemiring R] (m : Type v) [LinearOrder m] [Fintype m] : (↑(Algebra.TensorProduct.assoc R R R (CoordinateRing R m) (CoordinateRing R m) (CoordinateRing R m))).comp ((Algebra.TensorProduct.map (comul R m) (AlgHom.id R (CoordinateRing R m))).comp (comul R m)) = (Algebra.TensorProduct.map (AlgHom.id R (CoordinateRing R m)) (comul R m)).comp (comul R m)

Matrix-multiplication comultiplication is coassociative.

theorem TauCeti.UpperUnitriangular.comul_rTensor_counit (R : Type u) [CommSemiring R] (m : Type v) [LinearOrder m] [Fintype m] : (Algebra.TensorProduct.map (counit R m) (AlgHom.id R (CoordinateRing R m))).comp (comul R m) = ↑(Algebra.TensorProduct.lid R (CoordinateRing R m)).symm

Applying the counit in the left tensor factor is the left-unit identification.

theorem TauCeti.UpperUnitriangular.comul_lTensor_counit (R : Type u) [CommSemiring R] (m : Type v) [LinearOrder m] [Fintype m] : (Algebra.TensorProduct.map (AlgHom.id R (CoordinateRing R m)) (counit R m)).comp (comul R m) = ↑(Algebra.TensorProduct.rid R R (CoordinateRing R m)).symm

Applying the counit in the right tensor factor is the right-unit identification.