The standard complete isotropic flag subgroup of the symplectic group

In paired coordinates e₀, …, eₘ₋₁, f₀, …, fₘ₋₁, the standard complete isotropic flag is spanned successively by e₀, by e₀, e₁, and so on. Its self-dual completion orders the full basis as e₀, …, eₘ₋₁, fₘ₋₁, …, f₀. This file constructs the finite-type closed subgroup of Sp₂ₘ whose matrices are upper triangular in this order. In the original paired order these matrices have upper-triangular upper-left block, lower-triangular lower-right block, and zero lower-left block.

The quotient Hopf algebra represents these matrices over every commutative algebra, including nonreduced algebras and characteristic two. Its algebra-valued point groups are solvable. The diagonal symplectic torus factorization is developed in TauCeti.Algebra.AlgebraicGroup.Symplectic.IsotropicFlag.DiagonalTorus. These constructions provide the flag subgroup used in the standard symplectic pinning; no smoothness, connectedness, or Borel maximality assertion is made here.

The construction uses GeneralLinear.weightParabolicDefiningHopfIdeal; the quotient points arguments follow TauCeti.Algebra.AlgebraicGroup.SpecialLinear.UpperTriangular.Basic.

References

• J. S. Milne, Algebraic Groups (2017), §24.6 (symplectic groups and isotropic flags).
• B. Conrad, Reductive Group Schemes (2014), §5.1 (pinnings).

def TauCeti.Symplectic.IsotropicFlag.weights (m : ℕ) : Fin (m + m) → ℤ

General-linear upper-triangular weights read in the self-dual flag order.

Equations

• TauCeti.Symplectic.IsotropicFlag.weights m = TauCeti.GeneralLinear.UpperTriangular.weights (m + m) ∘ ⇑(TauCeti.GLSymplecticFin.IsotropicFlag.flagOrder m)

@[simp]

theorem TauCeti.Symplectic.IsotropicFlag.weights_apply (m : ℕ) (i : Fin (m + m)) : weights m i = GeneralLinear.UpperTriangular.weights (m + m) ((GLSymplecticFin.IsotropicFlag.flagOrder m) i)

The flag weight at a basis index is the upper-triangular weight of its flag-order index.

theorem TauCeti.Symplectic.IsotropicFlag.weights_lt_weights_iff (m : ℕ) (i j : Fin (m + m)) : weights m i < weights m j ↔ (GLSymplecticFin.IsotropicFlag.flagOrder m) j < (GLSymplecticFin.IsotropicFlag.flagOrder m) i

The flag weights decrease precisely when the flag-order index increases.

theorem TauCeti.Symplectic.IsotropicFlag.weights_injective (m : ℕ) : Function.Injective (weights m)

The flag weights are pairwise distinct.

noncomputable def TauCeti.Symplectic.IsotropicFlag.definingHopfIdeal (R : Type u) [CommRing R] (m : ℕ) : HopfIdeal R ↑(Symplectic.coordinateHopfAlgebra R m)

The Hopf ideal cutting out the standard complete isotropic flag subgroup in Sp₂ₘ. It is the image of GeneralLinear.weightParabolicDefiningHopfIdeal for the upper-triangular weights composed with flagOrder m, under symplectic coordinate restriction.

Equations

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

theorem TauCeti.Symplectic.IsotropicFlag.definingHopfIdeal_def (R : Type u) [CommRing R] (m : ℕ) : definingHopfIdeal R m = (GeneralLinear.weightParabolicDefiningHopfIdeal R (weights m)).map (CommHopfAlgCat.Hom.hom (Symplectic.coordinateMap R m))

The flag ideal is the symplectic restriction of the flag-order weight-parabolic ideal.

theorem TauCeti.Symplectic.IsotropicFlag.definingHopfIdeal_toIdeal (R : Type u) [CommRing R] (m : ℕ) : (definingHopfIdeal R m).toIdeal = Ideal.span (⇑(CommHopfAlgCat.Hom.hom (Symplectic.coordinateMap R m)) '' GeneralLinear.weightParabolicRelationSet R (weights m))

The flag ideal is generated by the generic symplectic entries strictly below the diagonal in the self-dual flag order.

theorem TauCeti.Symplectic.IsotropicFlag.definingHopfIdeal_toIdeal_fg (R : Type u) [CommRing R] (m : ℕ) : (definingHopfIdeal R m).toIdeal.FG

The isotropic flag subgroup is defined by finitely many equations.

@[reducible, inline]

noncomputable abbrev TauCeti.Symplectic.IsotropicFlag.coordinateHopfAlgebra (R : Type u) [CommRing R] (m : ℕ) : CommHopfAlgCat R

The coordinate Hopf algebra of the standard complete isotropic flag subgroup.

Equations

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

@[reducible, inline]

noncomputable abbrev TauCeti.Symplectic.IsotropicFlag.coordinateMap (R : Type u) [CommRing R] (m : ℕ) : Symplectic.coordinateHopfAlgebra R m ⟶ coordinateHopfAlgebra R m

Coordinate restriction from the symplectic group to the isotropic flag subgroup.

Equations

• TauCeti.Symplectic.IsotropicFlag.coordinateMap R m = TauCeti.CommHopfAlgCat.mkQuotient (TauCeti.Symplectic.coordinateHopfAlgebra R m) (TauCeti.Symplectic.IsotropicFlag.definingHopfIdeal R m)

instance TauCeti.Symplectic.IsotropicFlag.instAlgebraFiniteTypeCoordinateHopfAlgebra (R : Type u) [CommRing R] (m : ℕ) : Algebra.FiniteType R ↑(coordinateHopfAlgebra R m)

