Documentation

TauCeti.LinearAlgebra.Matrix.GeneralLinearGroup.Symplectic.Weyl

Weyl elements in the standard symplectic group #

For distinct coordinate indices i and j, this file constructs the standard representative

n_{i,j} = x_{e_i-e_j}(1) x_{e_j-e_i}(-1) x_{e_i-e_j}(1)

of the Weyl reflection exchanging i and j. It also constructs the long-root representative n_{2e_i}, which exchanges the two symplectic coordinates belonging to i. Conjugation by these representatives transports the root subgroups and acts on the paired diagonal torus by the corresponding type-C_m reflections. These identities work over an arbitrary commutative ring, so no division or characteristic restriction is needed.

The short-root representatives permute torus coordinates, while the long-root representatives invert individual coordinates. Together these give the permutation and sign-change generators of the signed permutation group, the Weyl group of the standard symplectic torus.

Main definitions and results #

References #

Both the short-root and the long-root representatives follow the Chevalley Weyl-word construction n_α = x_α(1) x_{-α}(-1) x_α(1) of these references.

source
def TauCeti.GLSymplecticFin.differenceShortRootWeylElement {R : Type u} [CommRing R] {m : ℕ} {i j : Fin m} (hij : i ≠ j) :
↥(GLSymplecticFin m R)

The standard representative of the Weyl reflection in the short root e_i-e_j: x_{e_i-e_j}(1) x_{e_j-e_i}(-1) x_{e_i-e_j}(1).

Equations
  • One or more equations did not get rendered due to their size.
