The upper-unitriangular group scheme

For a commutative ring R, the polynomial Hopf algebra on the entries strictly above the diagonal represents the upper-unitriangular group U_n. The entrywise inclusion of upper-unitriangular matrices into GL_n is represented by a surjective coordinate Hopf-algebra morphism, and hence gives a closed immersion of affine group schemes.

The construction includes rank zero and the zero ring. As in the existing general-linear scheme interface, scheme-valued points are stated in the same universe as the base ring.

Main declarations

• TauCeti.UpperUnitriangular.coordinateMap: the coordinate morphism O(GL_n) ⟶ O(U_n).
• TauCeti.UpperUnitriangular.groupScheme: the finite-type affine upper-unitriangular group scheme on a finite linearly ordered index type.
• TauCeti.UpperUnitriangular.inclusion: the closed immersion U_n ⟶ GL_n.
• TauCeti.UpperUnitriangular.schemePointsMulEquiv: scheme-valued points are upper-unitriangular matrices on the chosen index type.

References

• J. C. Jantzen, Representations of Algebraic Groups, I.2.
• T. A. Springer, Linear Algebraic Groups, Section 2.4.

The functor-of-points recovery follows the pattern used for root subgroups in TauCeti.Algebra.AlgebraicGroup.GeneralLinear.Root.Subgroup.

noncomputable def TauCeti.UpperUnitriangular.inclusionPoints (R : Type u) [CommRing R] (n : ℕ) {A : Type w} [CommRing A] [Algebra R A] : WithConv (↑(coordinateHopfAlgebra R (Fin n)) →ₐ[R] A) →* WithConv (↑(GeneralLinear.coordinateHopfAlgebra R n) →ₐ[R] A)

On algebra-valued points, include an upper-unitriangular matrix into the general linear group.

Equations

• One or more equations did not get rendered due to their size.

@[simp]

theorem TauCeti.UpperUnitriangular.pointToGeneralLinear_inclusionPoints (R : Type u) [CommRing R] (n : ℕ) {A : Type w} [CommRing A] [Algebra R A] (f : WithConv (↑(coordinateHopfAlgebra R (Fin n)) →ₐ[R] A)) : GeneralLinear.pointToGeneralLinear n ((inclusionPoints R n) f) = ↑((pointsMulEquiv R (Fin n)) f)

The general-linear matrix attached to inclusionPoints f is the underlying matrix of the upper-unitriangular point attached to f.

theorem TauCeti.UpperUnitriangular.mapValue_inclusionPoints (R : Type u) [CommRing R] (n : ℕ) {A : Type w} [CommRing A] [Algebra R A] {B : Type w} [CommRing B] [Algebra R B] (φ : A →ₐ[R] B) (f : WithConv (↑(coordinateHopfAlgebra R (Fin n)) →ₐ[R] A)) : (AlgHom.mapValue φ) ((inclusionPoints R n) f) = (inclusionPoints R n) ((AlgHom.mapValue φ) f)

Inclusion of upper-unitriangular points commutes with extension of the value algebra.

noncomputable def TauCeti.UpperUnitriangular.inclusionPointsMap (R : Type u) [CommRing R] (n : ℕ) : HopfAlgebra.pointsFunctor ⟶ HopfAlgebra.pointsFunctor

The natural inclusion from upper-unitriangular points to general-linear points.

Equations

• TauCeti.UpperUnitriangular.inclusionPointsMap R n = { app := fun (A : CommAlgCat R) => GrpCat.ofHom (TauCeti.UpperUnitriangular.inclusionPoints R n), naturality := ⋯ }

noncomputable def TauCeti.UpperUnitriangular.coordinateMap (R : Type u) [CommRing R] (n : ℕ) : GeneralLinear.coordinateHopfAlgebra R n ⟶ coordinateHopfAlgebra R (Fin n)

The coordinate morphism O(GL_n) ⟶ O(U_n) recovered from the natural inclusion on points.

Equations

• TauCeti.UpperUnitriangular.coordinateMap R n = TauCeti.CommHopfAlgCat.homOfPointsMap (TauCeti.UpperUnitriangular.inclusionPointsMap R n)

theorem TauCeti.UpperUnitriangular.mapPointsFunctor_coordinateMap (R : Type u) [CommRing R] (n : ℕ) : CommHopfAlgCat.mapPointsFunctor (coordinateMap R n) = inclusionPointsMap R n

Precomposition by coordinateMap is the upper-unitriangular inclusion on points.

@[simp]

theorem TauCeti.UpperUnitriangular.mapPointsFunctor_coordinateMap_app (R : Type u) [CommRing R] (n : ℕ) (A : CommAlgCat R) (f : ↑(HopfAlgebra.points A)) : WithConv.toConv (f.ofConv.comp ↑(CommHopfAlgCat.Hom.hom (coordinateMap R n))) = (inclusionPoints R n) f

