Documentation

TauCeti.RepresentationTheory.SU2.Weyl.Basic

The Weyl group of SU(2) #

The Weyl group of a compact group G with maximal torus T is the quotient N_G(T) / T of the normalizer of the torus by the torus. This file computes it for G = SU(2) and the diagonal maximal torus T of TauCeti/RepresentationTheory/SU2/Basic.lean: it is a group of order two, generated by the class of the quarter turn

w = !![0, -1; 1, 0],

whose nontrivial element acts on T by inversion, diag (z, z⁻¹) ↦ diag (z⁻¹, z).

The computation runs through the two rigidity facts about the maximal torus proved in TauCeti/RepresentationTheory/SU2/Basic.lean. First, a single torus element diag (z, z⁻¹) with z² ≠ 1 already has centralizer T (TauCeti.SU2.centralizer_torusHom). Second, conjugating a torus element back into the torus can only return it or its inverse (TauCeti.SU2.eq_or_eq_inv_of_conj_torusHom). Together they say that an element normalizing T either centralizes it, and so lies in T, or acts on it as w does, and so lies in w T.

Conjugation by N(T) therefore descends to an action of the Weyl group on T, read here through the circle parametrisation z ↦ diag (z, z⁻¹) as a homomorphism TauCeti.SU2.weylAut : W → MulAut Circle. It is faithful, and its nontrivial element is inversion. That is the sense in which the characters of SU(2) are W-invariant functions on T; the evenness of characters that this yields is proved in TauCeti/RepresentationTheory/SU2/Character.lean.

Main definitions #

Main results #

References #

This is the Weyl group of the engine case of TauCetiRoadmap/RepresentationTheory/CompactGroups/README.md, "Engine case: SU(2) and the maximal torus", which needs the W-invariant (even) functions on T to be the class functions of SU(2); it is the SU(2) instance of weylGroup T = N_G(T) / T from TauCetiRoadmap/RepresentationTheory/LieGroups/README.md, Layer 6.

Inside Tau Ceti, the inversion action of the Weyl reflection on the torus was first formalized by TauCeti.SU2.isConj_inv_of_mem_torus in TauCeti/RepresentationTheory/SU2/TorusConjugacy.lean, which conjugated a torus element to its inverse by the sign-opposite quarter turn !![0, 1; -1, 0] = w⁻¹. That is the same construction as TauCeti.SU2.weylElement_conj_torusHom here, in existential form: it asserts IsConj g g⁻¹ and so neither names a conjugating element nor records that the conjugator normalizes T, which is what the computation of N(T) and of the quotient needs. The quarter turn is therefore named here, and isConj_inv_of_mem_torus is now derived from TauCeti.SU2.weylElement_conj_torusHom rather than repeating the matrix computation; the dependency runs that way round because this file needs only SU2/Basic.lean, whereas TorusConjugacy rests on the spectral theorem.

The quarter turn #

source
def TauCeti.SU2.weylMatrix :
Matrix (Fin 2) (Fin 2) ℂ

The quarter turn !![0, -1; 1, 0], the matrix that represents the nontrivial element of the Weyl group of SU(2).

