Documentation

TauCeti.Algebra.AlgebraicGroup.GeneralLinear.Projective

The projective general linear point functor #

The represented center of GLₙ maps isomorphically onto the ordinary center of its group of points. Consequently, its pointwise center quotient is Mathlib's projective general linear group PGL(n, A) over every commutative value algebra A. This file proves that identification and packages it naturally in A.

This is an identification of the presheaf quotient before fppf sheafification. It does not assert that the pointwise quotient is already an fppf sheaf, or construct a representing Hopf algebra.

Main declarations #

References #

source
noncomputable def TauCeti.GeneralLinear.centerPointwiseQuotientIsoPGL {k : Type u} [Field k] (n : ℕ) (A : CommAlgCat k) :
CommHopfAlgCat.centerPointwiseQuotient (coordinateHopfAlgebra k n) A ≅ ↧(Matrix.ProjGenLinGroup (Fin n) ↑A)

The pointwise quotient of GLₙ by its represented center is the projective general linear group over the same value algebra.

Equations
  • One or more equations did not get rendered due to their size.
Instances For
    source
    @[simp]
    theorem TauCeti.GeneralLinear.centerPointwiseQuotientIsoPGL_hom_mk {k : Type u} [Field k] (n : ℕ) (A : CommAlgCat k) (q : ↑(HopfAlgebra.points A)) :
    (CategoryTheory.ConcreteCategory.hom (centerPointwiseQuotientIsoPGL n A).hom) ↑q = Matrix.ProjGenLinGroup.mk ((pointsMulEquiv n) q)

    The quotient equivalence sends the class of a GLₙ-point to the class of its associated invertible matrix.

    source
    @[simp]
    theorem TauCeti.GeneralLinear.centerPointwiseQuotientIsoPGL_inv_mk {k : Type u} [Field k] (n : ℕ) (A : CommAlgCat k) (g : GL (Fin n) ↑A) :
    (CategoryTheory.ConcreteCategory.hom (centerPointwiseQuotientIsoPGL n A).inv) (Matrix.ProjGenLinGroup.mk g) = ↑((pointsMulEquiv n).symm g)

    The inverse quotient equivalence sends the class of an invertible matrix to the class of its associated GLₙ-point.

    source
    noncomputable def TauCeti.GeneralLinear.pglPointsFunctor (n : ℕ) {R : Type u} [CommRing R] :
    CategoryTheory.Functor (CommAlgCat R) GrpCat

    The presheaf A ↦ GLₙ(A) / Z(GLₙ(A)), with values given by Mathlib's Matrix.ProjGenLinGroup, packaged as a group-valued functor. This is not the functor of points of the algebraic group PGLₙ; obtaining that functor requires fppf sheafification.

    Equations
    • One or more equations did not get rendered due to their size.
    Instances For
      source
      @[simp]
      theorem TauCeti.GeneralLinear.pglPointsFunctor_obj (n : ℕ) {R : Type u} [CommRing R] (A : CommAlgCat R) :
      (pglPointsFunctor n).obj A = ↧(Matrix.ProjGenLinGroup (Fin n) ↑A)

      The objects of pglPointsFunctor are Mathlib's projective general linear groups.

      source
      @[simp]
      theorem TauCeti.GeneralLinear.pglPointsFunctor_map (n : ℕ) {R : Type u} [CommRing R] {A B : CommAlgCat R} (φ : A ⟶ B) :
      (pglPointsFunctor n).map φ = CategoryTheory.CategoryStruct.comp (CategoryTheory.eqToHom ⋯) (CategoryTheory.CategoryStruct.comp (GrpCat.ofHom (Matrix.ProjGenLinGroup.map ↑(CommAlgCat.Hom.hom φ))) (CategoryTheory.eqToHom ⋯))

      The maps of pglPointsFunctor are induced by entrywise extension of scalars.

      source
      theorem TauCeti.GeneralLinear.centerPointwiseQuotientIsoPGL_hom_naturality {k : Type u} [Field k] (n : ℕ) {A B : CommAlgCat k} (φ : A ⟶ B) :
      CategoryTheory.CategoryStruct.comp (CommHopfAlgCat.mapPointwiseQuotient (coordinateHopfAlgebra k n) (CommHopfAlgCat.centerDefiningIdeal (coordinateHopfAlgebra k n)) ⋯ φ) (centerPointwiseQuotientIsoPGL n B).hom = CategoryTheory.CategoryStruct.comp (centerPointwiseQuotientIsoPGL n A).hom (GrpCat.ofHom (Matrix.ProjGenLinGroup.map (CommAlgCat.Hom.hom φ).toRingHom))

      The quotient equivalence commutes with extension of scalars in the value algebra.

      source
      noncomputable def TauCeti.GeneralLinear.centerPointwiseQuotientNatIsoPGL {k : Type u} [Field k] (n : ℕ) :
      CommHopfAlgCat.pointwiseQuotientFunctor (coordinateHopfAlgebra k n) (CommHopfAlgCat.centerDefiningIdeal (coordinateHopfAlgebra k n)) ⋯ ≅ pglPointsFunctor n

      The pointwise center quotient of GLₙ is naturally isomorphic to the presheaf with values Mathlib's projective general linear groups. This is a presheaf-level statement before fppf sheafification, not an identification with the functor of points of the algebraic group PGLₙ.

      Equations
      • One or more equations did not get rendered due to their size.
      Instances For
        source
        @[simp]
        theorem TauCeti.GeneralLinear.centerPointwiseQuotientNatIsoPGL_hom_app {k : Type u} [Field k] (n : ℕ) (A : CommAlgCat k) :
        CategoryTheory.CategoryStruct.comp (CategoryTheory.eqToHom ⋯) (CategoryTheory.CategoryStruct.comp ((centerPointwiseQuotientNatIsoPGL n).hom.app A) (CategoryTheory.eqToHom ⋯)) = (centerPointwiseQuotientIsoPGL n A).hom

        After transport to the concrete quotient groups, the hom component of the natural identification is the objectwise quotient isomorphism.

        source
        @[simp]
        theorem TauCeti.GeneralLinear.centerPointwiseQuotientNatIsoPGL_inv_app {k : Type u} [Field k] (n : ℕ) (A : CommAlgCat k) :
        CategoryTheory.CategoryStruct.comp (CategoryTheory.eqToHom ⋯) (CategoryTheory.CategoryStruct.comp ((centerPointwiseQuotientNatIsoPGL n).inv.app A) (CategoryTheory.eqToHom ⋯)) = (centerPointwiseQuotientIsoPGL n A).inv

        After transport to the concrete quotient groups, the inverse component of the natural identification is the inverse objectwise quotient isomorphism.

        source
        @[simp]
        theorem TauCeti.GeneralLinear.centerPointwiseQuotientNatIsoPGL_hom_app_mk {k : Type u} [Field k] (n : ℕ) (A : CommAlgCat k) (q : ↑(HopfAlgebra.points A)) :
        (CategoryTheory.ConcreteCategory.hom (CategoryTheory.eqToHom ⋯)) ((CategoryTheory.ConcreteCategory.hom ((centerPointwiseQuotientNatIsoPGL n).hom.app A)) ((CategoryTheory.ConcreteCategory.hom (CategoryTheory.eqToHom ⋯)) ↑q)) = Matrix.ProjGenLinGroup.mk ((pointsMulEquiv n) q)

        After transport to the concrete quotient groups, the hom component of the natural identification sends a quotient class to the class of its associated invertible matrix.

        source
        @[simp]
        theorem TauCeti.GeneralLinear.centerPointwiseQuotientNatIsoPGL_inv_app_mk {k : Type u} [Field k] (n : ℕ) (A : CommAlgCat k) (g : GL (Fin n) ↑A) :
        (CategoryTheory.ConcreteCategory.hom (CategoryTheory.eqToHom ⋯)) ((CategoryTheory.ConcreteCategory.hom ((centerPointwiseQuotientNatIsoPGL n).inv.app A)) ((CategoryTheory.ConcreteCategory.hom (CategoryTheory.eqToHom ⋯)) (Matrix.ProjGenLinGroup.mk g))) = ↑((pointsMulEquiv n).symm g)

        After transport to the concrete quotient groups, the inverse component of the natural identification sends the class of an invertible matrix to its associated quotient class.