The upper-triangular subgroup of the type-A full-weight carrier

The full-weight type-A_r carrier is an explicit closed subgroup scheme of GL_(r+1). This file intersects it scheme-theoretically with the standard upper-triangular subgroup scheme of GL_(r+1). On coordinate Hopf algebras, intersection is the join of the two defining Hopf ideals. The resulting TauCeti.SlStd.upperTriangularGroupScheme is therefore a closed subgroup scheme of the actual Chevalley carrier, not a separately chosen matrix group; it comes with closed immersions into both the carrier and the ambient upper-triangular subgroup scheme of GL_(r+1).

Over every commutative value ring A, its embedded matrix points are exactly

SlStd.points r A ∩ upperTriangularGroup (Fin (r + 1)) A.

The named split torus and every positive simple-root subgroup factor through this intersection as morphisms of group schemes, and their factorizations recompose to the carrier's own pinning morphisms. A negative simple-root point lies in the intersection exactly when its parameter is zero, so no comparable factorization of a negative root subgroup can exist: the construction selects the positive half of the carrier's pinning rather than merely containing all of its generators.

No maximal-solvability assertion is made here. Identifying this closed subgroup as a Borel and the named split torus as maximal requires the reductivity and root-datum structure of the carrier.

Main definitions

• TauCeti.SlStd.upperTriangularDefiningIdeal: the join of the carrier and upper-triangular defining Hopf ideals.
• TauCeti.SlStd.upperTriangularGroupScheme: the corresponding closed subgroup scheme.
• TauCeti.SlStd.upperTriangularInclusion: its closed immersion into the type-A carrier.
• TauCeti.SlStd.upperTriangularAmbientInclusion: its closed immersion into the upper-triangular subgroup scheme of GL_(r+1).
• TauCeti.SlStd.upperTriangularPoints: its matrix points inside GL_(r+1).
• TauCeti.SlStd.upperTriangularPointsPresentation: the presentation of those matrix points by their defining Hopf ideal. The shared GeneralLinear.IntegralPointsPresentation API supplies their maps, functor, and representing equivalence.
• TauCeti.SlStd.rootSubgroupUpperTriangular and TauCeti.SlStd.weightTorusUpperTriangular: the positive numbered root subgroups and the split weight torus, factored through it.

Main results

• TauCeti.SlStd.upperTriangularPoints_eq: the point group is the intersection of the carrier points with the upper-triangular matrices.
• TauCeti.SlStd.coe_mulEquiv_mapPointsFunctor_quotientMapOfLe: the point representation is compatible with inclusion into the carrier. Its compatibility with inclusion into GL_(r+1) is GeneralLinear.IntegralPointsPresentation.coe_mulEquiv_apply.
• TauCeti.SlStd.isUpperTriangular_coe_rootSubgroupPoints_positive and TauCeti.SlStd.rootSubgroupPoints_positive_mem_upperTriangularPoints: every positive numbered root subgroup point lies in the intersection.
• TauCeti.SlStd.isUpperTriangular_coe_rootSubgroupPoints_negative_iff and TauCeti.SlStd.rootSubgroupPoints_negative_mem_upperTriangularPoints_iff: a negative numbered root subgroup point lies in it only at the identity.
• TauCeti.SlStd.isUpperTriangular_coe_weightTorusPoints and TauCeti.SlStd.weightTorusPoints_mem_upperTriangularPoints: every split weight torus point lies in the intersection.
• TauCeti.SlStd.rootSubgroupUpperTriangular_comp_upperTriangularInclusion and TauCeti.SlStd.weightTorusUpperTriangular_comp_upperTriangularInclusion: the scheme-level factorizations recompose to the carrier's pinning morphisms.

References