The isotropic flag subgroup has finite-type coordinate algebra.

@[reducible, inline]

noncomputable abbrev TauCeti.Symplectic.IsotropicFlag.groupScheme (R : Type u) [CommRing R] (m : ℕ) : CategoryTheory.Grp (CategoryTheory.Over (AlgebraicGeometry.Spec ↧R))

The closed subgroup scheme of Sp₂ₘ of symplectic matrices preserving the standard complete isotropic flag.

Equations

• TauCeti.Symplectic.IsotropicFlag.groupScheme R m = TauCeti.CommHopfAlgCat.quotientSpec (TauCeti.Symplectic.coordinateHopfAlgebra R m) (TauCeti.Symplectic.IsotropicFlag.definingHopfIdeal R m)

@[reducible, inline]

noncomputable abbrev TauCeti.Symplectic.IsotropicFlag.inclusion (R : Type u) [CommRing R] (m : ℕ) : CommHopfAlgCat.quotientSpec (Symplectic.coordinateHopfAlgebra R m) (definingHopfIdeal R m) ⟶ (AlgebraicGeometry.hopfSpec ↧R).obj (Opposite.op (Symplectic.coordinateHopfAlgebra R m))

The closed-subgroup inclusion of the isotropic flag subgroup into the symplectic group.

Equations

• TauCeti.Symplectic.IsotropicFlag.inclusion R m = TauCeti.CommHopfAlgCat.quotientSpecι (TauCeti.Symplectic.coordinateHopfAlgebra R m) (TauCeti.Symplectic.IsotropicFlag.definingHopfIdeal R m)

@[simp]

theorem TauCeti.Symplectic.IsotropicFlag.mem_definingPointsSubgroup_iff (R : Type u) [CommRing R] (m : ℕ) {A : Type w} [CommRing A] [Algebra R A] (g : ↑(HopfAlgebra.points ↧A)) : g ∈ CommHopfAlgCat.quotientPointsSubgroup (Symplectic.coordinateHopfAlgebra R m) (definingHopfIdeal R m) ↧A ↔ (Symplectic.pointsMulEquiv R m) g ∈ GLSymplecticFin.IsotropicFlag.matrixSubgroup m

A symplectic point belongs to the isotropic flag subgroup precisely when its matrix is upper triangular after reversing the dual half of the basis.

noncomputable def TauCeti.Symplectic.IsotropicFlag.pointsMulEquiv (R : Type u) [CommRing R] (m : ℕ) {A : Type w} [CommRing A] [Algebra R A] : ↑(HopfAlgebra.points ↧A) ≃* ↥(GLSymplecticFin.IsotropicFlag.matrixSubgroup m)

The algebra-valued points of the isotropic flag subgroup are exactly the symplectic matrices upper triangular in the self-dual flag order.

Equations

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

@[simp]

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

The quotient-point inclusion agrees with the inclusion of flag-preserving symplectic matrices.

@[simp]

theorem TauCeti.Symplectic.IsotropicFlag.quotientPointsHom_pointsMulEquiv_symm (R : Type u) [CommRing R] (m : ℕ) {A : Type w} [CommRing A] [Algebra R A] (g : ↥(GLSymplecticFin.IsotropicFlag.matrixSubgroup m)) : (CategoryTheory.ConcreteCategory.hom (CommHopfAlgCat.quotientPointsHom (Symplectic.coordinateHopfAlgebra R m) (definingHopfIdeal R m) ↧A)) ((pointsMulEquiv R m).symm g) = (Symplectic.pointsMulEquiv R m).symm ↑g

The ambient point of a flag-preserving matrix is the symplectic point of that matrix.

theorem TauCeti.Symplectic.IsotropicFlag.pointsMulEquiv_mapValue (R : Type u) [CommRing R] (m : ℕ) {A : Type w} [CommRing A] [Algebra R A] {B : Type v} [CommRing B] [Algebra R B] (phi : A →ₐ[R] B) (f : ↑(HopfAlgebra.points ↧A)) : (pointsMulEquiv R m) ((AlgHom.mapValue phi) f) = (GLSymplecticFin.IsotropicFlag.map m ↑phi) ((pointsMulEquiv R m) f)

The flag-subgroup point equivalence is natural in the value algebra.

theorem TauCeti.Symplectic.IsotropicFlag.mapValue_pointsMulEquiv_symm_apply (R : Type u) [CommRing R] (m : ℕ) {A : Type w} [CommRing A] [Algebra R A] {B : Type v} [CommRing B] [Algebra R B] (phi : A →ₐ[R] B) (g : ↥(GLSymplecticFin.IsotropicFlag.matrixSubgroup m)) : (AlgHom.mapValue phi) ((pointsMulEquiv R m).symm g) = (pointsMulEquiv R m).symm ((GLSymplecticFin.IsotropicFlag.map m ↑phi) g)

The inverse flag-subgroup point equivalence is natural in the value algebra.

theorem TauCeti.Symplectic.IsotropicFlag.isSolvable_points (R : Type u) [CommRing R] (m : ℕ) {A : Type w} [CommRing A] [Algebra R A] : Group.IsSolvable ↑(HopfAlgebra.points ↧A)

Every algebra-valued point group of the isotropic flag subgroup is solvable.

theorem TauCeti.Symplectic.IsotropicFlag.geometricallySolvablePointsCommHopfAlgProperty_coordinateHopfAlgebra (m : ℕ) (k : Type u) [Field k] : geometricallySolvablePointsCommHopfAlgProperty k (coordinateHopfAlgebra k m)

The isotropic flag subgroup has solvable geometric points over every field.