Documentation

TauCeti.Algebra.AlgebraicGroup.SpecialLinear.Scheme

The special linear group scheme #

This file presents the special linear group scheme SLₙ as the closed subgroup scheme of GeneralLinear.groupScheme R n cut out by the determinant-one condition.

Main declarations #

References #

source
noncomputable def TauCeti.SpecialLinear.groupScheme (R : Type u) [CommRing R] (n : ℕ) :
CategoryTheory.Grp (CategoryTheory.Over (AlgebraicGeometry.Spec ↧R))

The special linear group scheme obtained by applying relative spectrum to the determinant-one coordinate Hopf algebra, which is the kernel Hopf-ideal quotient of GeneralLinear.coordinateHopfAlgebra.

Equations
Instances For
    source
    theorem TauCeti.SpecialLinear.groupScheme_def (R : Type u) [CommRing R] (n : ℕ) :
    groupScheme R n = (AlgebraicGeometry.hopfSpec ↧R).obj (Opposite.op (coordinateHopfAlgebra R n))

    The special linear group scheme is the relative spectrum of its determinant-one coordinate Hopf algebra.

    source
    theorem TauCeti.SpecialLinear.groupScheme_X_left (R : Type u) [CommRing R] (n : ℕ) :
    (groupScheme R n).X.left = AlgebraicGeometry.Spec ↧↑(coordinateHopfAlgebra R n)

    The scheme underlying the special linear group scheme is the spectrum of its coordinate Hopf algebra.

    source
    noncomputable def TauCeti.SpecialLinear.groupSchemeι (R : Type u) [CommRing R] (n : ℕ) :
    groupScheme R n ⟶ GeneralLinear.groupScheme R n

    The closed immersion of the special linear group scheme into the general linear group scheme.

    Equations
    • One or more equations did not get rendered due to their size.
    Instances For
      source
      theorem TauCeti.SpecialLinear.groupSchemeι_def (R : Type u) [CommRing R] (n : ℕ) :
      groupSchemeι R n = CategoryTheory.CategoryStruct.comp (CategoryTheory.eqToHom ⋯) (CategoryTheory.CategoryStruct.comp (CommHopfAlgCat.kernelSpecι (GeneralLinear.determinantCoordinateMap R n)) (CategoryTheory.eqToHom ⋯))

      The special-linear inclusion is the generic determinant-kernel inclusion transported to the named special-linear and general-linear presentations.

      source
      theorem TauCeti.SpecialLinear.groupSchemeι_comp_determinant (R : Type u) [CommRing R] (n : ℕ) :
      CategoryTheory.CategoryStruct.comp (groupSchemeι R n) (CategoryTheory.CategoryStruct.comp (CategoryTheory.eqToHom ⋯) ((AlgebraicGeometry.hopfSpec ↧R).map (GeneralLinear.determinantCoordinateMap R n).op)) = CategoryTheory.CategoryStruct.comp (CategoryTheory.eqToHom ⋯) ((AlgebraicGeometry.hopfSpec ↧R).map (CommHopfAlgCat.ofHom ((Bialgebra.unitBialgHom R ↑(coordinateHopfAlgebra R n)).comp (Bialgebra.counitBialgHom R ↑↧(MonoidAlgebra R (Multiplicative ℤ))))).op)

      The determinant is the unit section after restricting it along the named special-linear inclusion.

      source
      instance TauCeti.SpecialLinear.isClosedImmersion_groupSchemeι (R : Type u) [CommRing R] (n : ℕ) :
      AlgebraicGeometry.IsClosedImmersion (CategoryTheory.Over.Hom.left (groupSchemeι R n).hom.hom)

      The special-linear group scheme is a closed subgroup scheme of the named general-linear group scheme.

      source
      instance TauCeti.SpecialLinear.locallyOfFiniteType_groupScheme (R : Type u) [CommRing R] (n : ℕ) :
      AlgebraicGeometry.LocallyOfFiniteType (groupScheme R n).X.hom

      The structural morphism of the special-linear group scheme is locally of finite type.

      Scheme-valued points #

      source
      noncomputable def TauCeti.SpecialLinear.groupSchemePointMulEquiv {R : Type u} [CommRing R] (n : ℕ) (A : Type u) [CommRing A] [Algebra R A] :
      WithConv (↑(coordinateHopfAlgebra R n) →ₐ[R] A) ≃* ((AlgebraicGeometry.Spec ↧A).asOver (AlgebraicGeometry.Spec ↧R) ⟶ (groupScheme R n).X)

      Mathlib's spectrum-points equivalence for the special-linear coordinate Hopf algebra.

      Equations
      Instances For
        source
        @[simp]
        theorem TauCeti.SpecialLinear.groupSchemePointMulEquiv_apply_left {R : Type u} [CommRing R] (n : ℕ) (A : Type u) [CommRing A] [Algebra R A] (f : WithConv (↑(coordinateHopfAlgebra R n) →ₐ[R] A)) :
        CategoryTheory.Over.Hom.left ((groupSchemePointMulEquiv n A) f) = CategoryTheory.CategoryStruct.comp (AlgebraicGeometry.Spec.map (CommRingCat.ofHom ↑f.ofConv)) (CategoryTheory.eqToHom ⋯)

        The underlying spectrum map of the scheme point associated to a special-linear algebra point.

        source
        noncomputable def TauCeti.SpecialLinear.schemePointsMulEquiv {R : Type u} [CommRing R] (n : ℕ) (A : Type u) [CommRing A] [Algebra R A] :
        ((AlgebraicGeometry.Spec ↧A).asOver (AlgebraicGeometry.Spec ↧R) ⟶ (groupScheme R n).X) ≃* Matrix.SpecialLinearGroup (Fin n) A

        The group of scheme-valued points of the special-linear group scheme is the ordinary special linear group over the value algebra.

        Equations
        Instances For
          source
          @[simp]
          theorem TauCeti.SpecialLinear.schemePointsMulEquiv_groupSchemePointMulEquiv {R : Type u} [CommRing R] (n : ℕ) (A : Type u) [CommRing A] [Algebra R A] (q : WithConv (↑(coordinateHopfAlgebra R n) →ₐ[R] A)) :
          (schemePointsMulEquiv n A) ((groupSchemePointMulEquiv n A) q) = (pointsMulEquiv R n) q

          Evaluating the scheme-points equivalence on a point presented by groupSchemePointMulEquiv recovers the canonical algebra point.

          source
          @[simp]
          theorem TauCeti.SpecialLinear.schemePointsMulEquiv_symm_apply {R : Type u} [CommRing R] (n : ℕ) (A : Type u) [CommRing A] [Algebra R A] (g : Matrix.SpecialLinearGroup (Fin n) A) :
          (schemePointsMulEquiv n A).symm g = (groupSchemePointMulEquiv n A) ((pointsMulEquiv R n).symm g)

          The inverse scheme-points equivalence sends a determinant-one matrix to the spectrum point induced by its canonical coordinate-algebra point.

          source
          theorem TauCeti.SpecialLinear.schemePointsMulEquiv_apply {R : Type u} [CommRing R] (n : ℕ) (A : Type u) [CommRing A] [Algebra R A] (p : (AlgebraicGeometry.Spec ↧A).asOver (AlgebraicGeometry.Spec ↧R) ⟶ (groupScheme R n).X) :
          (schemePointsMulEquiv n A) p = (pointsMulEquiv R n) ((groupSchemePointMulEquiv n A).symm p)

          Evaluating the scheme-points equivalence directly on a scheme morphism.

          source
          @[simp]
          theorem TauCeti.SpecialLinear.schemePointsMulEquiv_comp_groupSchemeι {R : Type u} [CommRing R] (n : ℕ) (A : Type u) [CommRing A] [Algebra R A] (p : (AlgebraicGeometry.Spec ↧A).asOver (AlgebraicGeometry.Spec ↧R) ⟶ (groupScheme R n).X) :
          (GeneralLinear.schemePointsMulEquiv n A) (CategoryTheory.CategoryStruct.comp p (groupSchemeι R n).hom.hom) = Matrix.SpecialLinearGroup.toGL ((schemePointsMulEquiv n A) p)

          Composing a special-linear scheme point with the named inclusion into the general-linear group scheme is Mathlib's canonical inclusion Matrix.SpecialLinearGroup.toGL.