• J. E. Humphreys, Linear Algebraic Groups, Sections 26--28.
• J. C. Jantzen, Representations of Algebraic Groups, I.2 and II.1.
• R. Steinberg, Lectures on Chevalley Groups, Sections 3--4.
• The ambient upper-triangular Hopf ideal, group scheme and point identification are TauCeti.Algebra.AlgebraicGroup.GeneralLinear.UpperTriangular.Basic; the intersection of point groups cut out by a join of Hopf ideals is TauCeti.GeneralLinear.hopfIdealPointsSubgroup_sup, resting on TauCeti.CommHopfAlgCat.quotientPointsSubgroup_sup from TauCeti.Algebra.AlgebraicGroup.HopfIdeal.Points.Order.
• The carrier itself, its defining ideal, its numbered root subgroups and its weight torus are the existing SlStd formalization in TauCeti.Algebra.Lie.SpecialLinear.StandardCarrier.Basic and TauCeti.Algebra.Lie.SpecialLinear.StandardCarrier.DeterminantOne, built on the Kostant root-subgroup scheme API of TauCeti.Algebra.Lie.UniversalEnveloping.Kostant.RootSubgroup.Scheme; the scheme-level factorizations below follow the same CommHopfAlgCat.liftQuotient pattern used there.

The scheme-theoretic intersection

noncomputable def TauCeti.SlStd.upperTriangularDefiningIdeal (r : ℕ) : HopfIdeal ℤ ↑(GeneralLinear.coordinateHopfAlgebra ℤ (r + 1))

The defining ideal of the upper-triangular subgroup of the type-A_r carrier. The join imposes both the carrier equations and the vanishing of every coordinate below the diagonal.

Equations

• TauCeti.SlStd.upperTriangularDefiningIdeal r = TauCeti.SlStd.definingIdeal r ⊔ TauCeti.GeneralLinear.UpperTriangular.definingHopfIdeal ℤ (r + 1)

theorem TauCeti.SlStd.definingIdeal_le_upperTriangularDefiningIdeal (r : ℕ) : definingIdeal r ≤ upperTriangularDefiningIdeal r

The carrier defining ideal is contained in the upper-triangular defining ideal.

theorem TauCeti.SlStd.generalLinearUpperTriangularDefiningHopfIdeal_le_upperTriangularDefiningIdeal (r : ℕ) : GeneralLinear.UpperTriangular.definingHopfIdeal ℤ (r + 1) ≤ upperTriangularDefiningIdeal r

The ambient upper-triangular defining ideal is contained in the upper-triangular defining ideal of the carrier.

@[reducible, inline]

noncomputable abbrev TauCeti.SlStd.upperTriangularGroupScheme (r : ℕ) : CategoryTheory.Grp (CategoryTheory.Over (AlgebraicGeometry.Spec ↧ℤ))

The upper-triangular closed subgroup scheme of the full-weight type-A_r carrier.

Equations

• TauCeti.SlStd.upperTriangularGroupScheme r = TauCeti.CommHopfAlgCat.quotientSpec (TauCeti.GeneralLinear.coordinateHopfAlgebra ℤ (r + 1)) (TauCeti.SlStd.upperTriangularDefiningIdeal r)

noncomputable def TauCeti.SlStd.upperTriangularInclusion (r : ℕ) : upperTriangularGroupScheme r ⟶ groupScheme r

The canonical closed immersion of the upper-triangular subgroup scheme into the type-A_r carrier, induced by the inclusion of defining Hopf ideals.

Equations

• TauCeti.SlStd.upperTriangularInclusion r = TauCeti.CommHopfAlgCat.quotientSpecMapOfLe (TauCeti.GeneralLinear.coordinateHopfAlgebra ℤ (r + 1)) ⋯

instance TauCeti.SlStd.isClosedImmersion_upperTriangularInclusion (r : ℕ) : AlgebraicGeometry.IsClosedImmersion (CategoryTheory.Over.Hom.left (upperTriangularInclusion r).hom.hom)

The upper-triangular subgroup scheme is closed in the type-A_r carrier.

noncomputable def TauCeti.SlStd.upperTriangularAmbientInclusion (r : ℕ) : upperTriangularGroupScheme r ⟶ GeneralLinear.UpperTriangular.groupScheme ℤ (r + 1)

The canonical closed immersion of the upper-triangular subgroup scheme of the type-A_r carrier into the ambient upper-triangular subgroup scheme of GL_(r+1).

Equations

• TauCeti.SlStd.upperTriangularAmbientInclusion r = TauCeti.CommHopfAlgCat.quotientSpecMapOfLe (TauCeti.GeneralLinear.coordinateHopfAlgebra ℤ (r + 1)) ⋯

