The conjugation homomorphism from GLₙ to PGLₙ

An invertible matrix g acts on the matrix algebra Mₙ by the inner automorphism x ↦ g x g⁻¹. This file constructs the corresponding homomorphism of affine group schemes GLₙ → PGLₙ over a commutative ring R, where PGLₙ is the automorphism group scheme of Mₙ from TauCeti.Algebra.AlgebraicGroup.ProjectiveGeneralLinear.Basic, and identifies:

• its effect on points: over every commutative R-algebra A, a point g of GLₙ goes to the inner automorphism of Mₙ(A) defined by g;
• its kernel: a point lies in the scheme-theoretic kernel exactly when its matrix is central, and over a field the kernel Hopf ideal is the defining ideal of the center Z(GLₙ) (which is 𝔾ₘ when n > 0, and trivial when n = 0);
• its image on field-valued points: by the Skolem–Noether theorem every automorphism of Mₙ(K) over a field K is inner, so the map on K-points is surjective. Together with the kernel computation, the K-points of PGLₙ are Mathlib's PGL(n, K) = GLₙ(K) / Z(GLₙ(K)) (Matrix.ProjGenLinGroup.innerAut_bijective).

The pointwise facts about conjugation (Matrix.GeneralLinearGroup.innerAut, its kernel and its surjectivity over a field) are in TauCeti.LinearAlgebra.Matrix.GeneralLinearGroup.InnerAut. In coordinates, the inner automorphism by g has, in the matrix-unit basis, the matrix whose entry at ((p, q), (i, j)) is gₚᵢ (g⁻¹)ⱼq. Over the coordinate algebra of GLₙ, this conjugationMatrix of the generic matrix is multiplicative, so it defines a coordinate morphism O(GL_{n²}) → O(GLₙ) which kills the defining ideal of PGLₙ.

Main declarations

• TauCeti.ProjectiveGeneralLinear.conjugationMatrix: the matrix of x ↦ X x Y in the matrix-unit basis.
• TauCeti.ProjectiveGeneralLinear.conjugationMap: the coordinate morphism of GLₙ → PGLₙ.
• TauCeti.ProjectiveGeneralLinear.map_genericMatrix_conjugationMap: in coordinates, it sends the generic matrix of GL_{n²} to the conjugation matrix of the generic matrix of GLₙ.
• TauCeti.ProjectiveGeneralLinear.pointsMulEquiv_conjugationMap: on points, it is Matrix.GeneralLinearGroup.innerAut.
• TauCeti.ProjectiveGeneralLinear.mem_quotientPointsSubgroup_kernelHopfIdeal_conjugationMap_iff and TauCeti.ProjectiveGeneralLinear.kernelHopfIdeal_conjugationMap: its kernel is the center.
• TauCeti.ProjectiveGeneralLinear.mapPointsFunctor_conjugationMap_app_surjective: it is surjective on points with values in a field.

References

• J. S. Milne, Algebraic Groups (2017), where, for n > 0, PGLₙ is the quotient of GLₙ by its center 𝔾ₘ and is identified with the automorphism group functor of Mₙ.

def TauCeti.ProjectiveGeneralLinear.conjugationMatrix {n : ℕ} {S : Type v} [CommRing S] (X Y : Matrix (Fin n) (Fin n) S) : Matrix (Fin (n * n)) (Fin (n * n)) S

The matrix, in the matrix-unit basis of Mₙ(S), of the linear map x ↦ X x Y: the Kronecker product X ⊗ Yᵀ, reindexed along finProdFinEquiv. Its entry at ((p, q), (i, j)) is Xₚᵢ Yⱼq.

Equations

• TauCeti.ProjectiveGeneralLinear.conjugationMatrix X Y = (Matrix.reindex finProdFinEquiv finProdFinEquiv) (X.kronecker Y.transpose)

@[simp]

theorem TauCeti.ProjectiveGeneralLinear.conjugationMatrix_apply {n : ℕ} {S : Type v} [CommRing S] (X Y : Matrix (Fin n) (Fin n) S) (a c : Fin (n * n)) : conjugationMatrix X Y a c = X (finProdFinEquiv.symm a).1 (finProdFinEquiv.symm c).1 * Y (finProdFinEquiv.symm c).2 (finProdFinEquiv.symm a).2

The entry of the conjugation matrix at (a, c) is Xₚᵢ Yⱼq for (p, q) and (i, j) the pairs numbered by a and c.

theorem TauCeti.ProjectiveGeneralLinear.conjugationMatrix_map {n : ℕ} {S : Type v} [CommRing S] {T : Type w} [CommRing T] {F : Type u_1} [FunLike F S T] [RingHomClass F S T] (f : F) (X Y : Matrix (Fin n) (Fin n) S) : (conjugationMatrix X Y).map ⇑f = conjugationMatrix (X.map ⇑f) (Y.map ⇑f)

Entrywise ring homomorphisms commute with forming the conjugation matrix.

theorem TauCeti.ProjectiveGeneralLinear.toMatrix_mulLeft_comp_mulRight {n : ℕ} {S : Type v} [CommRing S] (X Y : Matrix (Fin n) (Fin n) S) : (LinearMap.toMatrix (matrixUnitBasis n S) (matrixUnitBasis n S)) (LinearMap.mulLeft S X ∘ₗ LinearMap.mulRight S Y) = conjugationMatrix X Y

conjugationMatrix X Y is the matrix of x ↦ X x Y in the matrix-unit basis.

