Documentation

TauCeti.Algebra.AlgebraicGroup.GeneralLinear.Root.Subgroup

The root subgroups of the general linear group #

For a pair of distinct indices i ≠ j, the elementary matrices xᵢⱼ(c) = 1 + c Eᵢⱼ form a one-parameter subgroup of GLₙ. This file promotes that family to a homomorphism of affine group schemes

xᵢⱼ : 𝔾ₐ → GLₙ

over an arbitrary commutative base ring R. On the A-points of 𝔾ₐ, which are the additive group of A, it is the map c ↦ xᵢⱼ(c) into the A-points of GLₙ, which are GL n A. The natural family of point maps determines a coordinate Hopf-algebra morphism by full faithfulness of the functor of points, and relative spectrum gives TauCeti.GeneralLinear.rootSubgroup as a morphism of affine group schemes.

Reading the index pair (i, j) as the root εᵢ - εⱼ of the diagonal torus of GLₙ, this is the root subgroup of that root. The relations it satisfies — additivity in the parameter, the Chevalley commutator relations, and the rescaling of the parameter under conjugation by the torus — all hold at the level of the matrices, and are proved in TauCeti/LinearAlgebra/Matrix/GeneralLinearGroup/Transvection.lean; the points equivalences TauCeti.GeneralLinear.pointsMulEquiv and TauCeti.AdditiveGroup.gaPointsMulEquiv transport them to any of the three views of the group. Nothing here needs R to be a field, and nothing needs the base to be reduced or the rank to be positive: the construction is the one over ℤ that a Chevalley–Demazure group of type A base changes from.

Formal references #

Main definitions #

Main results #

References #

source
noncomputable def TauCeti.GeneralLinear.rootSubgroupPoints {R : Type u} [CommRing R] {N : ℕ} {i j : Fin N} {A : Type w} [CommRing A] [Algebra R A] (hij : i ≠ j) :
WithConv (↑(AdditiveGroup.coordinateHopfAlgebra R) →ₐ[R] A) →* WithConv (↑(coordinateHopfAlgebra R N) →ₐ[R] A)

The root subgroup homomorphism on A-points: it sends the A-point c of 𝔾ₐ to the elementary matrix xᵢⱼ(c), an A-point of GLₙ.

Equations
  • One or more equations did not get rendered due to their size.
