Documentation

TauCeti.Algebra.Lie.F4.ShortRoot.Represented.Chevalley

The represented F4 Chevalley algebra in characteristic two #

The integral short-root matrices give a representation of the type-F₄ Serre algebra after base change to any commutative ring. This file constructs its image as a Lie subalgebra of the algebra of 26-by-26 matrices. Over ZMod 2 it also isolates the Lie ideal generated by the raising and lowering matrices at the two short simple roots.

An explicit description of this ideal and its quotient is used to construct the characteristic-two special isogeny.

Main definitions #

Main results #

References #

Base change of the represented generators #

source
noncomputable def TauCeti.F4ShortRoot.cartanMatrixBaseChange (R : Type u_1) [CommRing R] (i : Fin 4) :
Matrix (Fin 26) (Fin 26) R

The integral Cartan generator, with its entries mapped to R.

Equations
Instances For
    source
    noncomputable def TauCeti.F4ShortRoot.raisingMatrixBaseChange (R : Type u_1) [CommRing R] (i : Fin 4) :
    Matrix (Fin 26) (Fin 26) R

    The integral raising generator, with its entries mapped to R.

    Equations
    Instances For
      source
      noncomputable def TauCeti.F4ShortRoot.loweringMatrixBaseChange (R : Type u_1) [CommRing R] (i : Fin 4) :
      Matrix (Fin 26) (Fin 26) R

      The integral lowering generator, with its entries mapped to R.

      Equations
      Instances For
        source
        @[simp]
        theorem TauCeti.F4ShortRoot.cartanMatrixBaseChange_apply (R : Type u_1) [CommRing R] (i : Fin 4) (a b : Fin 26) :
        cartanMatrixBaseChange R i a b = ↑(cartanMatrix i a b)
        source
        @[simp]
        theorem TauCeti.F4ShortRoot.raisingMatrixBaseChange_apply (R : Type u_1) [CommRing R] (i : Fin 4) (a b : Fin 26) :
        raisingMatrixBaseChange R i a b = ↑(raisingMatrix i a b)
        source
        @[simp]
        theorem TauCeti.F4ShortRoot.loweringMatrixBaseChange_apply (R : Type u_1) [CommRing R] (i : Fin 4) (a b : Fin 26) :
        loweringMatrixBaseChange R i a b = ↑(loweringMatrix i a b)
        source
        theorem TauCeti.F4ShortRoot.isSerreSystemBaseChange (R : Type u_1) [CommRing R] :
        IsSerreSystem R CartanMatrix.F₄.transpose (cartanMatrixBaseChange R) (raisingMatrixBaseChange R) (loweringMatrixBaseChange R)

        The base-changed matrices satisfy the type-F₄ Chevalley--Serre relations.

        source
        noncomputable def TauCeti.F4ShortRoot.serreRepresentationBaseChange (R : Type u_1) [CommRing R] :
        Matrix.ToLieAlgebra R CartanMatrix.F₄.transpose →ₗ⁅R⁆ Matrix (Fin 26) (Fin 26) R

        The twenty-six-dimensional representation of the type-F₄ Serre algebra over R obtained by base change from the integral generator matrices.

        Equations
        Instances For
          source
          @[simp]
          theorem TauCeti.F4ShortRoot.serreRepresentationBaseChange_serreH (R : Type u_1) [CommRing R] (i : Fin 4) :
          (serreRepresentationBaseChange R) (serreH R CartanMatrix.F₄.transpose i) = cartanMatrixBaseChange R i
          source
          @[simp]
          theorem TauCeti.F4ShortRoot.serreRepresentationBaseChange_serreE (R : Type u_1) [CommRing R] (i : Fin 4) :
          (serreRepresentationBaseChange R) (serreE R CartanMatrix.F₄.transpose i) = raisingMatrixBaseChange R i
          source
          @[simp]
          theorem TauCeti.F4ShortRoot.serreRepresentationBaseChange_serreF (R : Type u_1) [CommRing R] (i : Fin 4) :
          (serreRepresentationBaseChange R) (serreF R CartanMatrix.F₄.transpose i) = loweringMatrixBaseChange R i

          The represented Chevalley algebra #

          source
          noncomputable def TauCeti.F4ShortRoot.representedChevalleyAlgebra (R : Type u_1) [CommRing R] :
          LieSubalgebra R (Matrix (Fin 26) (Fin 26) R)

          The represented type-F₄ Chevalley algebra: the image of the base-changed Serre representation in the algebra of 26-by-26 matrices.

          Equations
          Instances For
            source
            theorem TauCeti.F4ShortRoot.representedChevalleyAlgebra_eq_lieSpan (R : Type u_1) [CommRing R] :
            representedChevalleyAlgebra R = LieSubalgebra.lieSpan R (Matrix (Fin 26) (Fin 26) R) (Set.range (raisingMatrixBaseChange R) ∪ Set.range (loweringMatrixBaseChange R))

            The represented Chevalley algebra is generated, as a Lie algebra, by the base-changed raising and lowering matrices. The Cartan matrices need not be included because H_i = ⁅E_i, F_i⁆.

            source
            noncomputable def TauCeti.F4ShortRoot.representedH (R : Type u_1) [CommRing R] (i : Fin 4) :
            ↥(representedChevalleyAlgebra R)

            The represented Cartan generator as an element of the represented Chevalley algebra.

            Equations
            Instances For
              source
              noncomputable def TauCeti.F4ShortRoot.representedE (R : Type u_1) [CommRing R] (i : Fin 4) :
              ↥(representedChevalleyAlgebra R)

              The represented raising generator as an element of the represented Chevalley algebra.

              Equations
              Instances For
                source
                noncomputable def TauCeti.F4ShortRoot.representedF (R : Type u_1) [CommRing R] (i : Fin 4) :
                ↥(representedChevalleyAlgebra R)

                The represented lowering generator as an element of the represented Chevalley algebra.

                Equations
                Instances For
                  source
                  @[simp]
                  theorem TauCeti.F4ShortRoot.coe_representedH (R : Type u_1) [CommRing R] (i : Fin 4) :
                  ↑(representedH R i) = cartanMatrixBaseChange R i
                  source
                  @[simp]
                  theorem TauCeti.F4ShortRoot.coe_representedE (R : Type u_1) [CommRing R] (i : Fin 4) :
                  ↑(representedE R i) = raisingMatrixBaseChange R i
                  source
                  @[simp]
                  theorem TauCeti.F4ShortRoot.coe_representedF (R : Type u_1) [CommRing R] (i : Fin 4) :
                  ↑(representedF R i) = loweringMatrixBaseChange R i
                  source
                  @[simp]
                  theorem TauCeti.F4ShortRoot.lie_representedE_representedF_self (R : Type u_1) [CommRing R] (i : Fin 4) :
                  ⁅representedE R i, representedF R i⁆ = representedH R i

                  The short-root ideal in characteristic two #

                  source
                  noncomputable def TauCeti.F4ShortRoot.shortRootIdeal :
                  LieIdeal (ZMod 2) ↥(representedChevalleyAlgebra (ZMod 2))

                  The characteristic-two short-root ideal, generated by the positive and negative short simple root matrices. The short simple coroots are already forced into it by the Lie bracket.

                  Equations
                  Instances For
                    source
                    theorem TauCeti.F4ShortRoot.shortRootIdeal_le_iff (I : LieIdeal (ZMod 2) ↥(representedChevalleyAlgebra (ZMod 2))) :
                    shortRootIdeal ≤ I ↔ (∀ (i : Fin DynkinType.F4.rank), ¬DynkinType.F4.IsLongSimpleRoot i → representedE (ZMod 2) i ∈ I) ∧ ∀ (i : Fin DynkinType.F4.rank), ¬DynkinType.F4.IsLongSimpleRoot i → representedF (ZMod 2) i ∈ I

                    The universal property of the short-root ideal.

                    source
                    theorem TauCeti.F4ShortRoot.representedE_mem_shortRootIdeal (i : Fin 4) (hi : ¬DynkinType.F4.IsLongSimpleRoot i) :
                    representedE (ZMod 2) i ∈ shortRootIdeal

                    A represented raising matrix at a short simple root belongs to the short-root ideal.

                    source
                    theorem TauCeti.F4ShortRoot.representedF_mem_shortRootIdeal (i : Fin 4) (hi : ¬DynkinType.F4.IsLongSimpleRoot i) :
                    representedF (ZMod 2) i ∈ shortRootIdeal

                    A represented lowering matrix at a short simple root belongs to the short-root ideal.

                    source
                    theorem TauCeti.F4ShortRoot.representedH_mem_shortRootIdeal (i : Fin 4) (hi : ¬DynkinType.F4.IsLongSimpleRoot i) :
                    representedH (ZMod 2) i ∈ shortRootIdeal

                    The represented coroot at a short simple root belongs to the short-root ideal.

                    source
                    theorem TauCeti.F4ShortRoot.shortRootIdeal_ne_bot :
                    shortRootIdeal ≠ ⊥

                    The short-root ideal is nonzero: it contains the nonzero raising matrix at short node 2.