The general linear coordinate Hopf algebra

For a commutative ring R, this file constructs the coordinate Hopf algebra of GLₙ as

R[Xᵢⱼ][det(X)⁻¹].

The matrix-monoid comultiplication and counit extend across the localization because the generic determinant is group-like. The antipode evaluates the polynomial generators at the nonsingular inverse of the localized generic matrix. The bialgebra and Hopf laws are proved by localization extensionality and polynomial-generator calculations; in particular, the construction never assumes that the localization map is injective.

The raw structure dictionaries are named values rather than global instances. The bundled coordinateHopfAlgebra is the coherence boundary for the chosen matrix-coordinate structure, and finiteTypeCoordinateHopfAlgebra records that this localization is of finite type. The construction includes rank zero and the zero ring, with no nontriviality or positive-rank hypothesis.

Main declarations

• TauCeti.GeneralLinear.CoordinateRing: the determinant localization.
• TauCeti.GeneralLinear.comul, TauCeti.GeneralLinear.counit: the localized coalgebra maps.
• TauCeti.GeneralLinear.antipode: the inverse-matrix antipode.
• TauCeti.GeneralLinear.hopfAlgebra: the selected Hopf-algebra dictionary.
• TauCeti.GeneralLinear.coordinateHopfAlgebra: the bundled commutative Hopf algebra.
• TauCeti.GeneralLinear.adjoin_coordinateHopfAlgebra_X_union_antipode_X: its generic entries and their antipode images generate its carrier as an algebra.
• TauCeti.GeneralLinear.finiteTypeCoordinateHopfAlgebra: its finite-type package.

References

• J. S. Milne, Basic Theory of Affine Group Schemes, Chapter IV, §1.8.
• The Stacks Project, Tags 022W, 022X, and 00CM.

@[reducible, inline]

abbrev TauCeti.GeneralLinear.CoordinateRing (R : Type u) [CommRing R] (n : ℕ) : Type u

The coordinate ring of GLₙ, obtained by inverting the determinant of Mathlib's generic matrix in the matrix-monoid coordinate ring.

Equations

• TauCeti.GeneralLinear.CoordinateRing R n = Localization.Away (Matrix.mvPolynomialX (Fin n) (Fin n) R).det

noncomputable def TauCeti.GeneralLinear.coordinateRingMap (R : Type u) [CommRing R] (n : ℕ) : MatrixMonoid.CoordinateRing R n →ₐ[R] CoordinateRing R n

The canonical algebra map from the matrix-monoid coordinate ring into its determinant localization.

Equations

• TauCeti.GeneralLinear.coordinateRingMap R n = IsScalarTower.toAlgHom R (TauCeti.MatrixMonoid.CoordinateRing R n) (TauCeti.GeneralLinear.CoordinateRing R n)

theorem TauCeti.GeneralLinear.coordinateRingMap_apply (R : Type u) [CommRing R] (n : ℕ) (x : MatrixMonoid.CoordinateRing R n) : (coordinateRingMap R n) x = (algebraMap (MatrixMonoid.CoordinateRing R n) (CoordinateRing R n)) x

The canonical map into the determinant localization agrees with its algebra map.

noncomputable def TauCeti.GeneralLinear.localizedGenericMatrix (R : Type u) [CommRing R] (n : ℕ) : Matrix (Fin n) (Fin n) (CoordinateRing R n)

Mathlib's generic matrix after applying the canonical map into the determinant localization.

Equations

• TauCeti.GeneralLinear.localizedGenericMatrix R n = (Matrix.mvPolynomialX (Fin n) (Fin n) R).map ⇑(TauCeti.GeneralLinear.coordinateRingMap R n)

@[simp]

theorem TauCeti.GeneralLinear.localizedGenericMatrix_apply (R : Type u) [CommRing R] (n : ℕ) (i j : Fin n) : localizedGenericMatrix R n i j = (coordinateRingMap R n) (MvPolynomial.X (i, j))

An entry of the localized generic matrix is the image of the corresponding polynomial generator.

@[simp]

theorem TauCeti.GeneralLinear.det_localizedGenericMatrix (R : Type u) [CommRing R] (n : ℕ) : (localizedGenericMatrix R n).det = (coordinateRingMap R n) (Matrix.mvPolynomialX (Fin n) (Fin n) R).det

The determinant of the localized generic matrix is the image of the generic determinant.

theorem TauCeti.GeneralLinear.isUnit_det_localizedGenericMatrix (R : Type u) [CommRing R] (n : ℕ) : IsUnit (localizedGenericMatrix R n).det