Instances For
    source
    theorem TauCeti.GeneralLinear.pointsMulEquiv_rootSubgroupPoints {R : Type u} [CommRing R] {N : ℕ} {i j : Fin N} {A : Type w} [CommRing A] [Algebra R A] (hij : i ≠ j) (f : WithConv (↑(AdditiveGroup.coordinateHopfAlgebra R) →ₐ[R] A)) :
    (pointsMulEquiv N) ((rootSubgroupPoints hij) f) = transvectionUnit hij (Multiplicative.toAdd (AdditiveGroup.gaPointsMulEquiv f))

    On points, the root subgroup homomorphism is the elementary matrix of the parameter. This is not a simp lemma, since TauCeti.GeneralLinear.pointsMulEquiv_apply rewrites its left-hand side.

    source
    theorem TauCeti.GeneralLinear.rootSubgroupPoints_injective {R : Type u} [CommRing R] {N : ℕ} {i j : Fin N} {A : Type w} [CommRing A] [Algebra R A] (hij : i ≠ j) :
    Function.Injective ⇑(rootSubgroupPoints hij)

    The root subgroup homomorphism on points is injective.

    source
    theorem TauCeti.GeneralLinear.mapValue_rootSubgroupPoints {R : Type u} [CommRing R] {N : ℕ} {i j : Fin N} {A : Type w} [CommRing A] [Algebra R A] {B : Type w} [CommRing B] [Algebra R B] (φ : A →ₐ[R] B) (hij : i ≠ j) (f : WithConv (↑(AdditiveGroup.coordinateHopfAlgebra R) →ₐ[R] A)) :
    (AlgHom.mapValue φ) ((rootSubgroupPoints hij) f) = (rootSubgroupPoints hij) ((AlgHom.mapValue φ) f)

    The root subgroup homomorphism is natural in the value algebra: the elementary matrix of the image parameter is the image of the elementary matrix.

    source
    noncomputable def TauCeti.GeneralLinear.rootSubgroupPointsMap {R : Type u} [CommRing R] {N : ℕ} {i j : Fin N} (hij : i ≠ j) :
    HopfAlgebra.pointsFunctor ⟶ HopfAlgebra.pointsFunctor

    The natural transformation of group-valued functors whose component at an A-point sends c to the elementary matrix xᵢⱼ(c).

    Equations
    Instances For
      source
      @[simp]
      theorem TauCeti.GeneralLinear.rootSubgroupPointsMap_app {R : Type u} [CommRing R] {N : ℕ} {i j : Fin N} (hij : i ≠ j) (A : CommAlgCat R) :
      (rootSubgroupPointsMap hij).app A = GrpCat.ofHom (rootSubgroupPoints hij)

      The component of the natural points map at a value algebra is the root subgroup homomorphism on points.

      source
      noncomputable def TauCeti.GeneralLinear.rootSubgroupCoordinateMap {R : Type u} [CommRing R] {N : ℕ} {i j : Fin N} (hij : i ≠ j) :
      coordinateHopfAlgebra R N ⟶ AdditiveGroup.coordinateHopfAlgebra R

      The coordinate morphism of the root subgroup, recovered from its natural action on points. Its direction is O(GLₙ) → O(𝔾ₐ), opposite to the represented group-scheme morphism.

      Equations
      Instances For
        source
        theorem TauCeti.GeneralLinear.mapPointsFunctor_rootSubgroupCoordinateMap {R : Type u} [CommRing R] {N : ℕ} {i j : Fin N} (hij : i ≠ j) :
        CommHopfAlgCat.mapPointsFunctor (rootSubgroupCoordinateMap hij) = rootSubgroupPointsMap hij

        Precomposition by the root-subgroup coordinate morphism is the previously constructed natural map on convolution points.

        source
        @[simp]
        theorem TauCeti.GeneralLinear.mapPointsFunctor_rootSubgroupCoordinateMap_app {R : Type u} [CommRing R] {N : ℕ} {i j : Fin N} (hij : i ≠ j) (A : CommAlgCat R) (f : ↑(HopfAlgebra.points A)) :
        (CategoryTheory.ConcreteCategory.hom ((CommHopfAlgCat.mapPointsFunctor (rootSubgroupCoordinateMap hij)).app A)) f = (rootSubgroupPoints hij) f

        On every same-universe value algebra, the map induced by the root-subgroup coordinate morphism is the elementary root subgroup homomorphism already constructed on points.

        source
        @[simp]
        theorem TauCeti.GeneralLinear.rootSubgroupCoordinateMap_apply_X {R : Type u} [CommRing R] {N : ℕ} {i j : Fin N} (hij : i ≠ j) (a b : Fin N) :
        (CommHopfAlgCat.Hom.hom (rootSubgroupCoordinateMap hij)) ((coordinateHopfAlgebraAlgEquiv R N) ((coordinateRingMap R N) (MvPolynomial.X (a, b)))) = 1 a b + Matrix.single i j ((SymmetricAlgebra.ι R R) 1) a b

        The root-subgroup coordinate map sends a generic matrix entry to the corresponding entry of 1 + X Eᵢⱼ.

        source
        theorem TauCeti.GeneralLinear.rootSubgroupCoordinateMap_surjective {R : Type u} [CommRing R] {N : ℕ} {i j : Fin N} (hij : i ≠ j) :
        Function.Surjective ⇑(CommHopfAlgCat.Hom.hom (rootSubgroupCoordinateMap hij))

        The root-subgroup coordinate morphism is surjective over every commutative base ring.

        source
        noncomputable def TauCeti.GeneralLinear.rootSubgroup {R : Type u} [CommRing R] {N : ℕ} {i j : Fin N} (hij : i ≠ j) :
        AdditiveGroup.groupScheme R ⟶ groupScheme R N

        The root subgroup of GLₙ attached to the root εᵢ - εⱼ: the affine group-scheme morphism 𝔾ₐ → GLₙ whose value on points is c ↦ xᵢⱼ(c).

        Equations
        • One or more equations did not get rendered due to their size.
        Instances For
          source
          theorem TauCeti.GeneralLinear.rootSubgroup_def {R : Type u} [CommRing R] {N : ℕ} {i j : Fin N} (hij : i ≠ j) :
          rootSubgroup hij = CategoryTheory.CategoryStruct.comp (CategoryTheory.eqToHom ⋯) (CategoryTheory.CategoryStruct.comp ((AlgebraicGeometry.hopfSpec ↧R).map (rootSubgroupCoordinateMap hij).op) (CategoryTheory.eqToHom ⋯))

          The root subgroup is relative spectrum applied contravariantly to its coordinate Hopf-algebra morphism, transported across the named presentations of 𝔾ₐ and GLₙ.

          source
          @[simp]
          theorem TauCeti.GeneralLinear.schemePointsMulEquiv_rootSubgroup {R : Type u} [CommRing R] {N : ℕ} {i j : Fin N} (A : Type u) [CommRing A] [Algebra R A] (hij : i ≠ j) (p : (AlgebraicGeometry.Spec ↧A).asOver (AlgebraicGeometry.Spec ↧R) ⟶ (AdditiveGroup.groupScheme R).X) :
          (schemePointsMulEquiv N A) (CategoryTheory.CategoryStruct.comp p (rootSubgroup hij).hom.hom) = transvectionUnit hij (Multiplicative.toAdd ((AdditiveGroup.schemePointsMulEquiv A) p))

          The root subgroup on scheme-valued points: composing an A-point of 𝔾ₐ with the root subgroup morphism gives the elementary matrix xᵢⱼ(c) of its parameter c, as an A-point of GLₙ.