instance TauCeti.SlStd.isClosedImmersion_upperTriangularAmbientInclusion (r : ℕ) : AlgebraicGeometry.IsClosedImmersion (CategoryTheory.Over.Hom.left (upperTriangularAmbientInclusion r).hom.hom)

The upper-triangular subgroup scheme of the carrier is closed in the ambient upper-triangular subgroup scheme of GL_(r+1).

@[simp]

theorem TauCeti.SlStd.upperTriangularInclusion_comp_carrierι (r : ℕ) : CategoryTheory.CategoryStruct.comp (upperTriangularInclusion r) (carrierι r) = CategoryTheory.CategoryStruct.comp (CommHopfAlgCat.quotientSpecι (GeneralLinear.coordinateHopfAlgebra ℤ (r + 1)) (upperTriangularDefiningIdeal r)) (CategoryTheory.eqToHom ⋯)

Including the upper-triangular subgroup into the carrier and then into GL_(r+1) is the quotient-spectrum inclusion cut out by the joined ideal.

@[simp]

theorem TauCeti.SlStd.upperTriangularAmbientInclusion_comp_inclusion (r : ℕ) : CategoryTheory.CategoryStruct.comp (upperTriangularAmbientInclusion r) (GeneralLinear.UpperTriangular.inclusion ℤ (r + 1)) = CategoryTheory.CategoryStruct.comp (upperTriangularInclusion r) (carrierι r)

The two closed immersions of the upper-triangular subgroup scheme agree over GL_(r+1).

Matrix points

noncomputable def TauCeti.SlStd.upperTriangularPoints (r : ℕ) (A : Type v) [CommRing A] : Subgroup (GL (Fin (r + 1)) A)

The matrix points of the upper-triangular subgroup scheme of the type-A_r carrier.

Equations

• TauCeti.SlStd.upperTriangularPoints r A = TauCeti.GeneralLinear.hopfIdealPointsSubgroup (r + 1) (TauCeti.SlStd.upperTriangularDefiningIdeal r) A

theorem TauCeti.SlStd.upperTriangularPoints_eq (r : ℕ) (A : Type v) [CommRing A] : upperTriangularPoints r A = points r A ⊓ upperTriangularGroup (Fin (r + 1)) A

The upper-triangular points of the carrier are the intersection of the carrier points and the invertible upper-triangular matrices. This is the general law that a join of Hopf ideals cuts out an intersection of point groups, specialized to the two ideals at hand.

@[simp]

theorem TauCeti.SlStd.mem_upperTriangularPoints_iff (r : ℕ) (A : Type v) [CommRing A] (g : GL (Fin (r + 1)) A) : g ∈ upperTriangularPoints r A ↔ g ∈ points r A ∧ (↑g).IsUpperTriangular

Membership in the upper-triangular carrier points means carrier membership together with upper triangularity of the underlying matrix.

The functor of points

@[reducible, inline]

noncomputable abbrev TauCeti.SlStd.upperTriangularPointsPresentation (r : ℕ) (A : Type v) [CommRing A] : GeneralLinear.IntegralPointsPresentation (r + 1) (upperTriangularDefiningIdeal r) A

The upper-triangular carrier points, presented by their joined defining Hopf ideal.

Equations

• TauCeti.SlStd.upperTriangularPointsPresentation r A = ⟨TauCeti.SlStd.upperTriangularPoints r A, ⋯⟩

theorem TauCeti.SlStd.coe_mulEquiv_mapPointsFunctor_quotientMapOfLe (r : ℕ) (A : CommAlgCat ℤ) (q : ↑(HopfAlgebra.points A)) : ↑((pointsPresentation r ↑A).mulEquiv ((CategoryTheory.ConcreteCategory.hom ((CommHopfAlgCat.mapPointsFunctor (CommHopfAlgCat.quotientMapOfLe (GeneralLinear.coordinateHopfAlgebra ℤ (r + 1)) ⋯)).app A)) q)) = ↑((upperTriangularPointsPresentation r ↑A).mulEquiv q)

The point representation is compatible with the closed immersion into the carrier. Pushing a point of the upper-triangular subgroup scheme into the carrier along the coordinate morphism underlying TauCeti.SlStd.upperTriangularInclusion does not change its matrix.

