Documentation

TauCeti.Algebra.AlgebraicGroup.Symplectic.IsotropicFlag.Borel

Borel subgroups of Sp₂ₘ #

Over an algebraically closed field, every reduced, connected, solvable closed subgroup of Sp₂ₘ is contained in a conjugate, by a rational point of Sp₂ₘ, of the stabilizer of the standard complete isotropic flag. In Hopf coordinates containment of closed subgroups is reversed, so the conclusion reads (definingHopfIdeal k m).conjugate g ≤ I.

The proof restricts the standard representation k^(2m) to the subgroup. The standard alternating form is invariant, so the subgroup preserves a Lagrangian subspace L (LinearMap.BilinForm.IsAlt.exists_subcomodule_eq_orthogonal_of_isSolvable), and the Lie--Kolchin theorem gives a basis of L in which the subgroup acts by upper-triangular matrices. That basis extends to a symplectic basis of k^(2m) (LinearMap.BilinForm.IsAlt.exists_basis_toMatrix_eq_J_inl_eq). In the extended basis the generic point of the subgroup has upper-triangular upper-left block and vanishing lower-left block, and a symplectic matrix of this shape preserves the whole standard isotropic flag (TauCeti.GLSymplecticFin.IsotropicFlag.mem_matrixSubgroup_iff_castAdd). The change of basis matrix is symplectic, so it is a rational point of Sp₂ₘ.

The flag stabilizer is smooth, geometrically connected, and has solvable geometric points, so it is a Borel candidate. Combined with the containment above, it is a Borel subgroup, the Borel subgroups of Sp₂ₘ over an algebraically closed field are exactly its conjugates, and any two of them are conjugate. Its defining ideal commutes with base change, so it is a Borel subgroup of Sp₂ₘ over every commutative ring, and in particular over every field. All of this holds in every characteristic, including two.

Main declarations #

References #

source
theorem TauCeti.Symplectic.IsotropicFlag.exists_map_inv_mul_mul_map_mem_matrixSubgroup {k : Type u} [Field k] {m : ℕ} {Q : Type v} [CommRing Q] [HopfAlgebra k Q] [IsAlgClosed k] [Algebra.FiniteType k Q] [IsReduced Q] (hconn : geometricallyConnectedCommHopfAlgProperty k ↧Q) (hsolv : geometricallySolvablePointsCommHopfAlgProperty k ↧Q) (π : ↑(Symplectic.coordinateHopfAlgebra k m) →ₐc[k] Q) :
∃ (P : ↥(GLSymplecticFin m k)), (GLSymplecticFin.map m k (algebraMap k Q)) P⁻¹ * (Symplectic.pointsMulEquiv k m) (WithConv.toConv ↑π) * (GLSymplecticFin.map m k (algebraMap k Q)) P ∈ GLSymplecticFin.IsotropicFlag.matrixSubgroup m

Lie--Kolchin for Sp₂ₘ-valued points.

Let Q be the coordinate algebra of a reduced, geometrically connected, geometrically solvable affine group of finite type over an algebraically closed field k. For every bialgebra morphism π : O(Sp₂ₘ) → Q some rational symplectic matrix P conjugates the Q-valued point π into the stabilizer of the standard complete isotropic flag. The columns of P form a symplectic basis whose isotropic half is a Lie--Kolchin basis of an invariant Lagrangian subspace.

source
theorem TauCeti.Symplectic.IsotropicFlag.exists_conjugate_definingHopfIdeal_le {k : Type u} [Field k] {m : ℕ} [IsAlgClosed k] (I : HopfIdeal k ↑(Symplectic.coordinateHopfAlgebra k m)) [IsReduced ↑((Symplectic.coordinateHopfAlgebra k m).quotient I)] (hconn : geometricallyConnectedCommHopfAlgProperty k ((Symplectic.coordinateHopfAlgebra k m).quotient I)) (hsolv : geometricallySolvablePointsCommHopfAlgProperty k ((Symplectic.coordinateHopfAlgebra k m).quotient I)) :
∃ (g : WithConv (↑(Symplectic.coordinateHopfAlgebra k m) →ₐ[k] k)), (definingHopfIdeal k m).conjugate g ≤ I

