Documentation

TauCeti.Algebra.AlgebraicGroup.GeneralLinear.Center

The center of the general linear group #

For a field k and a positive integer n, this file identifies the center of the general linear group scheme GLโ‚™ with the multiplicative group ๐”พโ‚˜. On points, a unit acts by its scalar matrix. Mathlib's theorem Matrix.GeneralLinearGroup.center_eq_range_scalar supplies the matrix-theoretic classification of the center; universal centrality then upgrades the classification from each individual group of points to the represented center.

The natural pointwise equivalence and full faithfulness of the Hopf-algebra functor of points give an isomorphism

  k[GLโ‚™] / I(Z(GLโ‚™)) โ‰… k[T, Tโปยน]

of commutative Hopf algebras. Thus the abstract center construction has the expected concrete coordinate algebra in the basic reductive example.

Main declarations #

References #

source
noncomputable def TauCeti.GeneralLinear.scalarTorusPoints {R : Type u} [CommRing R] (n : โ„•) {A : Type w} [CommRing A] [Algebra R A] :
WithConv (LaurentPolynomial R โ†’โ‚[R] A) โ†’* WithConv (โ†‘(coordinateHopfAlgebra R n) โ†’โ‚[R] A)

Send a multiplicative-group point to the corresponding scalar general-linear point.

Equations
  • One or more equations did not get rendered due to their size.