@[simp]

theorem TauCeti.ProjectiveGeneralLinear.conjugationMatrix_one {n : ℕ} {S : Type v} [CommRing S] : conjugationMatrix 1 1 = 1

The conjugation matrix of the identity is the identity.

theorem TauCeti.ProjectiveGeneralLinear.conjugationMatrix_mul {n : ℕ} {S : Type v} [CommRing S] (X₁ X₂ Y₁ Y₂ : Matrix (Fin n) (Fin n) S) : conjugationMatrix (X₁ * X₂) (Y₂ * Y₁) = conjugationMatrix X₁ Y₁ * conjugationMatrix X₂ Y₂

Composing x ↦ X₂ x Y₂ with x ↦ X₁ x Y₁ gives x ↦ (X₁ X₂) x (Y₂ Y₁).

theorem TauCeti.ProjectiveGeneralLinear.preserves_conjugationMatrix {n : ℕ} {S : Type v} [CommRing S] (R : Type u) [CommRing R] [Algebra R S] {X Y : Matrix (Fin n) (Fin n) S} (h : Y * X = 1) : ConstantMultiplication.Preserves R (n * n) (structureMatrix n R) (conjugationMatrix X Y)

Conjugation x ↦ X x Y by a matrix X with left inverse Y preserves matrix multiplication.

theorem TauCeti.ProjectiveGeneralLinear.coe_autToGeneralLinear_innerAut {n : ℕ} {A : Type w} [CommRing A] (g : GL (Fin n) A) : ↑((autToGeneralLinear n A) (Matrix.GeneralLinearGroup.innerAut g)) = conjugationMatrix (↑g) (↑g)⁻¹

The matrix of the inner automorphism by g is the conjugation matrix of g and g⁻¹.

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

The conjugation homomorphism GLₙ → PGLₙ, as a morphism of coordinate Hopf algebras O(PGLₙ) → O(GLₙ): the conjugation representation GLₙ → GL_{n²} on Mₙ lands in the automorphism group scheme of Mₙ.

Equations

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

theorem TauCeti.ProjectiveGeneralLinear.map_genericMatrix_conjugationMap (n : ℕ) (R : Type u) [CommRing R] : (GeneralLinear.genericMatrix R (n * n)).map ⇑(CommHopfAlgCat.Hom.hom (CategoryTheory.CategoryStruct.comp (CommHopfAlgCat.mkQuotient (GeneralLinear.coordinateHopfAlgebra R (n * n)) (definingHopfIdeal n R)) (conjugationMap n R))) = conjugationMatrix (GeneralLinear.genericMatrix R n) (GeneralLinear.genericMatrix R n)⁻¹

GLₙ → PGLₙ in coordinates: the conjugation homomorphism sends the generic matrix of GL_{n²}, read in O(PGLₙ), to the conjugation matrix of the generic matrix X of GLₙ, whose entry at ((p, q), (i, j)) is Xₚᵢ (X⁻¹)ⱼq.

@[simp]

theorem TauCeti.ProjectiveGeneralLinear.pointsMulEquiv_conjugationMap (n : ℕ) (R : Type u) [CommRing R] (A : CommAlgCat R) (g : ↑(HopfAlgebra.points A)) : (pointsMulEquiv n R A) (WithConv.toConv (g.ofConv.comp ↑(CommHopfAlgCat.Hom.hom (conjugationMap n R)))) = Matrix.GeneralLinearGroup.innerAut ((GeneralLinear.pointsMulEquiv n) g)

On points, GLₙ → PGLₙ is conjugation: a point g of GLₙ goes to the inner automorphism of Mₙ(A) by its invertible matrix.

theorem TauCeti.ProjectiveGeneralLinear.mem_quotientPointsSubgroup_kernelHopfIdeal_conjugationMap_iff (n : ℕ) {R : Type u} [CommRing R] (A : CommAlgCat R) (g : ↑(HopfAlgebra.points A)) : g ∈ CommHopfAlgCat.quotientPointsSubgroup (GeneralLinear.coordinateHopfAlgebra R n) (CommHopfAlgCat.kernelHopfIdeal (conjugationMap n R)) A ↔ (GeneralLinear.pointsMulEquiv n) g ∈ Subgroup.center (GL (Fin n) ↑A)

The kernel of GLₙ → PGLₙ on points: a point of GLₙ lies in the scheme-theoretic kernel exactly when its invertible matrix is central.

theorem TauCeti.ProjectiveGeneralLinear.kernelHopfIdeal_conjugationMap (n : ℕ) (k : Type u) [Field k] : CommHopfAlgCat.kernelHopfIdeal (conjugationMap n k) = CommHopfAlgCat.centerDefiningIdeal (GeneralLinear.coordinateHopfAlgebra k n)

The kernel of GLₙ → PGLₙ is the center of GLₙ: over a field, the kernel Hopf ideal of the conjugation homomorphism is the defining ideal of the center.

theorem TauCeti.ProjectiveGeneralLinear.mapPointsFunctor_conjugationMap_app_surjective (n : ℕ) {R : Type u} [CommRing R] (K : Type w) [Field K] [Algebra R K] : Function.Surjective ⇑(CategoryTheory.ConcreteCategory.hom ((CommHopfAlgCat.mapPointsFunctor (conjugationMap n R)).app ↧K))

GLₙ → PGLₙ is surjective on field-valued points: by the Skolem–Noether theorem, every point of PGLₙ with values in a field comes from a point of GLₙ.