On every same-universe value algebra, coordinateMap induces the ordinary inclusion of upper-unitriangular matrices.

@[simp]

theorem TauCeti.UpperUnitriangular.coordinateMap_genericMatrix_apply (R : Type u) [CommRing R] (n : ℕ) (i j : Fin n) : (CommHopfAlgCat.Hom.hom (coordinateMap R n)) ((GeneralLinear.coordinateHopfAlgebraAlgEquiv R n) ((GeneralLinear.coordinateRingMap R n) (MvPolynomial.X (i, j)))) = (coordinateHopfAlgebraAlgEquiv R (Fin n)) (genericMatrix R (Fin n) i j)

The coordinate morphism sends a generic general-linear matrix entry to the corresponding entry of the generic upper-unitriangular matrix.

theorem TauCeti.UpperUnitriangular.coordinateMap_surjective (R : Type u) [CommRing R] (n : ℕ) : Function.Surjective ⇑(CommHopfAlgCat.Hom.hom (coordinateMap R n))

The coordinate morphism O(GL_n) ⟶ O(U_n) is surjective.

The group scheme and its closed immersion

noncomputable def TauCeti.UpperUnitriangular.groupScheme (R : Type u) [CommRing R] (m : Type) [Fintype m] [LinearOrder m] : CategoryTheory.Grp (CategoryTheory.Over (AlgebraicGeometry.Spec ↧R))

The upper-unitriangular group scheme obtained by applying relative spectrum to its coordinate Hopf algebra.

Equations

• TauCeti.UpperUnitriangular.groupScheme R m = (AlgebraicGeometry.hopfSpec ↧R).obj (Opposite.op (TauCeti.UpperUnitriangular.coordinateHopfAlgebra R m))

theorem TauCeti.UpperUnitriangular.groupScheme_def (R : Type u) [CommRing R] (m : Type) [Fintype m] [LinearOrder m] : groupScheme R m = (AlgebraicGeometry.hopfSpec ↧R).obj (Opposite.op (coordinateHopfAlgebra R m))

The upper-unitriangular group scheme is the Hopf spectrum of its coordinate algebra.

theorem TauCeti.UpperUnitriangular.groupScheme_X_left (R : Type u) [CommRing R] (m : Type) [Fintype m] [LinearOrder m] : (groupScheme R m).X.left = AlgebraicGeometry.Spec ↧↑(coordinateHopfAlgebra R m)

The underlying scheme is the spectrum of the upper-unitriangular coordinate Hopf algebra.

noncomputable def TauCeti.UpperUnitriangular.inclusion (R : Type u) [CommRing R] (n : ℕ) : groupScheme R (Fin n) ⟶ GeneralLinear.groupScheme R n

The closed immersion of the upper-unitriangular group scheme into GL_n.

Equations

• One or more equations did not get rendered due to their size.

theorem TauCeti.UpperUnitriangular.inclusion_def (R : Type u) [CommRing R] (n : ℕ) : inclusion R n = CategoryTheory.CategoryStruct.comp (CategoryTheory.eqToHom ⋯) (CategoryTheory.CategoryStruct.comp ((AlgebraicGeometry.hopfSpec ↧R).map (coordinateMap R n).op) (CategoryTheory.eqToHom ⋯))

The upper-unitriangular inclusion is relative spectrum applied contravariantly to coordinateMap.

instance TauCeti.UpperUnitriangular.isAffine_groupScheme (R : Type u) [CommRing R] (m : Type) [Fintype m] [LinearOrder m] : AlgebraicGeometry.IsAffine (groupScheme R m).X.left

The upper-unitriangular group scheme is affine.

instance TauCeti.UpperUnitriangular.locallyOfFiniteType_groupScheme (R : Type u) [CommRing R] (m : Type) [Fintype m] [LinearOrder m] : AlgebraicGeometry.LocallyOfFiniteType (groupScheme R m).X.hom

The structural morphism of the upper-unitriangular group scheme is locally of finite type.

instance TauCeti.UpperUnitriangular.isClosedImmersion_inclusion (R : Type u) [CommRing R] (n : ℕ) : AlgebraicGeometry.IsClosedImmersion (CategoryTheory.Over.Hom.left (inclusion R n).hom.hom)

The inclusion U_n ⟶ GL_n is a closed immersion.

Scheme-valued points

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

The canonical equivalence from algebra-valued points to scheme-valued upper-unitriangular points.

Equations

• TauCeti.UpperUnitriangular.groupSchemePointMulEquiv m A = TauCeti.CommHopfAlgCat.mapMulEquivOfPresentation (TauCeti.UpperUnitriangular.coordinateHopfAlgebra R m) A ⋯

@[simp]

