The projective general linear group scheme as automorphisms of a matrix algebra

For a commutative ring R and a natural number n, this file constructs the affine group scheme PGLₙ over R as the automorphism group scheme of the matrix algebra Mₙ: the closed subgroup scheme of GL_{n²} of invertible linear maps of Mₙ that are multiplicative. Over every commutative R-algebra A its points are exactly the A-algebra automorphisms of Mₙ(A).

Concretely, Mₙ(R) is free on the matrix units, numbered by Fin (n * n) through finProdFinEquiv. The structure matrices of Mₙ(R) in this basis are the left multiplication matrices of the matrix units, and TauCeti.ConstantMultiplication provides the Hopf ideal of O(GL_{n²}) cutting out the matrices preserving that multiplication. A bijective multiplicative linear map of a unital algebra automatically preserves the identity, so these matrices are exactly the matrices of algebra automorphisms.

This is the representing object for the projective general linear group: the conjugation homomorphism GLₙ → PGLₙ, its kernel and its surjectivity on field-valued points are in TauCeti.Algebra.AlgebraicGroup.ProjectiveGeneralLinear.Conjugation. The pointwise quotient A ↦ GLₙ(A) / Z(GLₙ(A)) of TauCeti.GeneralLinear.pglPointsFunctor maps injectively into the points of PGLₙ by conjugation (Matrix.ProjGenLinGroup.innerAut_injective), and bijectively over a field.

Main declarations

• TauCeti.ProjectiveGeneralLinear.matrixUnitBasis: the basis of matrix units of Mₙ(S), indexed by Fin (n * n).
• TauCeti.ProjectiveGeneralLinear.structureMatrix: the structure matrices of Mₙ(R) in that basis.
• TauCeti.ProjectiveGeneralLinear.definingHopfIdeal, TauCeti.ProjectiveGeneralLinear.coordinateHopfAlgebra and TauCeti.ProjectiveGeneralLinear.groupScheme: the closed subgroup scheme PGLₙ of GL_{n²}.
• TauCeti.ProjectiveGeneralLinear.autToGeneralLinear: the matrix of an algebra automorphism of Mₙ(A) in the matrix-unit basis.
• TauCeti.ProjectiveGeneralLinear.hopfIdealPointsSubgroup_definingHopfIdeal: the matrix points of PGLₙ are exactly the matrices of algebra automorphisms.
• TauCeti.ProjectiveGeneralLinear.pointsMulEquiv: the points of PGLₙ with values in A are the group of A-algebra automorphisms of Mₙ(A).

References

• J. S. Milne, Algebraic Groups (2017), where PGLₙ is identified with the automorphism group functor of the matrix algebra Mₙ.
• W. C. Waterhouse, Introduction to Affine Group Schemes (1979), Chapter 1, for closed subgroups of GLₙ cut out by polynomial identities.

noncomputable def TauCeti.ProjectiveGeneralLinear.matrixUnitBasis (n : ℕ) (S : Type v) [CommRing S] : Module.Basis (Fin (n * n)) S (Matrix (Fin n) (Fin n) S)

The basis of Matrix (Fin n) (Fin n) S by matrix units, indexed by Fin (n * n) through finProdFinEquiv: the kth basis vector is Matrix.single i j 1 for (i, j) = finProdFinEquiv.symm k.

Equations

• TauCeti.ProjectiveGeneralLinear.matrixUnitBasis n S = (Matrix.stdBasis S (Fin n) (Fin n)).reindex finProdFinEquiv

@[simp]

theorem TauCeti.ProjectiveGeneralLinear.matrixUnitBasis_apply (n : ℕ) (S : Type v) [CommRing S] (k : Fin (n * n)) : (matrixUnitBasis n S) k = Matrix.single (finProdFinEquiv.symm k).1 (finProdFinEquiv.symm k).2 1

The kth matrix unit.

@[simp]

