The upper-triangular subgroup scheme of the general linear group

For a commutative ring R, specialize the weight-parabolic construction for GL_n to the strictly decreasing weights i ↦ n - 1 - i. The resulting finite-type closed subgroup scheme represents the group of invertible upper-triangular matrices over every commutative R-algebra. The pointwise identifications are assembled into a natural isomorphism of group-valued functors.

Main declarations

• TauCeti.GeneralLinear.UpperTriangular.groupScheme: the finite-type closed subgroup scheme of upper-triangular matrices in GL_n.
• TauCeti.GeneralLinear.UpperTriangular.pointsMulEquiv: its points over an R-algebra A are the group TauCeti.upperTriangularGroup (Fin n) A.
• TauCeti.GeneralLinear.UpperTriangular.definingHopfIdeal_toIdeal_le_ker and TauCeti.GeneralLinear.UpperTriangular.definingHopfIdeal_toIdeal_le_ker_of_isUpperTriangular: a coordinate morphism kills the defining Hopf ideal as soon as it kills the coordinates below the diagonal, equivalently as soon as its tautological matrix point is upper triangular.
• TauCeti.GeneralLinear.UpperTriangular.pointsNatIso: the corresponding natural isomorphism of group-valued functors.
• TauCeti.GeneralLinear.UpperTriangular.rootSubgroup: the positive root subgroup x_ij factored through the upper-triangular subgroup scheme for i < j.
• TauCeti.GeneralLinear.UpperTriangular.rootSubgroup_comp_inclusion: this factorization recovers the ambient root subgroup of GL_n.

References

• J. C. Jantzen, Representations of Algebraic Groups, I.2.
• T. A. Springer, Linear Algebraic Groups, Sections 2.4 and 6.3.
• J. S. Milne, Algebraic Groups (2017), Chapters 12--13.
• The quotient-points equivalence and functor proofs follow the pattern of TauCeti.Algebra.AlgebraicGroup.SpecialLinear.Basic; TauCeti.Algebra.AlgebraicGroup.GeneralLinear.Borel is their rank-two specialization.
• The root-subgroup declarations generalize the rank-two construction formerly in TauCeti.Algebra.AlgebraicGroup.GeneralLinear.Borel under the GL2Borel API.

This advances Layer 5, "Lie--Kolchin; solvable groups", of the ReductiveGroups roadmap. It constructs the general-rank group scheme whose abstract point groups were already proved solvable.

def TauCeti.GeneralLinear.UpperTriangular.weights (n : ℕ) : Fin n → ℤ

The strictly decreasing weights defining the standard upper-triangular subgroup of GL_n. The shift makes the rank-two specialization exactly (1, 0).

Equations

• TauCeti.GeneralLinear.UpperTriangular.weights n i = ↑n - 1 - ↑↑i

@[simp]

theorem TauCeti.GeneralLinear.UpperTriangular.weights_apply (n : ℕ) (i : Fin n) : weights n i = ↑n - 1 - ↑↑i

Formula for a standard upper-triangular weight.

theorem TauCeti.GeneralLinear.UpperTriangular.weights_lt_weights_iff (n : ℕ) (i j : Fin n) : weights n i < weights n j ↔ j < i

The standard weights decrease precisely when the row index increases.

theorem TauCeti.GeneralLinear.UpperTriangular.weights_injective (n : ℕ) : Function.Injective (weights n)

The standard upper-triangular weights are pairwise distinct.

def TauCeti.GeneralLinear.UpperTriangular.definingRelationSet (R : Type u) [CommRing R] (n : ℕ) : Set ↑(GeneralLinear.coordinateHopfAlgebra R n)

The matrix coordinates strictly below the diagonal.

Equations

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

@[simp]

theorem TauCeti.GeneralLinear.UpperTriangular.mem_definingRelationSet_iff (R : Type u) [CommRing R] (n : ℕ) (x : ↑(GeneralLinear.coordinateHopfAlgebra R n)) : x ∈ definingRelationSet R n ↔ ∃ (i : Fin n), ∃ j < i, x = (coordinateHopfAlgebraAlgEquiv R n) ((coordinateRingMap R n) (MvPolynomial.X (i, j)))

Membership in the defining relation set means being a coordinate below the diagonal.

@[simp]

theorem TauCeti.GeneralLinear.UpperTriangular.weightParabolicRelationSet_weights (R : Type u) [CommRing R] (n : ℕ) : weightParabolicRelationSet R (weights n) = definingRelationSet R n

