The upper-unitriangular coordinate Hopf algebra

For a commutative ring R, inversion of the generic upper-unitriangular matrix equips its coordinate bialgebra with an antipode. This file packages that structure as a commutative Hopf algebra and records that its polynomial coordinate ring is of finite type.

This is the coordinate-Hopf-algebra part of the upper-unitriangular model in Layer 5, "Unipotent groups", of the ReductiveGroups roadmap. A subsequent closed-immersion module can identify its map to GL_m with the corresponding Hopf-ideal quotient.

Main declarations

• TauCeti.UpperUnitriangular.antipode: inverse-matrix evaluation on the coordinate ring.
• TauCeti.UpperUnitriangular.coordinateHopfAlgebra: its bundled commutative Hopf algebra.
• TauCeti.UpperUnitriangular.finiteTypeCoordinateHopfAlgebra: its finite-type package.

References

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

The layout follows TauCeti.GeneralLinear in GeneralLinear.Coordinate.HopfAlgebra.

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

Inverse-matrix antipode on the coordinate ring of U_m.

Equations

• TauCeti.UpperUnitriangular.antipode R m = MvPolynomial.aeval fun (ij : TauCeti.UpperUnitriangular.Index m) => ↑⋯.toGL⁻¹ (↑ij).1 (↑ij).2

theorem TauCeti.UpperUnitriangular.isUpperUnitriangular_inv_genericMatrix (R : Type u) [CommRing R] (m : Type v) [Fintype m] [LinearOrder m] : (genericMatrix R m)⁻¹.IsUpperUnitriangular

The inverse of the generic matrix is upper unitriangular.

@[simp]

theorem TauCeti.UpperUnitriangular.map_antipode_genericMatrix (R : Type u) [CommRing R] (m : Type v) [Fintype m] [LinearOrder m] : (genericMatrix R m).map ⇑(antipode R m) = (genericMatrix R m)⁻¹

The antipode evaluates the generic matrix at its inverse.

@[simp]

theorem TauCeti.UpperUnitriangular.antipode_genericMatrix_apply (R : Type u) [CommRing R] (m : Type v) [Fintype m] [LinearOrder m] (i j : m) : (antipode R m) (genericMatrix R m i j) = (genericMatrix R m)⁻¹ i j

The antipode on every generic matrix entry is the corresponding inverse-matrix entry.

@[simp]

theorem TauCeti.UpperUnitriangular.antipode_X (R : Type u) [CommRing R] (m : Type v) [Fintype m] [LinearOrder m] (ij : Index m) : (antipode R m) (MvPolynomial.X ij) = (genericMatrix R m)⁻¹ (↑ij).1 (↑ij).2

The antipode sends a strict-upper coordinate to the corresponding inverse-matrix entry.

noncomputable def TauCeti.UpperUnitriangular.coordinateHopfAlgebra (R : Type u) [CommRing R] (m : Type v) [Fintype m] [LinearOrder m] : CommHopfAlgCat R

The coordinate ring bundled with its upper-unitriangular Hopf-algebra structure.

Equations

• TauCeti.UpperUnitriangular.coordinateHopfAlgebra R m = ↧(TauCeti.UpperUnitriangular.CoordinateRing R m)

noncomputable def TauCeti.UpperUnitriangular.coordinateHopfAlgebraAlgEquiv (R : Type u) [CommRing R] (m : Type v) [Fintype m] [LinearOrder m] : CoordinateRing R m ≃ₐ[R] ↑(coordinateHopfAlgebra R m)

The identity algebra equivalence to the bundled coordinate Hopf algebra.

Equations

• TauCeti.UpperUnitriangular.coordinateHopfAlgebraAlgEquiv R m = AlgEquiv.refl

@[simp]

theorem TauCeti.UpperUnitriangular.coordinateHopfAlgebra_comul_apply (R : Type u) [CommRing R] (m : Type v) [Fintype m] [LinearOrder m] (x : CoordinateRing R m) : CoalgebraStruct.comul ((coordinateHopfAlgebraAlgEquiv R m) x) = (Algebra.TensorProduct.map ↑(coordinateHopfAlgebraAlgEquiv R m) ↑(coordinateHopfAlgebraAlgEquiv R m)) ((comul R m) x)

The bundled comultiplication agrees with matrix multiplication on the raw coordinate ring.

@[simp]

theorem TauCeti.UpperUnitriangular.coordinateHopfAlgebra_counit_apply (R : Type u) [CommRing R] (m : Type v) [Fintype m] [LinearOrder m] (x : CoordinateRing R m) : CoalgebraStruct.counit ((coordinateHopfAlgebraAlgEquiv R m) x) = (counit R m) x

The bundled counit agrees with evaluation at the identity matrix.

@[simp]