theorem TauCeti.ProjectiveGeneralLinear.matrixUnitBasis_repr_apply (n : ℕ) (S : Type v) [CommRing S] (x : Matrix (Fin n) (Fin n) S) (k : Fin (n * n)) : ((matrixUnitBasis n S).repr x) k = x (finProdFinEquiv.symm k).1 (finProdFinEquiv.symm k).2

The kth coordinate of a matrix in the matrix-unit basis is its entry at finProdFinEquiv.symm k.

noncomputable def TauCeti.ProjectiveGeneralLinear.structureMatrix (n : ℕ) (R : Type u) [CommRing R] (k : Fin (n * n)) : Matrix (Fin (n * n)) (Fin (n * n)) R

The structure matrices of the matrix algebra Mₙ(R): the kth one is the matrix, in the matrix-unit basis, of left multiplication by the kth matrix unit.

Equations

• TauCeti.ProjectiveGeneralLinear.structureMatrix n R k = (Algebra.leftMulMatrix (TauCeti.ProjectiveGeneralLinear.matrixUnitBasis n R)) ((TauCeti.ProjectiveGeneralLinear.matrixUnitBasis n R) k)

theorem TauCeti.ProjectiveGeneralLinear.toMatrix_mulLeft_matrixUnitBasis (n : ℕ) (S : Type v) [CommRing S] (R : Type u) [CommRing R] [Algebra R S] (k : Fin (n * n)) : (LinearMap.toMatrix (matrixUnitBasis n S) (matrixUnitBasis n S)) (LinearMap.mulLeft S ((matrixUnitBasis n S) k)) = (structureMatrix n R k).map ⇑(algebraMap R S)

The structure matrices are defined over the base: read in any commutative R-algebra S, they are the structure matrices of Mₙ(S).

@[reducible, inline]

noncomputable abbrev TauCeti.ProjectiveGeneralLinear.definingHopfIdeal (n : ℕ) (R : Type u) [CommRing R] : HopfIdeal R ↑(GeneralLinear.coordinateHopfAlgebra R (n * n))

The Hopf ideal of O(GL_{n²}) cutting out the invertible linear maps of Mₙ that are multiplicative.

Equations

• TauCeti.ProjectiveGeneralLinear.definingHopfIdeal n R = TauCeti.ConstantMultiplication.definingHopfIdeal R (n * n) (TauCeti.ProjectiveGeneralLinear.structureMatrix n R)

@[reducible, inline]

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

The coordinate Hopf algebra of PGLₙ, the automorphism group scheme of Mₙ.

Equations

• TauCeti.ProjectiveGeneralLinear.coordinateHopfAlgebra n R = TauCeti.ConstantMultiplication.coordinateHopfAlgebra R (n * n) (TauCeti.ProjectiveGeneralLinear.structureMatrix n R)

@[reducible, inline]

noncomputable abbrev TauCeti.ProjectiveGeneralLinear.groupScheme (n : ℕ) (R : Type u) [CommRing R] : CategoryTheory.Grp (CategoryTheory.Over (AlgebraicGeometry.Spec ↧R))

The projective general linear group scheme PGLₙ over R, as the automorphism group scheme of the matrix algebra Mₙ, a closed subgroup scheme of GL_{n²}.

Equations

• TauCeti.ProjectiveGeneralLinear.groupScheme n R = TauCeti.ConstantMultiplication.groupScheme R (n * n) (TauCeti.ProjectiveGeneralLinear.structureMatrix n R)

noncomputable def TauCeti.ProjectiveGeneralLinear.autToGeneralLinear (n : ℕ) (A : Type w) [CommRing A] : (Matrix (Fin n) (Fin n) A ≃ₐ[A] Matrix (Fin n) (Fin n) A) →* GL (Fin (n * n)) A

The matrix, in the matrix-unit basis, of an A-algebra automorphism of Mₙ(A), as a homomorphism into GL_{n²}(A).

Equations

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

@[simp]