For the standard decreasing weights, the weight-parabolic relations are exactly the coordinates strictly below the diagonal.

@[reducible, inline]

noncomputable abbrev TauCeti.GeneralLinear.UpperTriangular.definingHopfIdeal (R : Type u) [CommRing R] (n : ℕ) : HopfIdeal R ↑(GeneralLinear.coordinateHopfAlgebra R n)

The Hopf ideal generated by the matrix coordinates strictly below the diagonal.

Equations

• TauCeti.GeneralLinear.UpperTriangular.definingHopfIdeal R n = TauCeti.GeneralLinear.weightParabolicDefiningHopfIdeal R (TauCeti.GeneralLinear.UpperTriangular.weights n)

theorem TauCeti.GeneralLinear.UpperTriangular.definingHopfIdeal_toIdeal (R : Type u) [CommRing R] (n : ℕ) : (definingHopfIdeal R n).toIdeal = Ideal.span (definingRelationSet R n)

The underlying ideal of the upper-triangular Hopf ideal is generated by the coordinates strictly below the diagonal.

@[reducible, inline]

noncomputable abbrev TauCeti.GeneralLinear.UpperTriangular.coordinateHopfAlgebra (R : Type u) [CommRing R] (n : ℕ) : CommHopfAlgCat R

The coordinate Hopf algebra of the upper-triangular subgroup scheme.

Equations

• TauCeti.GeneralLinear.UpperTriangular.coordinateHopfAlgebra R n = TauCeti.GeneralLinear.weightParabolicCoordinateHopfAlgebra R (TauCeti.GeneralLinear.UpperTriangular.weights n)

@[reducible, inline]

noncomputable abbrev TauCeti.GeneralLinear.UpperTriangular.coordinateMap (R : Type u) [CommRing R] (n : ℕ) : GeneralLinear.coordinateHopfAlgebra R n ⟶ coordinateHopfAlgebra R n

The quotient coordinate morphism from O(GL_n) to the upper-triangular coordinate algebra.

Equations

• TauCeti.GeneralLinear.UpperTriangular.coordinateMap R n = TauCeti.GeneralLinear.weightParabolicCoordinateMap R (TauCeti.GeneralLinear.UpperTriangular.weights n)

theorem TauCeti.GeneralLinear.UpperTriangular.coordinateMap_def (R : Type u) [CommRing R] (n : ℕ) : coordinateMap R n = CommHopfAlgCat.mkQuotient (GeneralLinear.coordinateHopfAlgebra R n) (definingHopfIdeal R n)

The upper-triangular coordinate morphism is the canonical quotient morphism.

theorem TauCeti.GeneralLinear.UpperTriangular.coordinateMap_apply (R : Type u) [CommRing R] (n : ℕ) (h : ↑(GeneralLinear.coordinateHopfAlgebra R n)) : (CommHopfAlgCat.Hom.hom (coordinateMap R n)) h = (Ideal.Quotient.mkₐ R (definingHopfIdeal R n).toIdeal) h

The upper-triangular coordinate morphism sends an ambient coordinate to its quotient class.

@[reducible, inline]

noncomputable abbrev TauCeti.GeneralLinear.UpperTriangular.groupScheme (R : Type u) [CommRing R] (n : ℕ) : CategoryTheory.Grp (CategoryTheory.Over (AlgebraicGeometry.Spec ↧R))

The upper-triangular affine group scheme.

Equations

• TauCeti.GeneralLinear.UpperTriangular.groupScheme R n = TauCeti.GeneralLinear.weightParabolicGroupScheme R (TauCeti.GeneralLinear.UpperTriangular.weights n)

theorem TauCeti.GeneralLinear.UpperTriangular.groupScheme_def (R : Type u) [CommRing R] (n : ℕ) : groupScheme R n = CommHopfAlgCat.quotientSpec (GeneralLinear.coordinateHopfAlgebra R n) (definingHopfIdeal R n)

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

@[reducible, inline]

noncomputable abbrev TauCeti.GeneralLinear.UpperTriangular.inclusion (R : Type u) [CommRing R] (n : ℕ) : groupScheme R n ⟶ GeneralLinear.groupScheme R n

The closed-subgroup inclusion from the upper-triangular group scheme into GL_n.

Equations

• TauCeti.GeneralLinear.UpperTriangular.inclusion R n = TauCeti.GeneralLinear.weightParabolicInclusion R (TauCeti.GeneralLinear.UpperTriangular.weights n)

