Tangent Lie algebras of weight parabolics

The Lie algebra of the general-linear parabolic attached to integer coordinate weights consists of matrices preserving the decreasing weight filtration: the (i,j) entry vanishes whenever w i < w j. The tangent equivalence identifies the differential of the closed-subgroup inclusion with the inclusion of these block-triangular matrices. It works over arbitrary commutative base rings and coefficient algebras, including at rank zero and in positive characteristic.

The inverse-image criterion also computes the Lie algebra of the intersection of any represented subgroup of GL_N with this parabolic. In particular, self-dual coordinate weights give the tangent equations of symplectic flag stabilizers. These equations are used to test which root vectors lie in the chosen Borel.

The construction uses GeneralLinear.tangentLieEquivMatrix, HopfIdeal.quotientLieEquiv, and Mathlib's Matrix.blockTriangularSubalgebra rather than constructing a second block-triangular matrix Lie algebra. It follows the restriction construction of SpecialLinear.UpperTriangular.tangentLieEquiv.

References

• J. S. Milne, Algebraic Groups (2017), §§10.a and 13 (tangents and parabolics).
• B. Conrad, Reductive Group Schemes (2014), §5.1 (root spaces and pinnings).

theorem TauCeti.GeneralLinear.mem_lieSubalgebra_weightParabolicDefiningHopfIdeal_iff {R : Type u} [CommRing R] {B : Type v} [CommRing B] [Algebra R B] {N : ℕ} (w : Fin N → ℤ) (d : Derivation R (↑(coordinateHopfAlgebra R N)) (Bialgebra.CounitAlgebra R (↑(coordinateHopfAlgebra R N)) B)) : d ∈ (weightParabolicDefiningHopfIdeal R w).lieSubalgebra ↔ ((tangentMatrix N) d).BlockTriangular (⇑OrderDual.toDual ∘ w)

A tangent vector lies in the weight parabolic exactly when its matrix preserves the weight filtration. This is an explicit rewriting rule; the general Hopf-ideal membership lemma determines the simp normal form.

theorem TauCeti.GeneralLinear.map_lieSubalgebra_weightParabolicDefiningHopfIdeal {R : Type u} [CommRing R] {B : Type v} [CommRing B] [Algebra R B] {N : ℕ} (w : Fin N → ℤ) : LieSubalgebra.map (tangentLieEquivMatrix N).toLieHom (weightParabolicDefiningHopfIdeal R w).lieSubalgebra = lieSubalgebraOfSubalgebra B (Matrix (Fin N) (Fin N) B) (Matrix.blockTriangularSubalgebra B B (⇑OrderDual.toDual ∘ w))

The general-linear tangent equivalence carries the weight-parabolic tangent image onto Mathlib's block-triangular matrix Lie algebra.

noncomputable def TauCeti.GeneralLinear.weightParabolicTangentLieEquiv {R : Type u} [CommRing R] {B : Type v} [CommRing B] [Algebra R B] {N : ℕ} (w : Fin N → ℤ) : Derivation R (↑(weightParabolicCoordinateHopfAlgebra R w)) (Bialgebra.CounitAlgebra R (↑(weightParabolicCoordinateHopfAlgebra R w)) B) ≃ₗ⁅B⁆ ↥(lieSubalgebraOfSubalgebra B (Matrix (Fin N) (Fin N) B) (Matrix.blockTriangularSubalgebra B B (⇑OrderDual.toDual ∘ w)))

The Lie algebra of the represented weight parabolic is the block-triangular matrix Lie algebra for its decreasing weight filtration.

Equations

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

@[simp]

theorem TauCeti.GeneralLinear.weightParabolicTangentLieEquiv_apply_coe {R : Type u} [CommRing R] {B : Type v} [CommRing B] [Algebra R B] {N : ℕ} (w : Fin N → ℤ) (d : Derivation R (↑(weightParabolicCoordinateHopfAlgebra R w)) (Bialgebra.CounitAlgebra R (↑(weightParabolicCoordinateHopfAlgebra R w)) B)) : ↑((weightParabolicTangentLieEquiv w) d) = (tangentMatrix N) ((weightParabolicDefiningHopfIdeal R w).quotientLieHom d)

The tangent equivalence sends the closed-subgroup differential to its tangent matrix. The rule runs before simplification of the quotient-indexed coefficient algebra.

@[simp]

theorem TauCeti.GeneralLinear.tangentMatrix_quotientLieHom_weightParabolicTangentLieEquiv_symm {R : Type u} [CommRing R] {B : Type v} [CommRing B] [Algebra R B] {N : ℕ} (w : Fin N → ℤ) (X : ↥(lieSubalgebraOfSubalgebra B (Matrix (Fin N) (Fin N) B) (Matrix.blockTriangularSubalgebra B B (⇑OrderDual.toDual ∘ w)))) : (tangentMatrix N) ((weightParabolicDefiningHopfIdeal R w).quotientLieHom ((weightParabolicTangentLieEquiv w).symm X)) = ↑X

Descending a filtration-preserving matrix and differentiating its inclusion recovers that matrix. The rule runs before simplification of the quotient-indexed coefficient algebra.

theorem TauCeti.GeneralLinear.mem_lieSubalgebra_map_weightParabolicDefiningHopfIdeal_iff {R : Type u} [CommRing R] {B : Type v} [CommRing B] [Algebra R B] {N : ℕ} {H : Type u_1} [CommRing H] [HopfAlgebra R H] (w : Fin N → ℤ) (f : ↑(coordinateHopfAlgebra R N) →ₐc[R] H) (d : Derivation R H (Bialgebra.CounitAlgebra R H B)) : d ∈ ((weightParabolicDefiningHopfIdeal R w).map f).lieSubalgebra ↔ ((tangentMatrix N) ((derivationCompLieHom f) d)).BlockTriangular (⇑OrderDual.toDual ∘ w)

The tangent Lie algebra of the inverse image of a weight parabolic under a group homomorphism is cut out by the same forbidden entries of the differential.