Instances For
    source
    theorem TauCeti.GLSymplecticFin.differenceShortRootWeylElement_mem {R : Type u} [CommRing R] {m : ℕ} {i j : Fin m} (H : Subgroup ↥(GLSymplecticFin m R)) (hij : i ≠ j) (hforward : differenceShortRootUnit hij 1 ∈ H) (hbackward : differenceShortRootUnit ⋯ (-1) ∈ H) :
    differenceShortRootWeylElement hij ∈ H

    A subgroup containing the two difference-root elements forming a Weyl word contains the corresponding Weyl reflection representative.

    source
    @[simp]
    theorem TauCeti.GLSymplecticFin.coe_differenceShortRootWeylElement {R : Type u} [CommRing R] {m : ℕ} {i j : Fin m} (hij : i ≠ j) :
    ↑(differenceShortRootWeylElement hij) = transvectionWeylElement ⋯ * (transvectionWeylElement ⋯)⁻¹

    In sum coordinates the short-root Weyl representative is the product of the type-A Weyl representative on the first block and the inverse of the one on the second block.

    source
    @[simp]
    theorem TauCeti.GLSymplecticFin.differenceShortRootWeylElement_inv {R : Type u} [CommRing R] {m : ℕ} {i j : Fin m} (hij : i ≠ j) :
    (differenceShortRootWeylElement hij)⁻¹ = differenceShortRootWeylElement ⋯

    The inverse of the Weyl representative for e_i-e_j is the representative for the opposite root e_j-e_i.

    source
    @[simp]
    theorem TauCeti.GLSymplecticFin.differenceShortRootWeylElement_mul_differenceShortRootUnit_mul_inv {R : Type u} [CommRing R] {m : ℕ} {i j : Fin m} (hij : i ≠ j) (c : R) :
    differenceShortRootWeylElement hij * differenceShortRootUnit hij c * differenceShortRootWeylElement ⋯ = differenceShortRootUnit ⋯ (-c)

    Conjugation by the Weyl representative for e_i-e_j sends its short-root subgroup to the opposite short-root subgroup and negates the parameter.

    source
    @[simp]
    theorem TauCeti.GLSymplecticFin.differenceShortRootWeylElement_mul_positiveLongRootTransvectionUnit_mul_inv {R : Type u} [CommRing R] {m : ℕ} {i j : Fin m} (hij : i ≠ j) (c : R) :
    differenceShortRootWeylElement hij * positiveLongRootTransvectionUnit j c * differenceShortRootWeylElement ⋯ = positiveLongRootTransvectionUnit i c

    A short-root Weyl element transports positive long roots. Conjugation by the reflection representative for e_i-e_j sends x_{2e_j}(c) to x_{2e_i}(c), with no change of parameter.

    source
    @[simp]
    theorem TauCeti.GLSymplecticFin.differenceShortRootWeylElement_mul_negativeLongRootTransvectionUnit_mul_inv {R : Type u} [CommRing R] {m : ℕ} {i j : Fin m} (hij : i ≠ j) (c : R) :
    differenceShortRootWeylElement hij * negativeLongRootTransvectionUnit j c * differenceShortRootWeylElement ⋯ = negativeLongRootTransvectionUnit i c

    A short-root Weyl element transports negative long roots. Conjugation by the reflection representative for e_i-e_j sends x_{-2e_j}(c) to x_{-2e_i}(c), with no change of parameter.

    source
    @[simp]
    theorem TauCeti.GLSymplecticFin.map_differenceShortRootWeylElement {R : Type u} [CommRing R] {m : ℕ} {i j : Fin m} {S : Type v} [CommRing S] (f : R →+* S) (hij : i ≠ j) :
    (map m R f) (differenceShortRootWeylElement hij) = differenceShortRootWeylElement hij

    Applying a ring homomorphism entrywise to a short-root Weyl element gives the corresponding Weyl element over the target ring.

    source
    @[simp]
    theorem TauCeti.GLSymplecticFin.differenceShortRootWeylElement_mul_diagonal_mul_inv {R : Type u} [CommRing R] {m : ℕ} {i j : Fin m} (hij : i ≠ j) (t : Fin m → Rˣ) :
    differenceShortRootWeylElement hij * diagonal t * differenceShortRootWeylElement ⋯ = diagonal (t ∘ ⇑(Equiv.swap i j))

    A short-root Weyl element permutes torus coordinates. Conjugation by the reflection representative for e_i-e_j exchanges the i-th and j-th coordinates of the paired diagonal torus.

    source
    theorem TauCeti.GLSymplecticFin.differenceShortRootWeylElement_mem_normalizer_diagonalTorus {R : Type u} [CommRing R] {m : ℕ} {i j : Fin m} (hij : i ≠ j) :
    differenceShortRootWeylElement hij ∈ Subgroup.normalizer ↑(diagonalTorus R m)

    The short-root Weyl representative normalizes the paired diagonal torus.

    Long-root reflections #

    source
    def TauCeti.GLSymplecticFin.positiveLongRootWeylElement {R : Type u} [CommRing R] {m : ℕ} (i : Fin m) :
    ↥(GLSymplecticFin m R)

    The standard representative of the reflection in the long root 2e_i: x_{2e_i}(1) x_{-2e_i}(-1) x_{2e_i}(1).

    Equations
    • One or more equations did not get rendered due to their size.
    Instances For
      source
      def TauCeti.GLSymplecticFin.negativeLongRootWeylElement {R : Type u} [CommRing R] {m : ℕ} (i : Fin m) :
      ↥(GLSymplecticFin m R)

      The standard representative of the reflection in the opposite long root -2e_i: x_{-2e_i}(1) x_{2e_i}(-1) x_{-2e_i}(1).

      Equations
      • One or more equations did not get rendered due to their size.
      Instances For
        source
        theorem TauCeti.GLSymplecticFin.positiveLongRootWeylElement_mem {R : Type u} [CommRing R] {m : ℕ} (H : Subgroup ↥(GLSymplecticFin m R)) (i : Fin m) (hpositive : positiveLongRootTransvectionUnit i 1 ∈ H) (hnegative : negativeLongRootTransvectionUnit i (-1) ∈ H) :
        positiveLongRootWeylElement i ∈ H

        A subgroup containing the two opposite long-root elements in the Weyl word contains the positive long-root Weyl representative.

        source
        theorem TauCeti.GLSymplecticFin.negativeLongRootWeylElement_mem {R : Type u} [CommRing R] {m : ℕ} (H : Subgroup ↥(GLSymplecticFin m R)) (i : Fin m) (hnegative : negativeLongRootTransvectionUnit i 1 ∈ H) (hpositive : positiveLongRootTransvectionUnit i (-1) ∈ H) :
        negativeLongRootWeylElement i ∈ H

        A subgroup containing the two opposite long-root elements in the Weyl word contains the negative long-root Weyl representative.

        source
        @[simp]
        theorem TauCeti.GLSymplecticFin.coe_positiveLongRootWeylElement {R : Type u} [CommRing R] {m : ℕ} (i : Fin m) :
        ↑(positiveLongRootWeylElement i) = transvectionWeylElement ⋯

        The matrix underlying the positive long-root Weyl representative is the elementary Weyl matrix exchanging the two symplectic coordinates belonging to i.

        source
        @[simp]
        theorem TauCeti.GLSymplecticFin.coe_negativeLongRootWeylElement {R : Type u} [CommRing R] {m : ℕ} (i : Fin m) :
        ↑(negativeLongRootWeylElement i) = transvectionWeylElement ⋯

        The matrix underlying the negative long-root Weyl representative is the elementary Weyl matrix for the opposite ordered pair of symplectic coordinates.

        source
        @[simp]
        theorem TauCeti.GLSymplecticFin.positiveLongRootWeylElement_inv {R : Type u} [CommRing R] {m : ℕ} (i : Fin m) :
        (positiveLongRootWeylElement i)⁻¹ = negativeLongRootWeylElement i

        The representative for the opposite long root is the inverse of the positive long-root representative.

        source
        @[simp]
        theorem TauCeti.GLSymplecticFin.negativeLongRootWeylElement_inv {R : Type u} [CommRing R] {m : ℕ} (i : Fin m) :
        (negativeLongRootWeylElement i)⁻¹ = positiveLongRootWeylElement i

        The inverse of the negative long-root representative is the positive long-root representative.

        source
        @[simp]
        theorem TauCeti.GLSymplecticFin.positiveLongRootWeylElement_mul_positiveLongRootTransvectionUnit_mul_inv {R : Type u} [CommRing R] {m : ℕ} (i : Fin m) (c : R) :
        positiveLongRootWeylElement i * positiveLongRootTransvectionUnit i c * negativeLongRootWeylElement i = negativeLongRootTransvectionUnit i (-c)

        Conjugation by the long-root Weyl representative exchanges the positive and negative long root subgroups and negates the parameter.

        source
        @[simp]
        theorem TauCeti.GLSymplecticFin.positiveLongRootWeylElement_mul_negativeLongRootTransvectionUnit_mul_inv {R : Type u} [CommRing R] {m : ℕ} (i : Fin m) (c : R) :
        positiveLongRootWeylElement i * negativeLongRootTransvectionUnit i c * negativeLongRootWeylElement i = positiveLongRootTransvectionUnit i (-c)

        Conjugation by the long-root Weyl representative exchanges the negative and positive long root subgroups and negates the parameter.

        source
        @[simp]
        theorem TauCeti.GLSymplecticFin.positiveLongRootWeylElement_mul_diagonal_mul_inv {R : Type u} [CommRing R] {m : ℕ} (i : Fin m) (t : Fin m → Rˣ) :
        positiveLongRootWeylElement i * diagonal t * negativeLongRootWeylElement i = diagonal (Function.update t i (t i)⁻¹)

        Conjugation by the long-root Weyl representative inverts the corresponding coordinate of the paired diagonal torus and fixes every other coordinate.

        source
        @[simp]
        theorem TauCeti.GLSymplecticFin.negativeLongRootWeylElement_mul_diagonal_mul_inv {R : Type u} [CommRing R] {m : ℕ} (i : Fin m) (t : Fin m → Rˣ) :
        negativeLongRootWeylElement i * diagonal t * positiveLongRootWeylElement i = diagonal (Function.update t i (t i)⁻¹)

        Conjugation by the opposite long-root representative has the same reflection action on the paired diagonal torus.

        source
        theorem TauCeti.GLSymplecticFin.positiveLongRootWeylElement_mem_normalizer_diagonalTorus {R : Type u} [CommRing R] {m : ℕ} (i : Fin m) :
        positiveLongRootWeylElement i ∈ Subgroup.normalizer ↑(diagonalTorus R m)

        The long-root Weyl representative normalizes the paired diagonal torus.

        source
        theorem TauCeti.GLSymplecticFin.negativeLongRootWeylElement_mem_normalizer_diagonalTorus {R : Type u} [CommRing R] {m : ℕ} (i : Fin m) :
        negativeLongRootWeylElement i ∈ Subgroup.normalizer ↑(diagonalTorus R m)

        The opposite long-root Weyl representative normalizes the paired diagonal torus.

        source
        @[simp]
        theorem TauCeti.GLSymplecticFin.map_positiveLongRootWeylElement {R : Type u} [CommRing R] {m : ℕ} {S : Type v} [CommRing S] (f : R →+* S) (i : Fin m) :
        (map m R f) (positiveLongRootWeylElement i) = positiveLongRootWeylElement i

        Applying a ring homomorphism entrywise to a long-root Weyl representative gives the corresponding representative over the target ring.

        source
        @[simp]
        theorem TauCeti.GLSymplecticFin.map_negativeLongRootWeylElement {R : Type u} [CommRing R] {m : ℕ} {S : Type v} [CommRing S] (f : R →+* S) (i : Fin m) :
        (map m R f) (negativeLongRootWeylElement i) = negativeLongRootWeylElement i

        Applying a ring homomorphism entrywise to a negative long-root Weyl representative gives the corresponding representative over the target ring.