The determinant of the localized generic matrix is a unit.

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

The matrix-multiplication comultiplication extended across the determinant localization.

Equations

• TauCeti.GeneralLinear.comul R n = IsLocalization.Away.liftAlgHom (Matrix.mvPolynomialX (Fin n) (Fin n) R).det ⋯

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

The identity-matrix counit extended across the determinant localization.

Equations

• TauCeti.GeneralLinear.counit R n = IsLocalization.Away.liftAlgHom (Matrix.mvPolynomialX (Fin n) (Fin n) R).det ⋯

@[simp]

theorem TauCeti.GeneralLinear.comul_coordinateRingMap (R : Type u) [CommRing R] (n : ℕ) (x : MatrixMonoid.CoordinateRing R n) : (comul R n) ((coordinateRingMap R n) x) = (Algebra.TensorProduct.map (coordinateRingMap R n) (coordinateRingMap R n)) ((MatrixMonoid.comul R n) x)

The localized comultiplication restricts to the matrix-monoid comultiplication followed by the two canonical localization maps.

@[simp]

theorem TauCeti.GeneralLinear.counit_coordinateRingMap (R : Type u) [CommRing R] (n : ℕ) (x : MatrixMonoid.CoordinateRing R n) : (counit R n) ((coordinateRingMap R n) x) = (MatrixMonoid.counit R n) x

The localized counit restricts to the matrix-monoid counit.

noncomputable def TauCeti.GeneralLinear.antipode (R : Type u) [CommRing R] (n : ℕ) : CoordinateRing R n →ₐ[R] CoordinateRing R n

The antipode of the general linear coordinate ring. It evaluates the polynomial generators at the nonsingular inverse of the localized generic matrix and extends across the localization.

Equations

• TauCeti.GeneralLinear.antipode R n = IsLocalization.Away.liftAlgHom (Matrix.mvPolynomialX (Fin n) (Fin n) R).det ⋯

@[simp]

theorem TauCeti.GeneralLinear.antipode_coordinateRingMap (R : Type u) [CommRing R] (n : ℕ) (x : MatrixMonoid.CoordinateRing R n) : (antipode R n) ((coordinateRingMap R n) x) = (MvPolynomial.aeval fun (ij : Fin n × Fin n) => (localizedGenericMatrix R n)⁻¹ ij.1 ij.2) x

On the polynomial subalgebra, the antipode is evaluation at the nonsingular inverse of the localized generic matrix.

theorem TauCeti.GeneralLinear.algHom_ext_away (R : Type u) [CommRing R] (n : ℕ) {T : Type u_1} [Semiring T] [Algebra R T] {f g : CoordinateRing R n →ₐ[R] T} (h : f.comp (coordinateRingMap R n) = g.comp (coordinateRingMap R n)) : f = g

Two algebra homomorphisms out of the determinant localization are equal if they agree on the matrix-monoid coordinate ring.

@[simp]

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

Comultiplication sends a localized generic entry to the matrix-multiplication sum.

@[simp]

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

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

@[simp]

theorem TauCeti.GeneralLinear.antipode_X (R : Type u) [CommRing R] (n : ℕ) (i j : Fin n) : (antipode R n) ((coordinateRingMap R n) (MvPolynomial.X (i, j))) = (localizedGenericMatrix R n)⁻¹ i j

The antipode sends a localized generic entry to the corresponding entry of the nonsingular inverse.

@[simp]

theorem TauCeti.GeneralLinear.map_comul_localizedGenericMatrix (R : Type u) [CommRing R] (n : ℕ) : (localizedGenericMatrix R n).map ⇑(comul R n) = (localizedGenericMatrix R n).map ⇑Algebra.TensorProduct.includeLeft * (localizedGenericMatrix R n).map ⇑Algebra.TensorProduct.includeRight

Applying comultiplication entrywise to the localized generic matrix gives the product of its left- and right-tensor copies, in the order representing ordinary matrix multiplication.

@[simp]

theorem TauCeti.GeneralLinear.map_counit_localizedGenericMatrix (R : Type u) [CommRing R] (n : ℕ) : (localizedGenericMatrix R n).map ⇑(counit R n) = 1

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

@[simp]

theorem TauCeti.GeneralLinear.map_antipode_localizedGenericMatrix (R : Type u) [CommRing R] (n : ℕ) : (localizedGenericMatrix R n).map ⇑(antipode R n) = (localizedGenericMatrix R n)⁻¹

Applying the antipode entrywise to the localized generic matrix gives its nonsingular inverse.