theorem TauCeti.UpperUnitriangular.groupSchemePointMulEquiv_apply_left {R : Type u} [CommRing R] (m : Type) [Fintype m] [LinearOrder m] (A : Type u) [CommRing A] [Algebra R A] (f : WithConv (↑(coordinateHopfAlgebra R m) →ₐ[R] A)) : CategoryTheory.Over.Hom.left ((groupSchemePointMulEquiv m A) f) = CategoryTheory.CategoryStruct.comp (AlgebraicGeometry.Spec.map (CommRingCat.ofHom ↑f.ofConv)) (CategoryTheory.eqToHom ⋯)

The underlying spectrum map of the canonical algebra-to-scheme point equivalence.

noncomputable def TauCeti.UpperUnitriangular.schemePointsMulEquiv {R : Type u} [CommRing R] (m : Type) [Fintype m] [LinearOrder m] (A : Type u) [CommRing A] [Algebra R A] : ((AlgebraicGeometry.Spec ↧A).asOver (AlgebraicGeometry.Spec ↧R) ⟶ (groupScheme R m).X) ≃* ↥(upperUnitriangularGroup m A)

Scheme-valued upper-unitriangular points are upper-unitriangular matrices.

Equations

• TauCeti.UpperUnitriangular.schemePointsMulEquiv m A = (TauCeti.UpperUnitriangular.groupSchemePointMulEquiv m A).symm.trans (TauCeti.UpperUnitriangular.pointsMulEquiv R m)

@[simp]

theorem TauCeti.UpperUnitriangular.schemePointsMulEquiv_groupSchemePointMulEquiv {R : Type u} [CommRing R] (m : Type) [Fintype m] [LinearOrder m] (A : Type u) [CommRing A] [Algebra R A] (q : WithConv (↑(coordinateHopfAlgebra R m) →ₐ[R] A)) : (schemePointsMulEquiv m A) ((groupSchemePointMulEquiv m A) q) = (pointsMulEquiv R m) q

A scheme point presented by an algebra point corresponds to the same upper-unitriangular matrix under schemePointsMulEquiv.

theorem TauCeti.UpperUnitriangular.schemePointsMulEquiv_apply {R : Type u} [CommRing R] (m : Type) [Fintype m] [LinearOrder m] (A : Type u) [CommRing A] [Algebra R A] (p : (AlgebraicGeometry.Spec ↧A).asOver (AlgebraicGeometry.Spec ↧R) ⟶ (groupScheme R m).X) : (schemePointsMulEquiv m A) p = (pointsMulEquiv R m) ((groupSchemePointMulEquiv m A).symm p)

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

@[simp]

theorem TauCeti.UpperUnitriangular.schemePointsMulEquiv_symm_apply {R : Type u} [CommRing R] (m : Type) [Fintype m] [LinearOrder m] (A : Type u) [CommRing A] [Algebra R A] (g : ↥(upperUnitriangularGroup m A)) : (schemePointsMulEquiv m A).symm g = (groupSchemePointMulEquiv m A) ((pointsMulEquiv R m).symm g)

The inverse scheme-points equivalence presents an upper-unitriangular matrix as the corresponding spectrum point.

theorem TauCeti.UpperUnitriangular.schemePointsMulEquiv_mapValue {R : Type u} [CommRing R] (m : Type) [Fintype m] [LinearOrder m] (A : Type u) [CommRing A] [Algebra R A] {B : Type u} [CommRing B] [Algebra R B] (φ : A →ₐ[R] B) (p : (AlgebraicGeometry.Spec ↧A).asOver (AlgebraicGeometry.Spec ↧R) ⟶ (groupScheme R m).X) : (schemePointsMulEquiv m B) (CategoryTheory.CategoryStruct.comp (AlgebraicGeometry.Scheme.Hom.asOver (AlgebraicGeometry.Spec.map (CommRingCat.ofHom φ.toRingHom)) (AlgebraicGeometry.Spec ↧R)) p) = (UpperUnitriangularGroup.map φ.toRingHom) ((schemePointsMulEquiv m A) p)

The scheme-valued point identification is covariantly natural in the value algebra. An R-algebra map A → B becomes precomposition by the reversed spectrum map and acts entrywise on the corresponding upper-unitriangular matrix.

@[simp]

theorem TauCeti.UpperUnitriangular.schemePointsMulEquiv_comp_inclusion {R : Type u} [CommRing R] (n : ℕ) (A : Type u) [CommRing A] [Algebra R A] (p : (AlgebraicGeometry.Spec ↧A).asOver (AlgebraicGeometry.Spec ↧R) ⟶ (groupScheme R (Fin n)).X) : (GeneralLinear.schemePointsMulEquiv n A) (CategoryTheory.CategoryStruct.comp p (inclusion R n).hom.hom) = ↑((schemePointsMulEquiv (Fin n) A) p)

Composing a scheme-valued point with U_n ⟶ GL_n is ordinary subgroup inclusion on matrices.