The matrix-monoid coordinate bialgebra

For a commutative semiring R, this file equips the polynomial coordinate algebra R[Xᵢⱼ] of square matrices with the explicit bialgebra structure dual to matrix multiplication. Its comultiplication and counit satisfy

Δ(Xᵢⱼ) = ∑ₖ Xᵢₖ ⊗ Xₖⱼ and ε(Xᵢⱼ) = if i = j then 1 else 0.

The structure is a named Bialgebra value rather than a global instance. This distinction is essential: MvPolynomial is definitionally an additive monoid algebra, and importing the monoid-algebra bialgebra gives its variables a different, group-like comultiplication. Over a commutative ring, coordinateBialgebra locally selects the matrix-coordinate structure and stores it in a CommBialgCat object, providing a collision-free boundary for statements using typeclass-selected coalgebra operations.

The determinant of the generic matrix is group-like for this bundled structure. This is the algebraic input for subsequently localizing at the determinant to construct the coordinate Hopf algebra of GLₙ; localization and the antipode are deliberately not constructed here.

The construction includes n = 0 and requires no nontriviality hypothesis on the base.

Main declarations

• TauCeti.MatrixMonoid.comul: matrix-multiplication comultiplication on R[Xᵢⱼ].
• TauCeti.MatrixMonoid.counit: identity-matrix counit on R[Xᵢⱼ].
• TauCeti.MatrixMonoid.bialgebra: the explicit matrix-coordinate bialgebra dictionary.
• TauCeti.MatrixMonoid.coordinateBialgebra: the selected commutative bialgebra object.
• TauCeti.MatrixMonoid.isGroupLikeElem_determinant: the generic determinant is group-like.

References

The coordinate formulas are standard; see J. S. Milne, Algebraic Groups, §§3.3--3.6 and 4.2. The same construction appears in the Stacks Project, Example 39.5.4, Tag 022W. The role of determinant localization in constructing GLₙ is described in Milne, §2.8.

@[reducible, inline]

abbrev TauCeti.MatrixMonoid.CoordinateRing (R : Type u) [CommSemiring R] (n : ℕ) : Type u

The polynomial coordinate algebra of the monoid of n × n matrices over R.

Equations

• TauCeti.MatrixMonoid.CoordinateRing R n = MvPolynomial (Fin n × Fin n) R

noncomputable def TauCeti.MatrixMonoid.comul (R : Type u) [CommSemiring R] (n : ℕ) : CoordinateRing R n →ₐ[R] TensorProduct R (CoordinateRing R n) (CoordinateRing R n)

The comultiplication dual to multiplication of square matrices.

Equations

• TauCeti.MatrixMonoid.comul R n = MvPolynomial.aeval fun (ij : Fin n × Fin n) => ∑ k : Fin n, MvPolynomial.X (ij.1, k) ⊗ₜ[R] MvPolynomial.X (k, ij.2)

noncomputable def TauCeti.MatrixMonoid.counit (R : Type u) [CommSemiring R] (n : ℕ) : CoordinateRing R n →ₐ[R] R

The counit dual to the identity matrix.

Equations

• TauCeti.MatrixMonoid.counit R n = MvPolynomial.aeval fun (ij : Fin n × Fin n) => 1 ij.1 ij.2

@[simp]

theorem TauCeti.MatrixMonoid.comul_X (R : Type u) [CommSemiring R] (n : ℕ) (i j : Fin n) : (comul R n) (MvPolynomial.X (i, j)) = ∑ k : Fin n, MvPolynomial.X (i, k) ⊗ₜ[R] MvPolynomial.X (k, j)

The matrix-coordinate comultiplication sends a generic entry to the corresponding entry of the product of the generic matrices in the two tensor factors.

@[simp]

theorem TauCeti.MatrixMonoid.counit_X (R : Type u) [CommSemiring R] (n : ℕ) (i j : Fin n) : (counit R n) (MvPolynomial.X (i, j)) = if i = j then 1 else 0

The matrix-coordinate counit sends a generic entry to the corresponding identity-matrix entry.

@[simp]

theorem TauCeti.MatrixMonoid.map_counit_genericMatrix (R : Type u) [CommSemiring R] (n : ℕ) : (Matrix.mvPolynomialX (Fin n) (Fin n) R).map ⇑(counit R n) = 1

Applying the counit entrywise to the generic matrix gives the identity matrix.

@[simp]

theorem TauCeti.MatrixMonoid.map_comul_genericMatrix (R : Type u) [CommSemiring R] (n : ℕ) : (Matrix.mvPolynomialX (Fin n) (Fin n) R).map ⇑(comul R n) = (Matrix.mvPolynomialX (Fin n) (Fin n) R).map ⇑Algebra.TensorProduct.includeLeft * (Matrix.mvPolynomialX (Fin n) (Fin n) R).map ⇑Algebra.TensorProduct.includeRight

Applying the comultiplication entrywise to the generic matrix gives the product of its left-tensor and right-tensor copies. The order represents ordinary matrix multiplication, not the opposite monoid.

@[instance_reducible]

noncomputable def TauCeti.MatrixMonoid.bialgebra (R : Type u) [CommSemiring R] (n : ℕ) : Bialgebra R (CoordinateRing R n)

The matrix-coordinate bialgebra structure on the polynomial algebra R[Xᵢⱼ].

This is intentionally a named value, not an instance. Callers that need typeclass-selected coalgebra operations should use coordinateBialgebra, or install this value in a deliberately local scope.

Equations

• TauCeti.MatrixMonoid.bialgebra R n = Bialgebra.ofAlgHom (TauCeti.MatrixMonoid.comul R n) (TauCeti.MatrixMonoid.counit R n) ⋯ ⋯ ⋯