theorem TauCeti.GeneralLinear.comul_det_localizedGenericMatrix (R : Type u) [CommRing R] (n : ℕ) : (comul R n) (localizedGenericMatrix R n).det = (localizedGenericMatrix R n).det ⊗ₜ[R] (localizedGenericMatrix R n).det

The determinant of the localized generic matrix remains group-like for the localized comultiplication.

theorem TauCeti.GeneralLinear.counit_det_localizedGenericMatrix (R : Type u) [CommRing R] (n : ℕ) : (counit R n) (localizedGenericMatrix R n).det = 1

The counit sends the determinant of the localized generic matrix to one.

theorem TauCeti.GeneralLinear.antipode_det_localizedGenericMatrix (R : Type u) [CommRing R] (n : ℕ) : (antipode R n) (localizedGenericMatrix R n).det = Ring.inverse (localizedGenericMatrix R n).det

The antipode sends the localized generic determinant to its ring inverse.

@[instance_reducible]

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

The bialgebra structure on the determinant localization, with matrix-multiplication comultiplication and identity-matrix counit.

This is intentionally a named value rather than a global instance.

Equations

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

@[instance_reducible]

noncomputable def TauCeti.GeneralLinear.hopfAlgebra (R : Type u) [CommRing R] (n : ℕ) : HopfAlgebra R (CoordinateRing R n)

The Hopf-algebra structure on the determinant localization whose antipode is inverse-matrix evaluation.

This is intentionally a named value rather than a global instance. Use coordinateHopfAlgebra as the bundled coherence boundary.

Equations

• TauCeti.GeneralLinear.hopfAlgebra R n = HopfAlgebra.ofAlgHom (TauCeti.GeneralLinear.antipode R n) ⋯ ⋯

theorem TauCeti.GeneralLinear.hopfAlgebra_comul (R : Type u) [CommRing R] (n : ℕ) : CoalgebraStruct.comul ≍ (comul R n).toLinearMap

Selecting hopfAlgebra R n makes its comultiplication the explicit localized map comul R n. The equality is heterogeneous because opacity hides the stored module structure.

theorem TauCeti.GeneralLinear.hopfAlgebra_counit (R : Type u) [CommRing R] (n : ℕ) : CoalgebraStruct.counit ≍ (counit R n).toLinearMap

Selecting hopfAlgebra R n makes its counit the explicit localized map counit R n. The equality is heterogeneous because opacity hides the stored module structure.

theorem TauCeti.GeneralLinear.hopfAlgebra_antipode (R : Type u) [CommRing R] (n : ℕ) : HopfAlgebraStruct.antipode R ≍ (antipode R n).toLinearMap

Selecting hopfAlgebra R n makes its antipode the explicit inverse-matrix map antipode R n. The equality is heterogeneous because opacity hides the stored module structure.

noncomputable def TauCeti.GeneralLinear.coordinateHopfAlgebra (R : Type u) [CommRing R] (n : ℕ) : CommHopfAlgCat R

The determinant localization bundled with the selected general linear Hopf-algebra structure.

Equations

• TauCeti.GeneralLinear.coordinateHopfAlgebra R n = ↧(TauCeti.GeneralLinear.CoordinateRing R n)

noncomputable def TauCeti.GeneralLinear.coordinateHopfAlgebraAlgEquiv (R : Type u) [CommRing R] (n : ℕ) : CoordinateRing R n ≃ₐ[R] ↑(coordinateHopfAlgebra R n)

The canonical algebra equivalence from the determinant localization to the carrier of its bundled coordinate Hopf algebra.

Equations

• TauCeti.GeneralLinear.coordinateHopfAlgebraAlgEquiv R n = AlgEquiv.refl

noncomputable def TauCeti.GeneralLinear.genericMatrix (R : Type u) [CommRing R] (n : ℕ) : Matrix (Fin n) (Fin n) ↑(coordinateHopfAlgebra R n)

The localized generic matrix, read in the bundled coordinate Hopf algebra of GLₙ.

Equations

• TauCeti.GeneralLinear.genericMatrix R n = (TauCeti.GeneralLinear.localizedGenericMatrix R n).map ⇑(TauCeti.GeneralLinear.coordinateHopfAlgebraAlgEquiv R n)

@[simp]

theorem TauCeti.GeneralLinear.genericMatrix_apply (R : Type u) [CommRing R] (n : ℕ) (i j : Fin n) : genericMatrix R n i j = (coordinateHopfAlgebraAlgEquiv R n) ((coordinateRingMap R n) (MvPolynomial.X (i, j)))

An entry of the bundled generic matrix is the corresponding bundled coordinate.