Every reduced, connected, solvable closed subgroup of Sp₂ₘ is contained in a conjugate of the stabilizer of the standard complete isotropic flag, over an algebraically closed field. The inequality of Hopf ideals reverses subgroup containment.

source
theorem TauCeti.Symplectic.IsotropicFlag.isBorelCandidate_definingHopfIdeal (k : Type u) [Field k] (m : ℕ) :
HopfIdeal.IsBorelCandidate k (FiniteTypeCommHopfAlgCat.of k ↑(Symplectic.coordinateHopfAlgebra k m)) (definingHopfIdeal k m)

The stabilizer of the standard complete isotropic flag in Sp₂ₘ is a Borel candidate over every field: it is smooth, geometrically connected, and geometrically solvable.

source
theorem TauCeti.Symplectic.IsotropicFlag.isBorelOverAlgClosed_definingHopfIdeal (k : Type u) [Field k] (m : ℕ) [IsAlgClosed k] :
HopfIdeal.IsBorelOverAlgClosed k (FiniteTypeCommHopfAlgCat.of k ↑(Symplectic.coordinateHopfAlgebra k m)) (definingHopfIdeal k m)

The stabilizer of the standard complete isotropic flag is a Borel subgroup of Sp₂ₘ over an algebraically closed field: it is maximal among smooth, connected, solvable closed subgroups.

source
theorem TauCeti.Symplectic.IsotropicFlag.isBorelOverAlgClosed_iff_exists_eq_conjugate {k : Type u} [Field k] {m : ℕ} [IsAlgClosed k] (I : HopfIdeal k ↑(Symplectic.coordinateHopfAlgebra k m)) :
HopfIdeal.IsBorelOverAlgClosed k (FiniteTypeCommHopfAlgCat.of k ↑(Symplectic.coordinateHopfAlgebra k m)) I ↔ ∃ (g : WithConv (↑(Symplectic.coordinateHopfAlgebra k m) →ₐ[k] k)), I = (definingHopfIdeal k m).conjugate g

The Borel subgroups of Sp₂ₘ over an algebraically closed field are exactly the conjugates of the stabilizer of the standard complete isotropic flag. The equality is an equality of defining Hopf ideals, hence of closed subgroup schemes, rather than only of their rational points.

source
theorem TauCeti.Symplectic.IsotropicFlag.exists_conjugate_eq_of_isBorelOverAlgClosed {k : Type u} [Field k] {m : ℕ} [IsAlgClosed k] {I J : HopfIdeal k ↑(Symplectic.coordinateHopfAlgebra k m)} (hI : HopfIdeal.IsBorelOverAlgClosed k (FiniteTypeCommHopfAlgCat.of k ↑(Symplectic.coordinateHopfAlgebra k m)) I) (hJ : HopfIdeal.IsBorelOverAlgClosed k (FiniteTypeCommHopfAlgCat.of k ↑(Symplectic.coordinateHopfAlgebra k m)) J) :
∃ (g : WithConv (↑(Symplectic.coordinateHopfAlgebra k m) →ₐ[k] k)), I.conjugate g = J

Any two Borel subgroups of Sp₂ₘ over an algebraically closed field are conjugate by a rational point of Sp₂ₘ.

source
theorem TauCeti.Symplectic.IsotropicFlag.isBorelOver_definingHopfIdeal (R : Type u) [CommRing R] (m : ℕ) :
HopfIdeal.IsBorelOver R (Symplectic.coordinateHopfAlgebra R m) (definingHopfIdeal R m)

The stabilizer of the standard complete isotropic flag is a Borel subgroup of Sp₂ₘ over every commutative ring: it is smooth over the base, and on every geometric fiber it is the flag stabilizer, a Borel subgroup.

source
theorem TauCeti.Symplectic.IsotropicFlag.isBorel_definingHopfIdeal (k : Type u) [Field k] (m : ℕ) :
HopfIdeal.IsBorel k (Symplectic.coordinateHopfAlgebra k m) (definingHopfIdeal k m)

The stabilizer of the standard complete isotropic flag is a Borel subgroup of Sp₂ₘ over every field. Its base change to an algebraic closure is smooth, connected, solvable, and maximal among closed subgroups with those properties.