Triangularity of the pinning matrices

theorem TauCeti.SlStd.isUpperTriangular_coe_rootSubgroupPoints_positive (r : ℕ) (A : Type v) [CommRing A] (i : Fin r) (u : Multiplicative A) : (↑↑((rootSubgroupPoints r (Sum.inl i) A) u)).IsUpperTriangular

A positive numbered root-subgroup matrix is upper triangular.

theorem TauCeti.SlStd.isUpperTriangular_coe_rootSubgroupPoints_negative_iff (r : ℕ) (A : Type v) [CommRing A] (i : Fin r) (u : Multiplicative A) : (↑↑((rootSubgroupPoints r (Sum.inr i) A) u)).IsUpperTriangular ↔ Multiplicative.toAdd u = 0

A negative numbered root-subgroup matrix is upper triangular exactly when its parameter is zero: its only nonzero off-diagonal entry sits below the diagonal.

theorem TauCeti.SlStd.isUpperTriangular_coe_weightTorusPoints (r : ℕ) (A : Type v) [CommRing A] (s : Fin r → Aˣ) : (↑↑((weightTorusPoints r A) s)).IsUpperTriangular

A split weight torus matrix is diagonal, hence upper triangular.

The positive pinning lies in the intersection

theorem TauCeti.SlStd.rootSubgroupPoints_positive_mem_upperTriangularPoints (r : ℕ) (A : Type v) [CommRing A] (i : Fin r) (u : Multiplicative A) : ↑((rootSubgroupPoints r (Sum.inl i) A) u) ∈ upperTriangularPoints r A

Every positive numbered root-subgroup point belongs to the upper-triangular subgroup of the type-A_r carrier.

theorem TauCeti.SlStd.rootSubgroupPoints_negative_mem_upperTriangularPoints_iff (r : ℕ) (A : Type v) [CommRing A] (i : Fin r) (u : Multiplicative A) : ↑((rootSubgroupPoints r (Sum.inr i) A) u) ∈ upperTriangularPoints r A ↔ Multiplicative.toAdd u = 0

A negative numbered root-subgroup point lies in the upper-triangular subgroup exactly when its parameter is zero. In particular, the intersection selects the positive, rather than both, halves of the pinning.

theorem TauCeti.SlStd.weightTorusPoints_mem_upperTriangularPoints (r : ℕ) (A : Type v) [CommRing A] (s : Fin r → Aˣ) : ↑((weightTorusPoints r A) s) ∈ upperTriangularPoints r A

Every point of the named split weight torus belongs to the upper-triangular subgroup of the type-A_r carrier.

Scheme-level factorization of the positive pinning

noncomputable def TauCeti.SlStd.rootSubgroupUpperTriangular (r : ℕ) (i : Fin r) : AdditiveGroup.groupScheme ℤ ⟶ upperTriangularGroupScheme r

The positive numbered root subgroup, factored through the upper-triangular subgroup scheme of the type-A_r carrier.

Equations

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

noncomputable def TauCeti.SlStd.weightTorusUpperTriangular (r : ℕ) : SplitTorus.groupScheme ℤ (Fin r) ⟶ upperTriangularGroupScheme r

The split weight torus, factored through the upper-triangular subgroup scheme of the type-A_r carrier.

Equations

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

@[simp]

theorem TauCeti.SlStd.rootSubgroupUpperTriangular_comp_upperTriangularInclusion (r : ℕ) (i : Fin r) : CategoryTheory.CategoryStruct.comp (rootSubgroupUpperTriangular r i) (upperTriangularInclusion r) = rootSubgroup r (Sum.inl i)

Factoring a positive root subgroup through the upper-triangular subgroup and then including into the carrier recovers the carrier's own root subgroup.

@[simp]

theorem TauCeti.SlStd.weightTorusUpperTriangular_comp_upperTriangularInclusion (r : ℕ) : CategoryTheory.CategoryStruct.comp (weightTorusUpperTriangular r) (upperTriangularInclusion r) = weightTorus r

Factoring the split weight torus through the upper-triangular subgroup and then including into the carrier recovers the carrier's own weight torus.