Positive root subgroups in the special-linear Borel

The elementary root map xᵢⱼ : 𝔾ₐ → SLₙ factors through the upper-triangular closed subgroup when i < j. The factored map is a closed immersion and recovers the original map after inclusion in SLₙ. Over a nontrivial base ring, the converse holds: a root map factors through this subgroup exactly when the root is positive for the consecutive root base. Thus this is containment of represented root subgroups, over arbitrary rings, rather than a test of rational points or of tangent vectors alone.

On points over any commutative coefficient algebra, a negative root element lies in the upper-triangular subgroup exactly when its additive parameter is zero. This also covers nonreduced coefficient algebras and the zero ring.

The construction uses CommHopfAlgCat.liftQuotient and the existing special-linear root map. The general-linear analogue is GeneralLinear.UpperTriangular.rootSubgroupCoordinateMap.

References

• J. S. Milne, Algebraic Groups (2017), §21, Example 21.2.
• B. Conrad, Reductive Group Schemes (2014), §5.1 (root subgroups and pinnings).

@[simp]

theorem TauCeti.SpecialLinear.UpperTriangular.rootSubgroupPoints_mem_iff (R : Type u) [CommRing R] {n : ℕ} {i j : Fin n} {A : Type v} [CommRing A] [Algebra R A] (hij : i ≠ j) (f : ↑(HopfAlgebra.points ↧A)) : (rootSubgroupPoints hij) f ∈ CommHopfAlgCat.quotientPointsSubgroup (SpecialLinear.coordinateHopfAlgebra R n) (definingHopfIdeal R n) ↧A ↔ i < j ∨ Multiplicative.toAdd (AdditiveGroup.gaPointsMulEquiv f) = 0

A root element belongs to the upper-triangular subgroup exactly when its root is positive or its additive parameter vanishes.

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

Positive root-subgroup points lie in the upper-triangular subgroup over every commutative coefficient algebra.

theorem TauCeti.SpecialLinear.UpperTriangular.definingHopfIdeal_le_ker_rootSubgroupCoordinateMap (R : Type u) [CommRing R] {n : ℕ} {i j : Fin n} (hij : i < j) : (definingHopfIdeal R n).toIdeal ≤ RingHom.ker ↑↑(CommHopfAlgCat.Hom.hom (SpecialLinear.rootSubgroupCoordinateMap ⋯))

The coordinate morphism of a positive root subgroup kills the upper-triangular Hopf ideal, so the root map factors scheme-theoretically through the Borel.

@[simp]

theorem TauCeti.SpecialLinear.UpperTriangular.definingHopfIdeal_le_ker_rootSubgroupCoordinateMap_iff (R : Type u) [CommRing R] {n : ℕ} {i j : Fin n} [Nontrivial R] (hij : i ≠ j) : (definingHopfIdeal R n).toIdeal ≤ RingHom.ker ↑↑(CommHopfAlgCat.Hom.hom (SpecialLinear.rootSubgroupCoordinateMap hij)) ↔ i < j

Over a nontrivial base, a root map kills the Borel's defining ideal exactly when its row precedes its column. Testing the root element with parameter 1 detects the negative roots.

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

The coordinate morphism O(B) → O(𝔾ₐ) of a positive root subgroup of the upper-triangular determinant-one subgroup.

Equations

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

@[simp]

theorem TauCeti.SpecialLinear.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) = SpecialLinear.rootSubgroupCoordinateMap ⋯

The factorization through the Borel recovers the ambient root-coordinate map.

@[simp]

theorem TauCeti.SpecialLinear.UpperTriangular.coordinateMap_comp_rootSubgroupCoordinateMap_assoc (R : Type u) [CommRing R] {n : ℕ} {i j : Fin n} (hij : i < j) {Z : CommHopfAlgCat R} (h : AdditiveGroup.coordinateHopfAlgebra R ⟶ Z) : CategoryTheory.CategoryStruct.comp (coordinateMap R n) (CategoryTheory.CategoryStruct.comp (rootSubgroupCoordinateMap R hij) h) = CategoryTheory.CategoryStruct.comp (SpecialLinear.rootSubgroupCoordinateMap ⋯) h