theorem TauCeti.MatrixMonoid.bialgebra_comul (R : Type u) [CommSemiring R] (n : ℕ) : CoalgebraStruct.comul ≍ (comul R n).toLinearMap

Selecting bialgebra R n makes its comultiplication the explicit matrix-multiplication map comul R n. The equality is heterogeneous because opacity also hides the dictionary's stored module structure.

theorem TauCeti.MatrixMonoid.bialgebra_counit (R : Type u) [CommSemiring R] (n : ℕ) : CoalgebraStruct.counit ≍ (counit R n).toLinearMap

Selecting bialgebra R n makes its counit the explicit identity-matrix map counit R n. As for bialgebra_comul, opacity makes the map equality heterogeneous.

@[simp]

theorem TauCeti.MatrixMonoid.bialgebra_comul_X (R : Type u) [CommSemiring R] (n : ℕ) (i j : Fin n) : CoalgebraStruct.comul (MvPolynomial.X (i, j)) = ∑ k : Fin n, MvPolynomial.X (i, k) ⊗ₜ[R] MvPolynomial.X (k, j)

Under bialgebra R n, comultiplication has the matrix-multiplication formula on generators.

@[simp]

theorem TauCeti.MatrixMonoid.bialgebra_counit_X (R : Type u) [CommSemiring R] (n : ℕ) (i j : Fin n) : CoalgebraStruct.counit (MvPolynomial.X (i, j)) = if i = j then 1 else 0

Under bialgebra R n, the counit has the identity-matrix formula on generators.

@[simp]

theorem TauCeti.MatrixMonoid.counit_determinant (R : Type u) [CommRing R] (n : ℕ) : (counit R n) (Matrix.mvPolynomialX (Fin n) (Fin n) R).det = 1

Evaluating the generic determinant at the identity-matrix counit gives one.

@[simp]

theorem TauCeti.MatrixMonoid.comul_determinant (R : Type u) [CommRing R] (n : ℕ) : (comul R n) (Matrix.mvPolynomialX (Fin n) (Fin n) R).det = (Matrix.mvPolynomialX (Fin n) (Fin n) R).det ⊗ₜ[R] (Matrix.mvPolynomialX (Fin n) (Fin n) R).det

Matrix-multiplication comultiplication sends the generic determinant to its tensor square.

noncomputable def TauCeti.MatrixMonoid.coordinateBialgebra (R : Type u) [CommRing R] (n : ℕ) : CommBialgCat R

The polynomial coordinate algebra of the matrix monoid, bundled with the selected matrix-coordinate bialgebra structure.

The object stores bialgebra R n; it does not depend on whichever bialgebra instance may be available globally for the raw MvPolynomial carrier.

Equations

• TauCeti.MatrixMonoid.coordinateBialgebra R n = ↧(TauCeti.MatrixMonoid.CoordinateRing R n)

noncomputable def TauCeti.MatrixMonoid.coordinateBialgebraAlgEquiv (R : Type u) [CommRing R] (n : ℕ) : CoordinateRing R n ≃ₐ[R] ↑(coordinateBialgebra R n)

The canonical algebra equivalence from the polynomial coordinate ring to the carrier of its bundled matrix-coordinate bialgebra.

Equations

• TauCeti.MatrixMonoid.coordinateBialgebraAlgEquiv R n = AlgEquiv.refl

@[simp]

theorem TauCeti.MatrixMonoid.coordinateBialgebra_comul_apply (R : Type u) [CommRing R] (n : ℕ) (x : CoordinateRing R n) : CoalgebraStruct.comul ((coordinateBialgebraAlgEquiv R n) x) = (Algebra.TensorProduct.map ↑(coordinateBialgebraAlgEquiv R n) ↑(coordinateBialgebraAlgEquiv R n)) ((comul R n) x)

Comultiplication on the bundled coordinate bialgebra agrees with the explicit matrix-multiplication comultiplication after transport through coordinateBialgebraAlgEquiv.

@[simp]

theorem TauCeti.MatrixMonoid.coordinateBialgebra_counit_apply (R : Type u) [CommRing R] (n : ℕ) (x : CoordinateRing R n) : CoalgebraStruct.counit ((coordinateBialgebraAlgEquiv R n) x) = (counit R n) x

The counit on the bundled coordinate bialgebra agrees with the explicit identity-matrix counit after transport through coordinateBialgebraAlgEquiv.

@[simp]

theorem TauCeti.MatrixMonoid.coordinateBialgebra_comul_X (R : Type u) [CommRing R] (n : ℕ) (i j : Fin n) : CoalgebraStruct.comul ((coordinateBialgebraAlgEquiv R n) (MvPolynomial.X (i, j))) = ∑ k : Fin n, (coordinateBialgebraAlgEquiv R n) (MvPolynomial.X (i, k)) ⊗ₜ[R] (coordinateBialgebraAlgEquiv R n) (MvPolynomial.X (k, j))

The bundled coordinate bialgebra retains the matrix-multiplication comultiplication on its generic entries.

@[simp]

theorem TauCeti.MatrixMonoid.coordinateBialgebra_counit_X (R : Type u) [CommRing R] (n : ℕ) (i j : Fin n) : CoalgebraStruct.counit ((coordinateBialgebraAlgEquiv R n) (MvPolynomial.X (i, j))) = if i = j then 1 else 0

The bundled coordinate bialgebra retains the identity-matrix counit on its generic entries.

theorem TauCeti.MatrixMonoid.isGroupLikeElem_determinant (R : Type u) [CommRing R] (n : ℕ) : IsGroupLikeElem R ((coordinateBialgebraAlgEquiv R n) (Matrix.mvPolynomialX (Fin n) (Fin n) R).det)

The determinant of the generic matrix is group-like in the matrix-coordinate bialgebra.