theorem TauCeti.UpperUnitriangular.coordinateHopfAlgebra_antipode_apply (R : Type u) [CommRing R] (m : Type v) [Fintype m] [LinearOrder m] (x : CoordinateRing R m) : (HopfAlgebraStruct.antipode R) ((coordinateHopfAlgebraAlgEquiv R m) x) = (coordinateHopfAlgebraAlgEquiv R m) ((antipode R m) x)

The bundled antipode agrees with inverse-matrix evaluation on the raw coordinate ring.

@[simp]

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

The bundled comultiplication formula on a strict-upper coordinate.

@[simp]

theorem TauCeti.UpperUnitriangular.coordinateHopfAlgebra_counit_X (R : Type u) [CommRing R] (m : Type v) [Fintype m] [LinearOrder m] (ij : Index m) : CoalgebraStruct.counit ((coordinateHopfAlgebraAlgEquiv R m) (MvPolynomial.X ij)) = 0

The bundled counit vanishes on every strict-upper coordinate.

@[simp]

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

The bundled comultiplication formula on every generic matrix entry.

@[simp]

theorem TauCeti.UpperUnitriangular.coordinateHopfAlgebra_counit_genericMatrix_apply (R : Type u) [CommRing R] (m : Type v) [Fintype m] [LinearOrder m] (i j : m) : CoalgebraStruct.counit ((coordinateHopfAlgebraAlgEquiv R m) (genericMatrix R m i j)) = if i = j then 1 else 0

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

@[simp]

theorem TauCeti.UpperUnitriangular.coordinateHopfAlgebra_antipode_X (R : Type u) [CommRing R] (m : Type v) [Fintype m] [LinearOrder m] (ij : Index m) : (HopfAlgebraStruct.antipode R) ((coordinateHopfAlgebraAlgEquiv R m) (MvPolynomial.X ij)) = (coordinateHopfAlgebraAlgEquiv R m) ((genericMatrix R m)⁻¹ (↑ij).1 (↑ij).2)

The bundled antipode sends a strict-upper coordinate to the corresponding inverse-matrix entry.

@[simp]

theorem TauCeti.UpperUnitriangular.coordinateHopfAlgebra_antipode_genericMatrix_apply (R : Type u) [CommRing R] (m : Type v) [Fintype m] [LinearOrder m] (i j : m) : (HopfAlgebraStruct.antipode R) ((coordinateHopfAlgebraAlgEquiv R m) (genericMatrix R m i j)) = (coordinateHopfAlgebraAlgEquiv R m) ((genericMatrix R m)⁻¹ i j)

The bundled antipode sends a generic entry to the corresponding inverse-matrix entry.

noncomputable def TauCeti.UpperUnitriangular.finiteTypeCoordinateHopfAlgebra (R : Type u) [CommRing R] (m : Type v) [Fintype m] [LinearOrder m] : FiniteTypeCommHopfAlgCat R

coordinateHopfAlgebra bundled as a finite-type commutative Hopf algebra, using that its polynomial coordinate ring is a finitely generated R-algebra.

Equations

• TauCeti.UpperUnitriangular.finiteTypeCoordinateHopfAlgebra R m = TauCeti.FiniteTypeCommHopfAlgCat.of R (TauCeti.UpperUnitriangular.CoordinateRing R m)

@[simp]

theorem TauCeti.UpperUnitriangular.finiteTypeCoordinateHopfAlgebra_obj (R : Type u) [CommRing R] (m : Type v) [Fintype m] [LinearOrder m] : (finiteTypeCoordinateHopfAlgebra R m).obj = coordinateHopfAlgebra R m

The underlying Hopf algebra of the finite-type package is coordinateHopfAlgebra.

theorem TauCeti.UpperUnitriangular.coordinateHopfAlgebra_algHom_ext (R : Type u) [CommRing R] (m : Type v) [Fintype m] [LinearOrder m] {T : Type u_1} [Semiring T] [Algebra R T] {f g : ↑(coordinateHopfAlgebra R m) →ₐ[R] T} (h : ∀ (ij : Index m), f ((coordinateHopfAlgebraAlgEquiv R m) (MvPolynomial.X ij)) = g ((coordinateHopfAlgebraAlgEquiv R m) (MvPolynomial.X ij))) : f = g

Two algebra homomorphisms out of the bundled coordinate Hopf algebra are equal if they agree on every strict-upper coordinate.

theorem TauCeti.UpperUnitriangular.coordinateHopfAlgebra_algHom_ext_iff {R : Type u} [CommRing R] {m : Type v} [Fintype m] [LinearOrder m] {T : Type u_1} [Semiring T] [Algebra R T] {f g : ↑(coordinateHopfAlgebra R m) →ₐ[R] T} : f = g ↔ ∀ (ij : Index m), f ((coordinateHopfAlgebraAlgEquiv R m) (MvPolynomial.X ij)) = g ((coordinateHopfAlgebraAlgEquiv R m) (MvPolynomial.X ij))