noncomputable def TauCeti.GeneralLinear.UpperTriangular.finiteTypeCoordinateHopfAlgebra (R : Type u) [CommRing R] (n : ℕ) : FiniteTypeCommHopfAlgCat R

The upper-triangular coordinate Hopf algebra, bundled with its finite-type property.

Equations

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

@[simp]

theorem TauCeti.GeneralLinear.UpperTriangular.finiteTypeCoordinateHopfAlgebra_obj (R : Type u) [CommRing R] (n : ℕ) : (finiteTypeCoordinateHopfAlgebra R n).obj = coordinateHopfAlgebra R n

The finite-type package has the upper-triangular coordinate Hopf algebra as its object.

theorem TauCeti.GeneralLinear.UpperTriangular.definingHopfIdeal_toIdeal_le_ker (R : Type u) [CommRing R] (n : ℕ) {A : Type w} [CommRing A] [Algebra R A] (f : ↑(GeneralLinear.coordinateHopfAlgebra R n) →ₐ[R] A) (hf : ∀ (i j : Fin n), j < i → f ((coordinateHopfAlgebraAlgEquiv R n) ((coordinateRingMap R n) (MvPolynomial.X (i, j)))) = 0) : (definingHopfIdeal R n).toIdeal ≤ RingHom.ker f.toRingHom

A morphism out of the coordinate algebra of GL_n kills the upper-triangular defining Hopf ideal as soon as it kills every matrix coordinate strictly below the diagonal.

theorem TauCeti.GeneralLinear.UpperTriangular.definingHopfIdeal_toIdeal_le_ker_of_isUpperTriangular (R : Type u) [CommRing R] (n : ℕ) {A : Type w} [CommRing A] [Algebra R A] (f : ↑(GeneralLinear.coordinateHopfAlgebra R n) →ₐ[R] A) (hf : (↑(pointToGeneralLinear n (WithConv.toConv f))).IsUpperTriangular) : (definingHopfIdeal R n).toIdeal ≤ RingHom.ker f.toRingHom

A morphism out of the coordinate algebra of GL_n whose tautological matrix point is upper triangular kills the upper-triangular defining Hopf ideal.

@[simp]

theorem TauCeti.GeneralLinear.UpperTriangular.mem_definingPointsSubgroup_iff (R : Type u) [CommRing R] (n : ℕ) {A : Type w} [CommRing A] [Algebra R A] (g : ↑(HopfAlgebra.points ↧A)) : g ∈ CommHopfAlgCat.quotientPointsSubgroup (GeneralLinear.coordinateHopfAlgebra R n) (definingHopfIdeal R n) ↧A ↔ (GeneralLinear.pointsMulEquiv n) g ∈ upperTriangularGroup (Fin n) A

An ambient GL_n-point belongs to the upper-triangular closed subgroup exactly when its matrix is upper triangular.

theorem TauCeti.GeneralLinear.UpperTriangular.hopfIdealPointsSubgroup_eq (R : Type u) [CommRing R] (n : ℕ) {A : Type w} [CommRing A] [Algebra R A] : hopfIdealPointsSubgroup n (definingHopfIdeal R n) A = upperTriangularGroup (Fin n) A

The matrix subgroup cut out by the upper-triangular Hopf ideal is exactly the group of invertible upper-triangular matrices.

noncomputable def TauCeti.GeneralLinear.UpperTriangular.pointsMulEquiv (R : Type u) [CommRing R] (n : ℕ) {A : Type w} [CommRing A] [Algebra R A] : ↑(HopfAlgebra.points ↧A) ≃* ↥(upperTriangularGroup (Fin n) A)

The group of algebra-valued points of the upper-triangular coordinate Hopf algebra is the group of invertible upper-triangular matrices.

Equations

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

@[simp]

theorem TauCeti.GeneralLinear.UpperTriangular.pointsMulEquiv_coe (R : Type u) [CommRing R] (n : ℕ) {A : Type w} [CommRing A] [Algebra R A] (f : ↑(HopfAlgebra.points ↧A)) : pointToGeneralLinear n ((CategoryTheory.ConcreteCategory.hom (CommHopfAlgCat.quotientPointsHom (GeneralLinear.coordinateHopfAlgebra R n) (definingHopfIdeal R n) ↧A)) f) = ↑((pointsMulEquiv R n) f)

Under the upper-triangular and general-linear point equivalences, the quotient-point inclusion is the ordinary inclusion of upper-triangular matrices into GL_n.

@[simp]