theorem TauCeti.GeneralLinear.isUnit_det_genericMatrix (R : Type u) [CommRing R] (n : ℕ) : IsUnit (genericMatrix R n).det

The determinant of the bundled generic matrix is a unit.

theorem TauCeti.GeneralLinear.genericMatrix_inv_apply (R : Type u) [CommRing R] (n : ℕ) (i j : Fin n) : (genericMatrix R n)⁻¹ i j = (coordinateHopfAlgebraAlgEquiv R n) ((localizedGenericMatrix R n)⁻¹ i j)

An entry of the inverse bundled generic matrix is the bundled image of the corresponding localized inverse entry.

theorem TauCeti.GeneralLinear.map_inv_genericMatrix (R : Type u) [CommRing R] (n : ℕ) {T : Type u_1} [CommRing T] [Algebra R T] (φ : ↑(coordinateHopfAlgebra R n) →ₐ[R] T) : (genericMatrix R n)⁻¹.map ⇑φ = ((genericMatrix R n).map ⇑φ)⁻¹

Algebra morphisms out of O(GLₙ) commute with inverting the generic matrix.

@[simp]

theorem TauCeti.GeneralLinear.coordinateHopfAlgebra_comul_apply (R : Type u) [CommRing R] (n : ℕ) (x : CoordinateRing R n) : CoalgebraStruct.comul ((coordinateHopfAlgebraAlgEquiv R n) x) = (Algebra.TensorProduct.map ↑(coordinateHopfAlgebraAlgEquiv R n) ↑(coordinateHopfAlgebraAlgEquiv R n)) ((comul R n) x)

Comultiplication on the bundled coordinate Hopf algebra agrees with the explicit localized comultiplication after transport through coordinateHopfAlgebraAlgEquiv.

@[simp]

theorem TauCeti.GeneralLinear.coordinateHopfAlgebra_counit_apply (R : Type u) [CommRing R] (n : ℕ) (x : CoordinateRing R n) : CoalgebraStruct.counit ((coordinateHopfAlgebraAlgEquiv R n) x) = (counit R n) x

The counit on the bundled coordinate Hopf algebra agrees with the explicit localized counit after transport through coordinateHopfAlgebraAlgEquiv.

@[simp]

theorem TauCeti.GeneralLinear.coordinateHopfAlgebra_antipode_apply (R : Type u) [CommRing R] (n : ℕ) (x : CoordinateRing R n) : (HopfAlgebraStruct.antipode R) ((coordinateHopfAlgebraAlgEquiv R n) x) = (coordinateHopfAlgebraAlgEquiv R n) ((antipode R n) x)

The antipode on the bundled coordinate Hopf algebra agrees with inverse-matrix evaluation after transport through coordinateHopfAlgebraAlgEquiv.

@[simp]

theorem TauCeti.GeneralLinear.coordinateHopfAlgebra_comul_X (R : Type u) [CommRing R] (n : ℕ) (i j : Fin n) : CoalgebraStruct.comul ((coordinateHopfAlgebraAlgEquiv R n) ((coordinateRingMap R n) (MvPolynomial.X (i, j)))) = ∑ k : Fin n, (coordinateHopfAlgebraAlgEquiv R n) ((coordinateRingMap R n) (MvPolynomial.X (i, k))) ⊗ₜ[R] (coordinateHopfAlgebraAlgEquiv R n) ((coordinateRingMap R n) (MvPolynomial.X (k, j)))

The bundled coordinate Hopf algebra retains the matrix-multiplication comultiplication on localized generic entries.

@[simp]

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

The bundled coordinate Hopf algebra retains the identity-matrix counit on localized generic entries.

@[simp]

theorem TauCeti.GeneralLinear.coordinateHopfAlgebra_antipode_X (R : Type u) [CommRing R] (n : ℕ) (i j : Fin n) : (HopfAlgebraStruct.antipode R) ((coordinateHopfAlgebraAlgEquiv R n) ((coordinateRingMap R n) (MvPolynomial.X (i, j)))) = (coordinateHopfAlgebraAlgEquiv R n) ((localizedGenericMatrix R n)⁻¹ i j)

The bundled coordinate Hopf algebra sends a localized generic entry under the antipode to the corresponding inverse-matrix entry.

@[simp]

theorem TauCeti.GeneralLinear.map_counit_genericMatrix (R : Type u) [CommRing R] (n : ℕ) : (genericMatrix R n).map ⇑(Bialgebra.counitAlgHom R ↑(coordinateHopfAlgebra R n)) = 1

