Documentation

TauCeti.Algebra.AlgebraicGroup.SpecialLinear.Conjugation

Conjugation from the special linear group to the projective general linear group #

Construct the coordinate morphism of SLₙ → PGLₙ by restricting the general linear conjugation morphism. In coordinates, it sends the generic matrix of PGLₙ ⊆ GL_{n²} to the conjugation matrix of the generic matrix of SLₙ and its inverse. Over every commutative value algebra it sends a determinant-one matrix to its inner automorphism of the matrix algebra. Over a field, for positive n, its scheme-theoretic kernel is the represented centre of SLₙ, hence μₙ. This identifies the whole kernel scheme, including its infinitesimal structure when the characteristic divides n.

The morphism is surjective on algebraically closed field-valued points. Its finiteness and the centrality of its kernel are proved in TauCeti.Algebra.AlgebraicGroup.SpecialLinear.CentralIsogeny; faithful flatness is not asserted.

References #

The construction reuses ProjectiveGeneralLinear.conjugationMap.

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

The coordinate morphism of SLₙ → PGLₙ, given by conjugation on the matrix algebra.

Equations
Instances For
    source
    theorem TauCeti.SpecialLinear.conjugationMap_def (n : ℕ) (R : Type u) [CommRing R] :
    conjugationMap n R = CategoryTheory.CategoryStruct.comp (ProjectiveGeneralLinear.conjugationMap n R) (coordinateMap R n)

    The special-linear conjugation morphism is the restriction of general-linear conjugation.

    source
    theorem TauCeti.SpecialLinear.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)) (ProjectiveGeneralLinear.definingHopfIdeal n R)) (conjugationMap n R))) = ProjectiveGeneralLinear.conjugationMatrix ((GeneralLinear.genericMatrix R n).map ⇑(CommHopfAlgCat.Hom.hom (coordinateMap R n))) ((GeneralLinear.genericMatrix R n).map ⇑(CommHopfAlgCat.Hom.hom (coordinateMap R n)))⁻¹

    SLₙ → 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 SLₙ, whose entry at ((p, q), (i, j)) is Xₚᵢ (X⁻¹)ⱼq.

    source
    @[simp]
    theorem TauCeti.SpecialLinear.pointsMulEquiv_conjugationMap (n : ℕ) {R : Type u} [CommRing R] (A : CommAlgCat R) (g : ↑(HopfAlgebra.points A)) :
    (ProjectiveGeneralLinear.pointsMulEquiv n R A) (WithConv.toConv (g.ofConv.comp ↑(CommHopfAlgCat.Hom.hom (conjugationMap n R)))) = Matrix.GeneralLinearGroup.innerAut (Matrix.SpecialLinearGroup.toGL ((pointsMulEquiv R n) g))

    On algebra-valued points, the conjugation morphism sends a special-linear matrix to its inner automorphism of the matrix algebra.

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

    The scheme-theoretic kernel on any commutative value algebra consists precisely of the central special-linear matrices.

    source
    theorem TauCeti.SpecialLinear.kernelHopfIdeal_conjugationMap (n : ℕ) {k : Type u} [Field k] (hn : 0 < n) :
    CommHopfAlgCat.kernelHopfIdeal (conjugationMap n k) = CommHopfAlgCat.centerDefiningIdeal (coordinateHopfAlgebra k n)

    Over a field, the kernel of SLₙ → PGLₙ is the represented centre of SLₙ. The equality is of defining Hopf ideals, so also detects nonreduced central subgroup schemes.

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

    Conjugation from SLₙ to PGLₙ is surjective on algebraically closed field-valued points, in every characteristic and also in rank zero.