theorem TauCeti.GeneralLinear.UpperTriangular.quotientPointsHom_pointsMulEquiv_symm (R : Type u) [CommRing R] (n : ℕ) {A : Type w} [CommRing A] [Algebra R A] (g : ↥(upperTriangularGroup (Fin n) A)) : (CategoryTheory.ConcreteCategory.hom (CommHopfAlgCat.quotientPointsHom (GeneralLinear.coordinateHopfAlgebra R n) (definingHopfIdeal R n) ↧A)) ((pointsMulEquiv R n).symm g) = (GeneralLinear.pointsMulEquiv n).symm ↑g

The ambient point attached to an upper-triangular matrix is the general-linear point attached to its ordinary inclusion.

@[simp]

theorem TauCeti.GeneralLinear.UpperTriangular.pointsMulEquiv_mapValue (R : Type u) [CommRing R] (n : ℕ) {A : Type w} [CommRing A] [Algebra R A] {B : Type w'} [CommRing B] [Algebra R B] (phi : A →ₐ[R] B) (f : ↑(HopfAlgebra.points ↧A)) : (pointsMulEquiv R n) (WithConv.toConv (phi.comp f.ofConv)) = (UpperTriangularGroup.map phi.toRingHom) ((pointsMulEquiv R n) f)

The upper-triangular point equivalence is natural in the value algebra.

noncomputable def TauCeti.GeneralLinear.UpperTriangular.upperTriangularFunctor (R : Type u) [CommRing R] (n : ℕ) : CategoryTheory.Functor (CommAlgCat R) GrpCat

The group-valued functor sending an R-algebra to its invertible upper-triangular matrices.

Equations

• TauCeti.GeneralLinear.UpperTriangular.upperTriangularFunctor R n = (TauCeti.GeneralLinear.UpperTriangular.upperTriangularFunctorUnlifted✝ R n).comp GrpCat.uliftFunctor

theorem TauCeti.GeneralLinear.UpperTriangular.upperTriangularFunctor_obj (R : Type u) [CommRing R] (n : ℕ) (A : CommAlgCat R) : (upperTriangularFunctor R n).obj A = ↧(ULift.{u, w} ↥(upperTriangularGroup (Fin n) ↑A))

The object part of upperTriangularFunctor is the universe lift of the upper-triangular matrix group.

theorem TauCeti.GeneralLinear.UpperTriangular.upperTriangularFunctor_map (R : Type u) [CommRing R] (n : ℕ) {A B : CommAlgCat R} (phi : A ⟶ B) : (upperTriangularFunctor R n).map phi = CategoryTheory.CategoryStruct.comp (CategoryTheory.eqToHom ⋯) (CategoryTheory.CategoryStruct.comp (GrpCat.ofHom (MulEquiv.ulift.symm.toMonoidHom.comp ((UpperTriangularGroup.map (CommAlgCat.Hom.hom phi).toRingHom).comp MulEquiv.ulift.toMonoidHom))) (CategoryTheory.eqToHom ⋯))

The morphism part of upperTriangularFunctor is entrywise application, transported across the universe lift.

@[simp]

theorem TauCeti.GeneralLinear.UpperTriangular.upperTriangularFunctor_map_apply_apply (R : Type u) [CommRing R] (n : ℕ) {A B : CommAlgCat R} (phi : A ⟶ B) (g : ULift.{u, w} ↥(upperTriangularGroup (Fin n) ↑A)) (i j : Fin n) : ↑↑((CategoryTheory.ConcreteCategory.hom (CategoryTheory.eqToHom ⋯)) ((CategoryTheory.ConcreteCategory.hom ((upperTriangularFunctor R n).map phi)) ((CategoryTheory.ConcreteCategory.hom (CategoryTheory.eqToHom ⋯)) g))).down i j = (CommAlgCat.Hom.hom phi) (↑↑g.down i j)

The morphism part of the upper-triangular functor applies an algebra morphism entrywise.

noncomputable def TauCeti.GeneralLinear.UpperTriangular.pointsNatIso (R : Type u) [CommRing R] (n : ℕ) : HopfAlgebra.pointsFunctor ≅ upperTriangularFunctor R n

The functor of points of the upper-triangular coordinate Hopf algebra is naturally isomorphic to the upper-triangular matrix-group functor.

Equations

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

@[simp]

theorem TauCeti.GeneralLinear.UpperTriangular.pointsNatIso_hom_app_apply (R : Type u) [CommRing R] (n : ℕ) (A : CommAlgCat R) (f : ↑(HopfAlgebra.points A)) : ((CategoryTheory.ConcreteCategory.hom (CategoryTheory.eqToHom ⋯)) ((CategoryTheory.ConcreteCategory.hom ((pointsNatIso R n).hom.app A)) f)).down = (pointsMulEquiv R n) f

The forward component of pointsNatIso is the pointwise upper-triangular equivalence.

@[simp]

theorem TauCeti.GeneralLinear.UpperTriangular.pointsNatIso_inv_app_apply (R : Type u) [CommRing R] (n : ℕ) (A : CommAlgCat R) (g : ULift.{u, w} ↥(upperTriangularGroup (Fin n) ↑A)) : (CategoryTheory.ConcreteCategory.hom ((pointsNatIso R n).inv.app A)) ((CategoryTheory.ConcreteCategory.hom (CategoryTheory.eqToHom ⋯)) g) = (pointsMulEquiv R n).symm g.down

The inverse component of pointsNatIso is the inverse pointwise upper-triangular equivalence.

theorem TauCeti.GeneralLinear.UpperTriangular.rootSubgroupPoints_mem (R : Type u) [CommRing R] {n : ℕ} {i j : Fin n} (hij : i < j) {A : Type w} [CommRing A] [Algebra R A] (f : ↑(HopfAlgebra.points ↧A)) : (rootSubgroupPoints ⋯) f ∈ CommHopfAlgCat.quotientPointsSubgroup (GeneralLinear.coordinateHopfAlgebra R n) (definingHopfIdeal R n) ↧A

A root subgroup indexed by i < j consists of upper-triangular matrices, so its points lie in the standard upper-triangular closed subgroup.

noncomputable def TauCeti.GeneralLinear.UpperTriangular.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 x_ij, for i < j, into the standard upper-triangular coordinate Hopf algebra.

Equations

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

@[simp]

theorem TauCeti.GeneralLinear.UpperTriangular.coordinateMap_comp_rootSubgroupCoordinateMap (R : Type u) [CommRing R] {n : ℕ} {i j : Fin n} (hij : i < j) : CategoryTheory.CategoryStruct.comp (coordinateMap R n) (rootSubgroupCoordinateMap R hij) = GeneralLinear.rootSubgroupCoordinateMap ⋯

Precomposing a factored positive-root coordinate morphism with the upper-triangular quotient map recovers the ambient general-linear root-subgroup coordinate morphism.

@[simp]

theorem TauCeti.GeneralLinear.UpperTriangular.pointsMulEquiv_rootSubgroupCoordinateMap (R : Type u) [CommRing R] {n : ℕ} {i j : Fin n} (hij : i < j) {A : Type w} [CommRing A] [Algebra R A] (f : ↑(HopfAlgebra.points ↧A)) : ↑((pointsMulEquiv R n) (WithConv.toConv (f.ofConv.comp ↑(CommHopfAlgCat.Hom.hom (rootSubgroupCoordinateMap R hij))))) = (GeneralLinear.pointsMulEquiv n) ((rootSubgroupPoints ⋯) f)

Under the upper-triangular and general-linear point equivalences, the factored positive-root coordinate morphism gives the same transvection as the ambient root-subgroup morphism.

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

The positive root subgroup x_ij : 𝔾ₐ → B_n inside the standard upper-triangular subgroup scheme, for an ordered pair i < j.

Equations

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

theorem TauCeti.GeneralLinear.UpperTriangular.rootSubgroup_def (R : Type u) [CommRing R] {n : ℕ} {i j : Fin n} (hij : i < j) : rootSubgroup R hij = CategoryTheory.CategoryStruct.comp (CategoryTheory.eqToHom ⋯) (CategoryTheory.CategoryStruct.comp ((AlgebraicGeometry.hopfSpec ↧R).map (rootSubgroupCoordinateMap R hij).op) (CategoryTheory.eqToHom ⋯))

The upper-triangular root subgroup is relative spectrum applied contravariantly to its coordinate morphism, transported across the named presentations.

@[simp]

theorem TauCeti.GeneralLinear.UpperTriangular.rootSubgroup_comp_inclusion (R : Type u) [CommRing R] {n : ℕ} {i j : Fin n} (hij : i < j) : CategoryTheory.CategoryStruct.comp (rootSubgroup R hij) (inclusion R n) = GeneralLinear.rootSubgroup ⋯

Composing a positive root subgroup of the standard upper-triangular group with its inclusion into GL_n recovers the ambient root subgroup x_ij.