theorem TauCeti.ProjectiveGeneralLinear.coe_autToGeneralLinear (n : ℕ) {A : Type w} [CommRing A] (e : Matrix (Fin n) (Fin n) A ≃ₐ[A] Matrix (Fin n) (Fin n) A) : ↑((autToGeneralLinear n A) e) = (LinearMap.toMatrix (matrixUnitBasis n A) (matrixUnitBasis n A)) e.toLinearMap

The underlying matrix of autToGeneralLinear n A e is the matrix of e in the matrix-unit basis.

theorem TauCeti.ProjectiveGeneralLinear.autToGeneralLinear_injective (n : ℕ) {A : Type w} [CommRing A] : Function.Injective ⇑(autToGeneralLinear n A)

An algebra automorphism of Mₙ(A) is determined by its matrix.

theorem TauCeti.ProjectiveGeneralLinear.preserves_toMatrix_iff (n : ℕ) (R : Type u) [CommRing R] {A : Type w} [CommRing A] [Algebra R A] (f : Matrix (Fin n) (Fin n) A →ₗ[A] Matrix (Fin n) (Fin n) A) : ConstantMultiplication.Preserves R (n * n) (structureMatrix n R) ((LinearMap.toMatrix (matrixUnitBasis n A) (matrixUnitBasis n A)) f) ↔ ∀ (x y : Matrix (Fin n) (Fin n) A), f (x * y) = f x * f y

The matrix in the matrix-unit basis of a linear endomorphism of Mₙ(A) preserves the multiplication exactly when the endomorphism is multiplicative.

theorem TauCeti.ProjectiveGeneralLinear.preserves_iff_mem_range_autToGeneralLinear (n : ℕ) (R : Type u) [CommRing R] {A : Type w} [CommRing A] [Algebra R A] (g : GL (Fin (n * n)) A) : ConstantMultiplication.Preserves R (n * n) (structureMatrix n R) ↑g ↔ g ∈ (autToGeneralLinear n A).range

An invertible matrix preserves the multiplication of Mₙ(A) exactly when it is the matrix of an algebra automorphism. Multiplicativity and bijectivity force the identity to be preserved.

theorem TauCeti.ProjectiveGeneralLinear.hopfIdealPointsSubgroup_definingHopfIdeal (n : ℕ) (R : Type u) [CommRing R] (A : Type w) [CommRing A] [Algebra R A] : GeneralLinear.hopfIdealPointsSubgroup (n * n) (definingHopfIdeal n R) A = (autToGeneralLinear n A).range

The matrix points of PGLₙ are the matrices of algebra automorphisms: the subgroup of GL_{n²}(A) cut out by the defining Hopf ideal is the image of the automorphism group of Mₙ(A).

noncomputable def TauCeti.ProjectiveGeneralLinear.pointsMulEquiv (n : ℕ) (R : Type u) [CommRing R] (A : CommAlgCat R) : ↑(HopfAlgebra.points A) ≃* Matrix (Fin n) (Fin n) ↑A ≃ₐ[↑A] Matrix (Fin n) (Fin n) ↑A

The points of PGLₙ are the automorphisms of the matrix algebra: for every commutative R-algebra A, the group of A-points of PGLₙ is the group of A-algebra automorphisms of Mₙ(A).

Equations

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

@[simp]

theorem TauCeti.ProjectiveGeneralLinear.autToGeneralLinear_pointsMulEquiv (n : ℕ) {R : Type u} [CommRing R] (A : CommAlgCat R) (q : ↑(HopfAlgebra.points A)) : (autToGeneralLinear n ↑A) ((pointsMulEquiv n R A) q) = (GeneralLinear.pointsMulEquiv (n * n)) ((CategoryTheory.ConcreteCategory.hom (CommHopfAlgCat.quotientPointsHom (GeneralLinear.coordinateHopfAlgebra R (n * n)) (definingHopfIdeal n R) A)) q)

The automorphism attached to a point of PGLₙ has, as its matrix, the invertible matrix of the underlying point of GL_{n²}. Together with autToGeneralLinear_injective this determines pointsMulEquiv.