The determinant morphism of the general linear group

For a commutative ring R, this file constructs the determinant coordinate morphism

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

The determinant of the localized generic matrix is group-like in the bundled coordinate Hopf algebra of GLₙ. The free-group property of Multiplicative ℤ therefore sends an integer to the corresponding integral power of this group-like element. Extending that homomorphism to the group algebra and evaluating group-like elements gives the coordinate morphism. Its direction is opposite to the represented group morphism det : GLₙ ⟶ 𝔾ₘ.

On algebra-valued convolution points, precomposition with this coordinate morphism agrees with the ordinary unit-valued determinant of an invertible matrix. This comparison is compatible with both the group-algebra presentation D(Multiplicative ℤ) and Tau Ceti's Laurent-polynomial multiplicative-group points API. The construction includes rank zero and the zero ring.

Main declarations

• TauCeti.GeneralLinear.determinantGroupLike: the localized generic determinant as a group-like element.
• TauCeti.GeneralLinear.determinantCoordinateMap: the coordinate Hopf-algebra morphism from D(Multiplicative ℤ) to GLₙ.
• TauCeti.GeneralLinear.determinantCoordinateMap_single: its value on every group-algebra basis element.
• TauCeti.GeneralLinear.determinantPoints: the induced homomorphism on convolution points.
• TauCeti.GeneralLinear.pointsMulEquiv_determinantPoints: under the standard point equivalences, the induced homomorphism is matrix determinant.

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

The determinant of the localized generic matrix, transported to the bundled coordinate Hopf algebra of GLₙ, as a group-like element.

Equations

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

@[simp]

theorem TauCeti.GeneralLinear.determinantGroupLike_val (R : Type u) [CommRing R] (n : ℕ) : ↑(determinantGroupLike R n) = (coordinateHopfAlgebraAlgEquiv R n) (localizedGenericMatrix R n).det

The value of determinantGroupLike is the transported localized generic determinant.

noncomputable def TauCeti.GeneralLinear.determinantCoordinateMap (R : Type u) [CommRing R] (n : ℕ) : ↧(MonoidAlgebra R (Multiplicative ℤ)) ⟶ coordinateHopfAlgebra R n

The determinant coordinate morphism O(𝔾ₘ) = R[Multiplicative ℤ] ⟶ O(GLₙ), packaged between the underlying commutative Hopf algebras of the existing finite-type coordinate objects. Relative spectrum reverses this arrow to the represented morphism det : GLₙ ⟶ 𝔾ₘ.

Equations

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

theorem TauCeti.GeneralLinear.determinantCoordinateMap_single (R : Type u) [CommRing R] (n : ℕ) (m : ℤ) (r : R) : (CommHopfAlgCat.Hom.hom (determinantCoordinateMap R n)) (MonoidAlgebra.single (Multiplicative.ofAdd m) r) = r • ↑(determinantGroupLike R n ^ m)

The determinant coordinate morphism sends the basis element indexed by m to the scalar multiple of the m-th integral power of the group-like generic determinant.

@[simp]

theorem TauCeti.GeneralLinear.determinantCoordinateMap_ofAdd_one (R : Type u) [CommRing R] (n : ℕ) : (CommHopfAlgCat.Hom.hom (determinantCoordinateMap R n)) (MonoidAlgebra.single (Multiplicative.ofAdd 1) 1) = (coordinateHopfAlgebraAlgEquiv R n) (localizedGenericMatrix R n).det

The standard group-algebra generator maps to the localized generic determinant.

noncomputable def TauCeti.GeneralLinear.determinantPoints (R : Type u) [CommRing R] (n : ℕ) {A : Type w} [CommSemiring A] [Algebra R A] : WithConv (↑(coordinateHopfAlgebra R n) →ₐ[R] A) →* WithConv (MonoidAlgebra R (Multiplicative ℤ) →ₐ[R] A)

Precomposition with the determinant coordinate morphism, as a homomorphism from GLₙ convolution points to points of the group-algebra presentation of 𝔾ₘ.

Equations

• TauCeti.GeneralLinear.determinantPoints R n = TauCeti.AlgHom.mapDomain (CommHopfAlgCat.Hom.hom (TauCeti.GeneralLinear.determinantCoordinateMap R n))

theorem TauCeti.GeneralLinear.determinantPoints_apply_apply (R : Type u) [CommRing R] (n : ℕ) {A : Type w} [CommSemiring A] [Algebra R A] (f : WithConv (↑(coordinateHopfAlgebra R n) →ₐ[R] A)) (x : MonoidAlgebra R (Multiplicative ℤ)) : ((determinantPoints R n) f).ofConv x = f.ofConv ((CommHopfAlgCat.Hom.hom (determinantCoordinateMap R n)) x)

The point induced by the determinant coordinate morphism acts by precomposition.

theorem TauCeti.GeneralLinear.mapValue_determinantPoints (R : Type u) [CommRing R] (n : ℕ) {A : Type w} [CommSemiring A] [Algebra R A] {B : Type u_1} [CommSemiring B] [Algebra R B] (phi : A →ₐ[R] B) : (determinantPoints R n).comp (AlgHom.mapValue phi) = (AlgHom.mapValue phi).comp (determinantPoints R n)

The determinant homomorphism on convolution points is natural in the value algebra.

theorem TauCeti.GeneralLinear.point_apply_determinantGroupLike (R : Type u) [CommRing R] (n : ℕ) {A : Type w} [CommRing A] [Algebra R A] (f : WithConv (↑(coordinateHopfAlgebra R n) →ₐ[R] A)) : f.ofConv ↑(determinantGroupLike R n) = (↑(pointToGeneralLinear n f)).det

Evaluation of the group-like generic determinant at a general-linear point is the determinant of the associated invertible matrix.

theorem TauCeti.GeneralLinear.pointsMulEquiv_determinantPoints (R : Type u) [CommRing R] (n : ℕ) {A : Type w} [CommRing A] [Algebra R A] (f : WithConv (↑(coordinateHopfAlgebra R n) →ₐ[R] A)) : (DiagonalizableGroup.pointsMulEquiv ((determinantPoints R n) f)) (Multiplicative.ofAdd 1) = Matrix.GeneralLinearGroup.det ((pointsMulEquiv n) f)

Under the diagonalizable-group and general-linear point equivalences, precomposition with the determinant coordinate morphism is the ordinary unit-valued matrix determinant.

theorem TauCeti.GeneralLinear.pointsMulEquiv_determinantPoints_symm_apply (R : Type u) [CommRing R] (n : ℕ) {A : Type w} [CommRing A] [Algebra R A] (g : GL (Fin n) A) : (DiagonalizableGroup.pointsMulEquiv ((determinantPoints R n) ((pointsMulEquiv n).symm g))) (Multiplicative.ofAdd 1) = Matrix.GeneralLinearGroup.det g

Starting with an invertible matrix, the point induced by the determinant coordinate morphism corresponds to its ordinary determinant unit.

theorem TauCeti.GeneralLinear.multiplicativeGroup_pointEquiv_determinantPoints (R : Type u) [CommRing R] (n : ℕ) {A : Type w} [CommRing A] [Algebra R A] (f : WithConv (↑(coordinateHopfAlgebra R n) →ₐ[R] A)) : MultiplicativeGroup.pointEquiv (((determinantPoints R n) f).ofConv.comp ↑(AddMonoidAlgebra.toMultiplicativeAlgEquiv R R ℤ)) = Matrix.GeneralLinearGroup.det ((pointsMulEquiv n) f)

The determinant comparison through Tau Ceti's Laurent-polynomial multiplicative-group points equivalence.