The factorization through the Borel recovers the ambient root-coordinate map.

@[simp]

theorem TauCeti.SpecialLinear.UpperTriangular.pointsMulEquiv_rootSubgroupCoordinateMap (R : Type u) [CommRing R] {n : ℕ} {i j : Fin n} (hij : i < j) {A : Type v} [CommRing A] [Algebra R A] (f : ↑(HopfAlgebra.points ↧A)) : ↑((pointsMulEquiv R n) (WithConv.toConv (f.ofConv.comp ↑(CommHopfAlgCat.Hom.hom (rootSubgroupCoordinateMap R hij))))) = Matrix.SpecialLinearGroup.transvection ⋯ (Multiplicative.toAdd (AdditiveGroup.gaPointsMulEquiv f))

On algebra-valued points, the factored root map gives the same determinant-one transvection as the ambient root map.

theorem TauCeti.SpecialLinear.UpperTriangular.rootSubgroupCoordinateMap_surjective (R : Type u) [CommRing R] {n : ℕ} {i j : Fin n} (hij : i < j) : Function.Surjective ⇑(CommHopfAlgCat.Hom.hom (rootSubgroupCoordinateMap R hij))

The positive root subgroup is closed even as a subgroup of the Borel.

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

The positive root map into the represented upper-triangular subgroup of SLₙ.

Equations

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

@[simp]

theorem TauCeti.SpecialLinear.UpperTriangular.rootSubgroup_comp_quotientSpecι (R : Type u) [CommRing R] {n : ℕ} {i j : Fin n} (hij : i < j) : CategoryTheory.CategoryStruct.comp (rootSubgroup R hij) (CategoryTheory.CategoryStruct.comp (CommHopfAlgCat.quotientSpecι (SpecialLinear.coordinateHopfAlgebra R n) (definingHopfIdeal R n)) (CategoryTheory.eqToHom ⋯)) = SpecialLinear.rootSubgroup ⋯

Inclusion of a factored positive root subgroup in SLₙ recovers the elementary root map.

@[simp]

theorem TauCeti.SpecialLinear.UpperTriangular.rootSubgroup_comp_quotientSpecι_assoc (R : Type u) [CommRing R] {n : ℕ} {i j : Fin n} (hij : i < j) {Z : CategoryTheory.Grp (CategoryTheory.Over (AlgebraicGeometry.Spec ↧R))} (h : groupScheme R n ⟶ Z) : CategoryTheory.CategoryStruct.comp (rootSubgroup R hij) (CategoryTheory.CategoryStruct.comp (CommHopfAlgCat.quotientSpecι (SpecialLinear.coordinateHopfAlgebra R n) (definingHopfIdeal R n)) (CategoryTheory.CategoryStruct.comp (CategoryTheory.eqToHom ⋯) h)) = CategoryTheory.CategoryStruct.comp (SpecialLinear.rootSubgroup ⋯) h

Inclusion of a factored positive root subgroup in SLₙ recovers the elementary root map.

instance TauCeti.SpecialLinear.UpperTriangular.isClosedImmersion_rootSubgroup (R : Type u) [CommRing R] {n : ℕ} {i j : Fin n} (hij : i < j) : AlgebraicGeometry.IsClosedImmersion (CategoryTheory.Over.Hom.left (rootSubgroup R hij).hom.hom)

Each positive root map identifies 𝔾ₐ with a closed subgroup scheme of the Borel.

theorem TauCeti.SpecialLinear.UpperTriangular.definingHopfIdeal_le_ker_rootSubgroupCoordinateMap_iff_isPos (R : Type u) [CommRing R] [Nontrivial R] (r : ℕ) (p : SplitTorus.CoordinateRootIndex (Fin (r + 1))) : (definingHopfIdeal R (r + 1)).toIdeal ≤ RingHom.ker ↑↑(CommHopfAlgCat.Hom.hom (SpecialLinear.rootSubgroupCoordinateMap ⋯)) ↔ (diagonalRootBase r).IsPos p

A root of the diagonal root datum has its represented additive root subgroup inside the standard Borel exactly when it is positive.