The counit sends the bundled generic matrix to the identity matrix.

@[simp]

theorem TauCeti.GeneralLinear.map_comul_genericMatrix (R : Type u) [CommRing R] (n : ℕ) : (genericMatrix R n).map ⇑(Bialgebra.comulAlgHom R ↑(coordinateHopfAlgebra R n)) = (genericMatrix R n).map ⇑Algebra.TensorProduct.includeLeft * (genericMatrix R n).map ⇑Algebra.TensorProduct.includeRight

The comultiplication sends the bundled generic matrix to the product of its two tensor inclusions: Δ X = (X ⊗ 1)(1 ⊗ X).

@[simp]

theorem TauCeti.GeneralLinear.map_antipode_genericMatrix (R : Type u) [CommRing R] (n : ℕ) : (genericMatrix R n).map ⇑(HopfAlgebra.antipodeAlgHom R ↑(coordinateHopfAlgebra R n)) = (genericMatrix R n)⁻¹

The antipode sends the bundled generic matrix to its bundled inverse.

theorem TauCeti.GeneralLinear.coordinateHopfAlgebra_algHom_ext (R : Type u) [CommRing R] (n : ℕ) {T : Type u_1} [Semiring T] [Algebra R T] {f g : ↑(coordinateHopfAlgebra R n) →ₐ[R] T} (h : ∀ (i j : Fin n), f ((coordinateHopfAlgebraAlgEquiv R n) ((coordinateRingMap R n) (MvPolynomial.X (i, j)))) = g ((coordinateHopfAlgebraAlgEquiv R n) ((coordinateRingMap R n) (MvPolynomial.X (i, j))))) : f = g

Two algebra homomorphisms out of the bundled coordinate Hopf algebra of GLₙ are equal if they agree on the localized generic entries. This is the bundled counterpart of algHom_ext_away.

theorem TauCeti.GeneralLinear.coordinateHopfAlgebra_bialgHom_ext (R : Type u) [CommRing R] (n : ℕ) {T : Type u_1} [Semiring T] [Bialgebra R T] {f g : ↑(coordinateHopfAlgebra R n) →ₐc[R] T} (h : ∀ (i j : Fin n), f ((coordinateHopfAlgebraAlgEquiv R n) ((coordinateRingMap R n) (MvPolynomial.X (i, j)))) = g ((coordinateHopfAlgebraAlgEquiv R n) ((coordinateRingMap R n) (MvPolynomial.X (i, j))))) : f = g

Two bialgebra homomorphisms out of the bundled coordinate Hopf algebra of GLₙ are equal if they agree on the localized generic entries.

theorem TauCeti.GeneralLinear.adjoin_coordinateHopfAlgebra_X_union_antipode_X (R : Type u) [CommRing R] (n : ℕ) : Algebra.adjoin R ((Set.range fun (ij : Fin n × Fin n) => (coordinateHopfAlgebraAlgEquiv R n) ((coordinateRingMap R n) (MvPolynomial.X ij))) ∪ Set.range fun (ij : Fin n × Fin n) => (HopfAlgebraStruct.antipode R) ((coordinateHopfAlgebraAlgEquiv R n) ((coordinateRingMap R n) (MvPolynomial.X ij)))) = ⊤

The localized generic entries and their images under the stored antipode generate the carrier of the bundled general linear coordinate Hopf algebra.

noncomputable def TauCeti.GeneralLinear.finiteTypeCoordinateHopfAlgebra (R : Type u) [CommRing R] (n : ℕ) : FiniteTypeCommHopfAlgCat R

The general linear coordinate Hopf algebra bundled with its finite-type algebra property.

Equations

• TauCeti.GeneralLinear.finiteTypeCoordinateHopfAlgebra R n = { obj := TauCeti.GeneralLinear.coordinateHopfAlgebra R n, property := ⋯ }

@[simp]

theorem TauCeti.GeneralLinear.finiteTypeCoordinateHopfAlgebra_obj (R : Type u) [CommRing R] (n : ℕ) : (finiteTypeCoordinateHopfAlgebra R n).obj = coordinateHopfAlgebra R n

The underlying commutative Hopf algebra of finiteTypeCoordinateHopfAlgebra is coordinateHopfAlgebra.

instance TauCeti.GeneralLinear.instAlgebraFiniteTypeCoordinateHopfAlgebra (R : Type u) [CommRing R] (n : ℕ) : Algebra.FiniteType R ↑(coordinateHopfAlgebra R n)

The coordinate Hopf algebra of GL_n carries the finite-type instance recorded by its bundled finite-type coordinate algebra.