Documentation

TauCeti.Algebra.AlgebraicGroup.GeneralLinear.Conjugation

Conjugation of GLₙ by a constant matrix, in coordinates #

An invertible matrix P over the base ring R is an R-valued point of GLₙ, so inner conjugation by it is an automorphism of the affine group scheme GLₙ over R, and hence an automorphism of the coordinate Hopf algebra O(GLₙ/R). This file names that coordinate automorphism and records what it does on algebra-valued points: precomposing a point with it conjugates the corresponding invertible matrix by the image of P,

g ↦ P g P⁻¹.

This is the form in which a comparison of two closed subgroup schemes of GLₙ related by a change of basis is stated: a Hopf ideal is carried to another one exactly when the coordinate automorphism carries it there, and on points that is conjugation by the change-of-basis matrix.

Main declarations #

Main results #

References #

source
noncomputable def TauCeti.GeneralLinear.conjCoordinateIso {R : Type u} [CommRing R] {n : ℕ} (P : GL (Fin n) R) :
coordinateHopfAlgebra R n ≅ coordinateHopfAlgebra R n

The coordinate Hopf-algebra automorphism of GLₙ over R induced by conjugation by a constant invertible matrix P.

Equations
Instances For
    source
    theorem TauCeti.GeneralLinear.pointsMulEquiv_mapPointsFunctor_conjCoordinateIso {R : Type u} [CommRing R] {n : ℕ} (P : GL (Fin n) R) (A : CommAlgCat R) (f : ↑(HopfAlgebra.points A)) :
    (pointsMulEquiv n) ((CategoryTheory.ConcreteCategory.hom ((CommHopfAlgCat.mapPointsFunctor (conjCoordinateIso P).hom).app A)) f) = (Matrix.GeneralLinearGroup.map (algebraMap R ↑A)) P * (pointsMulEquiv n) f * ((Matrix.GeneralLinearGroup.map (algebraMap R ↑A)) P)⁻¹

    On algebra-valued points, the coordinate automorphism of conjugation by P is conjugation by the image of P.

    source
    theorem TauCeti.GeneralLinear.pointsMulEquiv_toConv_comp_conjCoordinateIso {R : Type u} [CommRing R] {n : ℕ} (P : GL (Fin n) R) (A : Type v) [CommRing A] [Algebra R A] (f : WithConv (↑(coordinateHopfAlgebra R n) →ₐ[R] A)) :
    (pointsMulEquiv n) (WithConv.toConv (f.ofConv.comp ↑(CommHopfAlgCat.Hom.hom (conjCoordinateIso P).hom))) = (Matrix.GeneralLinearGroup.map (algebraMap R A)) P * (pointsMulEquiv n) f * ((Matrix.GeneralLinearGroup.map (algebraMap R A)) P)⁻¹

    Precomposing a point with the coordinate automorphism of conjugation by P conjugates its matrix by the image of P, over a value ring in any universe.

    source
    @[simp]
    theorem TauCeti.GeneralLinear.conjCoordinateIso_inv {R : Type u} [CommRing R] {n : ℕ} (P : GL (Fin n) R) :
    conjCoordinateIso P⁻¹ = (conjCoordinateIso P).symm

    Conjugation by the inverse matrix is the inverse coordinate automorphism.