The symplectic isotropic flag matrix subgroup #

The self-dual basis order fixes the isotropic half and reverses its dual half. The subgroup of symplectic matrices upper triangular in this order has an upper-triangular upper-left block, a lower-triangular lower-right block, and a zero lower-left block. It is solvable over every commutative ring, by its inclusion in the upper-triangular general linear group. Its representing Hopf algebra is constructed in TauCeti.Algebra.AlgebraicGroup.Symplectic.IsotropicFlag.Basic.

References #

J. S. Milne, Algebraic Groups (2017), §24.6 (symplectic groups and isotropic flags).

source

def TauCeti.GLSymplecticFin.IsotropicFlag.flagOrder (m : ℕ) :

Equiv.Perm (Fin (m + m))

The basis permutation giving the self-dual flag order: fix the e block and reverse the f block.

Equations

TauCeti.GLSymplecticFin.IsotropicFlag.flagOrder m = (finSumFinEquiv.symm.trans ((Equiv.refl (Fin m)).sumCongr Fin.revPerm)).trans finSumFinEquiv

Instances For

source

@[simp]

theorem TauCeti.GLSymplecticFin.IsotropicFlag.flagOrder_castAdd (m : ℕ) (i : Fin m) :

(flagOrder m) (Fin.castAdd m i) = Fin.castAdd m i

The isotropic half of the basis keeps its standard order.

source

@[simp]

theorem TauCeti.GLSymplecticFin.IsotropicFlag.flagOrder_addNat (m : ℕ) (i : Fin m) :

(flagOrder m) (i.addNat m) = i.rev.addNat m

The dual half of the basis is reversed in the self-dual flag order.

source

theorem TauCeti.GLSymplecticFin.IsotropicFlag.flagOrder_castAdd_lt_castAdd_iff (m : ℕ) (i j : Fin m) :

(flagOrder m) (Fin.castAdd m j) < (flagOrder m) (Fin.castAdd m i) ↔ j < i

Flag order preserves comparisons within the isotropic half.

source

theorem TauCeti.GLSymplecticFin.IsotropicFlag.flagOrder_addNat_lt_addNat_iff (m : ℕ) (i j : Fin m) :

(flagOrder m) (j.addNat m) < (flagOrder m) (i.addNat m) ↔ i < j

Flag order reverses comparisons within the dual half.

source

theorem TauCeti.GLSymplecticFin.IsotropicFlag.flagOrder_castAdd_lt_addNat (m : ℕ) (i j : Fin m) :

(flagOrder m) (Fin.castAdd m j) < (flagOrder m) (i.addNat m)

Every isotropic basis index precedes every dual basis index in flag order.

source

theorem TauCeti.GLSymplecticFin.IsotropicFlag.not_flagOrder_addNat_lt_castAdd (m : ℕ) (i j : Fin m) :

¬(flagOrder m) (j.addNat m) < (flagOrder m) (Fin.castAdd m i)

No dual basis index precedes an isotropic basis index in flag order.

source

@[simp]

theorem TauCeti.GLSymplecticFin.IsotropicFlag.flagOrder_symm (m : ℕ) :

Equiv.symm (flagOrder m) = flagOrder m

The self-dual flag-order permutation is its own inverse.

source

def TauCeti.GLSymplecticFin.IsotropicFlag.matrixSubgroup (m : ℕ) {A : Type u_1} [CommRing A] :

Subgroup ↥(GLSymplecticFin m A)

The subgroup of symplectic matrices that become upper triangular after reindexing by flagOrder m. Its paired-block form is recorded in mem_matrixSubgroup_iff.

Equations

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

Instances For

source

theorem TauCeti.GLSymplecticFin.IsotropicFlag.mem_matrixSubgroup_iff_flagOrder (m : ℕ) {A : Type u_1} [CommRing A] (g : ↥(GLSymplecticFin m A)) :

g ∈ matrixSubgroup m ↔ ∀ (i j : Fin (m + m)), (flagOrder m) j < (flagOrder m) i → ↑↑g i j = 0

Membership in the flag subgroup is entrywise vanishing below the diagonal in flag order.

source

@[simp]

theorem TauCeti.GLSymplecticFin.IsotropicFlag.mem_matrixSubgroup_iff (m : ℕ) {A : Type u_1} [CommRing A] (g : ↥(GLSymplecticFin m A)) :

g ∈ matrixSubgroup m ↔ (∀ (i j : Fin m), j < i → ↑↑g (Fin.castAdd m i) (Fin.castAdd m j) = 0) ∧ (∀ (i j : Fin m), i < j → ↑↑g (i.addNat m) (j.addNat m) = 0) ∧ ∀ (i j : Fin m), ↑↑g (i.addNat m) (Fin.castAdd m j) = 0

In paired coordinates, the flag subgroup consists of matrices whose upper-left block is upper triangular, whose lower-right block is lower triangular, and whose lower-left block vanishes.

source