Instances For
    source
    @[simp]
    theorem TauCeti.GeneralLinear.pointToGeneralLinear_scalarTorusPoints {R : Type u} [CommRing R] (n : โ„•) {A : Type w} [CommRing A] [Algebra R A] (f : WithConv (LaurentPolynomial R โ†’โ‚[R] A)) :
    pointToGeneralLinear n ((scalarTorusPoints n) f) = (Matrix.GeneralLinearGroup.scalar (Fin n)) (MultiplicativeGroup.pointsMulEquiv f)

    Under the standard point equivalences, scalarTorusPoints is the usual scalar-matrix homomorphism.

    source
    theorem TauCeti.GeneralLinear.pointsMulEquiv_scalarTorusPoints {R : Type u} [CommRing R] (n : โ„•) {A : Type w} [CommRing A] [Algebra R A] (f : WithConv (LaurentPolynomial R โ†’โ‚[R] A)) :
    (pointsMulEquiv n) ((scalarTorusPoints n) f) = (Matrix.GeneralLinearGroup.scalar (Fin n)) (MultiplicativeGroup.pointsMulEquiv f)

    Under the multiplicative point equivalences, a scalar-torus point is the corresponding scalar matrix.

    source
    theorem TauCeti.GeneralLinear.mapValue_scalarTorusPoints {R : Type u} [CommRing R] (n : โ„•) {A : Type w} {B : Type w'} [CommRing A] [CommRing B] [Algebra R A] [Algebra R B] (ฯ† : A โ†’โ‚[R] B) (f : WithConv (LaurentPolynomial R โ†’โ‚[R] A)) :
    (AlgHom.mapValue ฯ†) ((scalarTorusPoints n) f) = (scalarTorusPoints n) ((AlgHom.mapValue ฯ†) f)

    The scalar-matrix construction is natural in the value algebra.

    source
    theorem TauCeti.GeneralLinear.scalarTorusPoints_injective {R : Type u} [CommRing R] (n : โ„•) (hn : 0 < n) {A : Type w} [CommRing A] [Algebra R A] :
    Function.Injective โ‡‘(scalarTorusPoints n)

    Scalar multiplication is injective in positive rank, stated on the represented point groups.

    source
    theorem TauCeti.GeneralLinear.scalarTorusPoints_isCentralPoint {R : Type u} [CommRing R] (n : โ„•) {A : Type u} [CommRing A] [Algebra R A] (f : WithConv (LaurentPolynomial R โ†’โ‚[R] A)) :
    HopfAlgebra.IsCentralPoint ((scalarTorusPoints n) f)

    Scalar points are universally central over any commutative base ring.

    source
    theorem TauCeti.GeneralLinear.scalarTorusPoints_mem_centerPointsSubgroup (n : โ„•) {k : Type u} [Field k] {A : Type u} [CommRing A] [Algebra k A] (f : WithConv (LaurentPolynomial k โ†’โ‚[k] A)) :
    (scalarTorusPoints n) f โˆˆ CommHopfAlgCat.centerPointsSubgroup (coordinateHopfAlgebra k n) โ†งA

    Every scalar point is a point of the represented center of GLโ‚™.

    source
    noncomputable def TauCeti.GeneralLinear.scalarTorusCenterHom (n : โ„•) {k : Type u} [Field k] (A : CommAlgCat k) :
    โ†‘(HopfAlgebra.points A) โ†’* โ†ฅ(CommHopfAlgCat.centerPointsSubgroup (coordinateHopfAlgebra k n) A)

    The scalar-matrix map with codomain restricted to the represented center.

    Equations
    • One or more equations did not get rendered due to their size.
    Instances For
      source
      @[simp]
      theorem TauCeti.GeneralLinear.coe_scalarTorusCenterHom_apply (n : โ„•) {k : Type u} [Field k] (A : CommAlgCat k) (f : โ†‘(HopfAlgebra.points A)) :
      โ†‘((scalarTorusCenterHom n A) f) = (scalarTorusPoints n) f

      The underlying value of scalarTorusCenterHom is the scalar-matrix point.

      source
      theorem TauCeti.GeneralLinear.scalarTorusCenterHom_bijective (n : โ„•) {k : Type u} [Field k] (hn : 0 < n) (A : CommAlgCat k) :
      Function.Bijective โ‡‘(scalarTorusCenterHom n A)

      In positive rank, scalar matrices give every universally central point of GLโ‚™.

      source
      theorem TauCeti.GeneralLinear.mem_centerPointsSubgroup_iff_exists_scalarTorusPoints (n : โ„•) {k : Type u} [Field k] (hn : 0 < n) (A : CommAlgCat k) (g : โ†‘(HopfAlgebra.points A)) :
      g โˆˆ CommHopfAlgCat.centerPointsSubgroup (coordinateHopfAlgebra k n) A โ†” โˆƒ (f : โ†‘(HopfAlgebra.points A)), (scalarTorusPoints n) f = g

      A general-linear point is universally central exactly when it is a scalar point.

      source
      theorem TauCeti.GeneralLinear.map_centerPointsSubgroup_pointsMulEquiv_eq_center (n : โ„•) {k : Type u} [Field k] (A : CommAlgCat k) :
      Subgroup.map (โ†‘(pointsMulEquiv n)) (CommHopfAlgCat.centerPointsSubgroup (coordinateHopfAlgebra k n) A) = Subgroup.center (GL (Fin n) โ†‘A)

      Under the standard equivalence between GLโ‚™-points and invertible matrices, the represented center maps onto the ordinary group-theoretic center.

      source
      noncomputable def TauCeti.GeneralLinear.scalarTorusCenterIso (n : โ„•) {k : Type u} [Field k] (hn : 0 < n) (A : CommAlgCat k) :
      HopfAlgebra.points A โ‰… โ†งโ†ฅ(CommHopfAlgCat.centerPointsSubgroup (coordinateHopfAlgebra k n) A)

      For every value algebra, scalar matrices identify the multiplicative group with the represented center of GLโ‚™.

      Equations
      Instances For
        source
        @[simp]
        theorem TauCeti.GeneralLinear.scalarTorusCenterIso_hom_apply (n : โ„•) {k : Type u} [Field k] (hn : 0 < n) (A : CommAlgCat k) (f : โ†‘(HopfAlgebra.points A)) :
        (CategoryTheory.ConcreteCategory.hom (scalarTorusCenterIso n hn A).hom) f = (scalarTorusCenterHom n A) f

        The forward component of scalarTorusCenterIso is the scalar-matrix homomorphism.

        source
        noncomputable def TauCeti.GeneralLinear.scalarTorusCenterNatIso (n : โ„•) {k : Type u} [Field k] (hn : 0 < n) :
        HopfAlgebra.pointsFunctor โ‰… CommHopfAlgCat.quotientPointsSubgroupFunctor (coordinateHopfAlgebra k n) (CommHopfAlgCat.centerDefiningIdeal (coordinateHopfAlgebra k n))

        Scalar matrices identify the multiplicative-group functor with the represented center subfunctor of GLโ‚™.

        Equations
        Instances For
          source
          @[simp]
          theorem TauCeti.GeneralLinear.scalarTorusCenterNatIso_hom_app_apply (n : โ„•) {k : Type u} [Field k] (hn : 0 < n) (A : CommAlgCat k) (f : โ†‘(HopfAlgebra.points A)) :
          (CategoryTheory.ConcreteCategory.hom ((scalarTorusCenterNatIso n hn).hom.app A)) f = (scalarTorusCenterHom n A) f

          The natural isomorphism sends a multiplicative-group point to its scalar matrix.

          source
          noncomputable def TauCeti.GeneralLinear.scalarTorusCenterCoordinatePointsNatIso (n : โ„•) {k : Type u} [Field k] (hn : 0 < n) :
          CommHopfAlgCat.pointsFunctor.obj (Opposite.op โ†ง(LaurentPolynomial k)) โ‰… CommHopfAlgCat.pointsFunctor.obj (Opposite.op (CommHopfAlgCat.quotient (coordinateHopfAlgebra k n) (CommHopfAlgCat.centerDefiningIdeal (coordinateHopfAlgebra k n))))

          The point functor of ๐”พโ‚˜ is naturally isomorphic to the point functor represented by the center coordinate Hopf algebra of GLโ‚™.

          Equations
          • One or more equations did not get rendered due to their size.
          Instances For
            source
            noncomputable def TauCeti.GeneralLinear.centerCoordinateLaurentIso (n : โ„•) {k : Type u} [Field k] (hn : 0 < n) :
            CommHopfAlgCat.quotient (coordinateHopfAlgebra k n) (CommHopfAlgCat.centerDefiningIdeal (coordinateHopfAlgebra k n)) โ‰… โ†ง(LaurentPolynomial k)

            The coordinate Hopf algebra of the center of positive-rank GLโ‚™ is the Laurent-polynomial Hopf algebra of ๐”พโ‚˜.

            Equations
            • One or more equations did not get rendered due to their size.
            Instances For
              source
              theorem TauCeti.GeneralLinear.pointsFunctor_mapIso_centerCoordinateLaurentIso (n : โ„•) {k : Type u} [Field k] (hn : 0 < n) :
              CommHopfAlgCat.pointsFunctor.mapIso (centerCoordinateLaurentIso n hn).op = scalarTorusCenterCoordinatePointsNatIso n hn

              Applying the functor of points to centerCoordinateLaurentIso recovers the scalar-matrix natural isomorphism used to construct it.