Equations
Instances For
    source
    theorem TauCeti.SU2.weylMatrix_mem :
    weylMatrix ∈ Matrix.specialUnitaryGroup (Fin 2) ℂ

    The quarter turn is unitary with determinant 1.

    source
    def TauCeti.SU2.weylElement :
    SU2

    The quarter turn as an element of SU(2). Conjugation by it inverts the maximal torus, and its class generates the Weyl group.

    Equations
    Instances For
      source
      @[simp]
      theorem TauCeti.SU2.coe_weylElement :
      ↑weylElement = weylMatrix

      The matrix underlying the quarter turn of SU(2).

      source
      theorem TauCeti.SU2.weylElement_notMem_torus :
      weylElement ∉ torus

      The quarter turn is not diagonal, so it does not lie in the maximal torus.

      Conjugation by the quarter turn inverts the torus #

      source
      theorem TauCeti.SU2.weylMatrix_mul_torusMatrix (z : Circle) :
      weylMatrix * torusMatrix z = torusMatrix z⁻¹ * weylMatrix

      The matrix form of TauCeti.SU2.weylElement_mul_torusHom: the quarter turn intertwines diag (z, z⁻¹) with diag (z⁻¹, z).

      source
      theorem TauCeti.SU2.weylElement_mul_torusHom (z : Circle) :
      weylElement * torusHom z = torusHom z⁻¹ * weylElement

      The quarter turn intertwines a torus element with its inverse.

      source
      @[simp]
      theorem TauCeti.SU2.weylElement_conj_torusHom (z : Circle) :
      weylElement * torusHom z * weylElement⁻¹ = torusHom z⁻¹

      Conjugation by the quarter turn inverts the maximal torus. This single identity carries the whole Weyl-group action of SU(2): w diag (z, z⁻¹) w⁻¹ = diag (z⁻¹, z).

      source
      theorem TauCeti.SU2.weylElement_mem_normalizer :
      weylElement ∈ Subgroup.normalizer ↑torus

      The quarter turn normalizes the maximal torus.

      The normalizer of the maximal torus #

      source
      theorem TauCeti.SU2.mem_normalizer_torus_iff {g : SU2} :
      g ∈ Subgroup.normalizer ↑torus ↔ g ∈ torus ∨ weylElement⁻¹ * g ∈ torus

      The normalizer of the maximal torus, elementwise. An element of SU(2) normalizes the diagonal torus exactly when it is diagonal, or is the quarter turn times a diagonal element.

      source
      theorem TauCeti.SU2.normalizer_torus :
      Subgroup.normalizer ↑torus = torus ⊔ Subgroup.zpowers weylElement

      The normalizer of the maximal torus of SU(2) is generated by the torus together with the quarter turn.

      The Weyl group #

      source
      @[reducible, inline]
      abbrev TauCeti.SU2.weylGroup :
      Type

      The Weyl group of SU(2), N(T) / T for the diagonal maximal torus T. This is Subgroup.normalizerQuotient, the general normalizer quotient of TauCeti/Algebra/Group/NormalizerQuotient/Basic.lean, at the maximal torus.

      Equations
      Instances For
        source
        noncomputable def TauCeti.SU2.weylNormalizerElement :
        ↥(Subgroup.normalizer ↑torus)

        The quarter turn, as an element of the normalizer of the maximal torus.

        Equations
        Instances For
          source
          @[simp]
          theorem TauCeti.SU2.coe_weylNormalizerElement :
          ↑weylNormalizerElement = weylElement

          The element of SU(2) underlying TauCeti.SU2.weylNormalizerElement.

          source
          noncomputable def TauCeti.SU2.weylClass :
          weylGroup

          The class of the quarter turn in the Weyl group of SU(2); it is the nontrivial element.

          Equations
          Instances For
            source
            theorem TauCeti.SU2.weylClass_ne_one :
            weylClass ≠ 1

            The class of the quarter turn is nontrivial, because the quarter turn is not diagonal.

            source
            @[simp]
            theorem TauCeti.SU2.weylClass_sq :
            weylClass ^ 2 = 1

            The nontrivial element of the Weyl group of SU(2) has order two, because the square of the quarter turn is -1, which is diagonal and so lies in the maximal torus.

            source
            @[simp]
            theorem TauCeti.SU2.weylClass_inv :
            weylClass⁻¹ = weylClass

            The nontrivial element of the Weyl group of SU(2) is its own inverse.

            source
            theorem TauCeti.SU2.eq_one_or_eq_weylClass (q : weylGroup) :
            q = 1 ∨ q = weylClass

            Every element of the Weyl group of SU(2) is trivial or the class of the quarter turn.

            source
            theorem TauCeti.SU2.card_weylGroup :
            Nat.card weylGroup = 2

            The Weyl group of SU(2) has order two.

            source
            instance TauCeti.SU2.instFiniteWeylGroup :
            Finite weylGroup

            The Weyl group of SU(2) is finite, having order two.

            source
            theorem TauCeti.SU2.conj_torusHom_of_mem_normalizer {n : SU2} (hn : n ∈ Subgroup.normalizer ↑torus) (z : Circle) :
            n * torusHom z * n⁻¹ = torusHom z ∨ n * torusHom z * n⁻¹ = torusHom z⁻¹

            The Weyl group acts on the maximal torus by z ↦ z^{±1}. An element normalizing T either centralizes it or inverts it, according to which of the two classes of N(T) / T it lies in.

            The action of the Weyl group on the maximal torus #

            source
            noncomputable def TauCeti.SU2.normalizerAut :
            ↥(Subgroup.normalizer ↑torus) →* MulAut Circle

            Conjugation of the maximal torus by an element of its normalizer, read through the circle parametrisation z ↦ diag (z, z⁻¹): this is Mathlib's Subgroup.normalizerMonoidHom at the maximal torus, transported along TauCeti.SU2.torusContinuousMulEquiv. So normalizerAut n is the automorphism of Circle with diag (normalizerAut n z, (normalizerAut n z)⁻¹) = n diag (z, z⁻¹) n⁻¹, which is TauCeti.SU2.torusHom_normalizerAut.

            Equations
            Instances For
              source
              theorem TauCeti.SU2.torusHom_normalizerAut (n : ↥(Subgroup.normalizer ↑torus)) (z : Circle) :
              torusHom ((normalizerAut n) z) = ↑n * torusHom z * (↑n)⁻¹

              TauCeti.SU2.normalizerAut is conjugation in SU(2), read on the circle parameter.

              source
              theorem TauCeti.SU2.normalizerAut_ker :
              normalizerAut.ker = torus.subgroupOf (Subgroup.normalizer ↑torus)

              The conjugation action of N(T) on the maximal torus has kernel exactly T. This is Mathlib's Subgroup.normalizerMonoidHom_ker, whose kernel is the centralizer of T, together with TauCeti.SU2.centralizer_torus, which says that the centralizer of T is T. It supplies both halves of the Weyl-group action: T acts trivially, so conjugation descends to N(T) / T, and nothing else does, so the descended action is faithful.

              source
              theorem TauCeti.SU2.normalizerAut_eq_one_iff (n : ↥(Subgroup.normalizer ↑torus)) :
              normalizerAut n = 1 ↔ ↑n ∈ torus

              An element of N(T) acts trivially on the maximal torus exactly when it lies in T.

              source
              noncomputable def TauCeti.SU2.weylAut :
              weylGroup →* MulAut Circle

              The action of the Weyl group of SU(2) on the maximal torus. Conjugation by N(T) descends to the quotient N(T) / T, because T is commutative and so acts trivially on itself; the automorphism of Circle produced here is the automorphism of T it names under TauCeti.SU2.torusContinuousMulEquiv.

              Equations
              Instances For
                source
                theorem TauCeti.SU2.torusHom_weylAut_mk (n : ↥(Subgroup.normalizer ↑torus)) (z : Circle) :
                torusHom ((weylAut (torus.normalizerQuotientMk n)) z) = ↑n * torusHom z * (↑n)⁻¹

                The Weyl-group action of the class of n ∈ N(T), unfolded to conjugation by n in SU(2). The action is that of any representative, being independent of the choice of representative by construction.

                source
                @[simp]
                theorem TauCeti.SU2.weylAut_weylClass :
                weylAut weylClass = MulEquiv.inv Circle

                The nontrivial element of the Weyl group of SU(2) acts on the maximal torus by inversion.

                source
                theorem TauCeti.SU2.weylAut_injective :
                Function.Injective ⇑weylAut

                The Weyl group of SU(2) acts faithfully on the maximal torus, because the kernel of the conjugation action of N(T) is exactly T.