Documentation

TauCeti.Algebra.Lie.F4.ShortRoot.Represented.Flag.Basic

The represented split flag for modular F4 #

The adjoint action on the modular short-root ideal gives subspaces J = ρ(I) ⊆ M = ρ(L) ⊆ End(I). This file chooses an ambient basis adapted to that flag. The middle block is prescribed: modulo J, it is the special-isogeny-indexed basis of L / I transported through the represented-quotient equivalence. The bases of J and End(I) / M are arbitrary, so no dimensions of J or M need to be computed.

The ambient endomorphism space is then identified with the fixed cotangent dual of GL₂₆, where the existing adjoint comodule acts. Weights 2, 1, and 0 record the three blocks.

source
@[reducible, inline]
noncomputable abbrev TauCeti.DynkinType.f4ShortRootRepresentedIdealRank :
ℕ

The dimension of the represented image of the short-root ideal.

Equations
Instances For
    source
    @[reducible, inline]
    noncomputable abbrev TauCeti.DynkinType.f4ShortRootRepresentedComplementRank :
    ℕ

    The dimension of the quotient of the ambient endomorphism space by the represented range.

    Equations
    Instances For
      source
      noncomputable def TauCeti.DynkinType.f4ShortRootRepresentedIdealBasis :
      Module.Basis (Fin f4ShortRootRepresentedIdealRank) (ZMod 2) ↥f4ShortRootRepresentedIdeal

      An arbitrary basis of the represented image of the short-root ideal.

      Equations
      Instances For
        source
        noncomputable def TauCeti.DynkinType.f4ShortRootRepresentedQuotientBasis :
        Module.Basis (Fin 26) (ZMod 2) (↥(↑f4ShortRootAdjoint).range ⧸ Submodule.map (↑f4ShortRootAdjoint).rangeRestrict f4ShortRootSubspace)

        The prescribed basis of M / J, obtained from the special-isogeny-indexed basis of L / I.

        Equations
        • One or more equations did not get rendered due to their size.
        Instances For
          source
          noncomputable def TauCeti.DynkinType.f4ShortRootRepresentedRangeBasis :
          Module.Basis (Fin (f4ShortRootRepresentedIdealRank + 26)) (ZMod 2) ↥f4ShortRootRepresentedRange

          A basis of the represented range M adapted to J ⊆ M, with prescribed quotient block.

          Equations
          • One or more equations did not get rendered due to their size.
          Instances For
            source
            noncomputable def TauCeti.DynkinType.f4ShortRootRepresentedComplementBasis :
            Module.Basis (Fin f4ShortRootRepresentedComplementRank) (ZMod 2) (Module.End (ZMod 2) ↥f4ShortRootLieIdeal ⧸ f4ShortRootRepresentedRange)

            An arbitrary basis of End(I) / M.

            Equations
            • One or more equations did not get rendered due to their size.
            Instances For
              source
              noncomputable def TauCeti.DynkinType.f4ShortRootEndBasis :
              Module.Basis (Fin (f4ShortRootRepresentedIdealRank + 26 + f4ShortRootRepresentedComplementRank)) (ZMod 2) (Module.End (ZMod 2) ↥f4ShortRootLieIdeal)

              A basis of End(I) adapted to J ⊆ M ⊆ End(I).

              Equations
              • One or more equations did not get rendered due to their size.
              Instances For
                source
                noncomputable def TauCeti.DynkinType.f4ShortRootEndEquivCotangentDual :
                Module.End (ZMod 2) ↥f4ShortRootLieIdeal ≃ₗ[ZMod 2] Module.Dual (ZMod 2) (Bialgebra.CotangentSpace (ZMod 2) ↑(GeneralLinear.coordinateHopfAlgebra (ZMod 2) 26))

                Identify endomorphisms of the based short-root ideal with the cotangent dual of GL₂₆.

                Equations
                • One or more equations did not get rendered due to their size.
                Instances For
                  source
                  @[simp]
                  theorem TauCeti.DynkinType.cotangentDualMatrixEquiv_f4ShortRootEndEquivCotangentDual (T : Module.End (ZMod 2) ↥f4ShortRootLieIdeal) :
                  GeneralLinear.cotangentDualMatrixEquiv (f4ShortRootEndEquivCotangentDual T) = (LinearMap.toMatrix f4ShortRootLieIdealBasis f4ShortRootLieIdealBasis) T

                  Matrix coordinates undo the endomorphism-to-cotangent identification.

                  source
                  noncomputable def TauCeti.DynkinType.f4ShortRootCotangentFlagBasis :
                  Module.Basis (Fin (f4ShortRootRepresentedIdealRank + 26 + f4ShortRootRepresentedComplementRank)) (ZMod 2) (Module.Dual (ZMod 2) (Bialgebra.CotangentSpace (ZMod 2) ↑(GeneralLinear.coordinateHopfAlgebra (ZMod 2) 26)))

                  The cotangent-dual basis carrying the represented flag J ⊆ M ⊆ End(I).

                  Equations
                  Instances For
                    source
                    @[simp]
                    theorem TauCeti.DynkinType.f4ShortRootCotangentFlagBasis_apply (i : Fin (f4ShortRootRepresentedIdealRank + 26 + f4ShortRootRepresentedComplementRank)) :
                    f4ShortRootCotangentFlagBasis i = f4ShortRootEndEquivCotangentDual (f4ShortRootEndBasis i)
                    source
                    noncomputable def TauCeti.DynkinType.f4ShortRootCotangentFlagWeight (i : Fin (f4ShortRootRepresentedIdealRank + 26 + f4ShortRootRepresentedComplementRank)) :
                    ℤ

                    Weights 2, 1, and 0 on the J, M/J, and End(I)/M blocks.

                    Equations
                    • One or more equations did not get rendered due to their size.
                    Instances For
                      source
                      theorem TauCeti.DynkinType.f4ShortRootCotangentFlagWeight_of_ideal (i : Fin (f4ShortRootRepresentedIdealRank + 26 + f4ShortRootRepresentedComplementRank)) (hi : ↑i < f4ShortRootRepresentedIdealRank) :
                      f4ShortRootCotangentFlagWeight i = 2

                      Indices in the represented ideal have weight two.

                      source
                      theorem TauCeti.DynkinType.f4ShortRootCotangentFlagWeight_of_quotient (i : Fin (f4ShortRootRepresentedIdealRank + 26 + f4ShortRootRepresentedComplementRank)) (hi : ¬↑i < f4ShortRootRepresentedIdealRank) (hir : ↑i < f4ShortRootRepresentedIdealRank + 26) :
                      f4ShortRootCotangentFlagWeight i = 1

                      Indices in the represented quotient block have weight one.

                      source
                      theorem TauCeti.DynkinType.f4ShortRootCotangentFlagWeight_of_complement (i : Fin (f4ShortRootRepresentedIdealRank + 26 + f4ShortRootRepresentedComplementRank)) (hi : ¬↑i < f4ShortRootRepresentedIdealRank + 26) :
                      f4ShortRootCotangentFlagWeight i = 0

                      Indices after the represented range have weight zero.

                      source
                      @[simp]
                      theorem TauCeti.DynkinType.f4ShortRootRepresentedRangeBasis_ideal (i : Fin f4ShortRootRepresentedIdealRank) :
                      f4ShortRootRepresentedRangeBasis (Fin.castAdd 26 i) = ↑(f4ShortRootRepresentedIdealBasis i)

                      The first block of the represented-range basis is the represented-ideal basis.

                      source
                      @[simp]
                      theorem TauCeti.DynkinType.f4ShortRootRepresentedRangeBasis_quotient (a : Fin 26) :
                      Submodule.Quotient.mk (f4ShortRootRepresentedRangeBasis (Fin.natAdd f4ShortRootRepresentedIdealRank a)) = ((↑f4ShortRootAdjoint).quotientEquivRangeQuotientMap f4ShortRootSubspace ker_f4ShortRootAdjoint_le_f4ShortRootSubspace) (f4ShortRootQuotientBasis a)

                      The second block of the represented-range basis projects to the modular quotient basis.

                      source
                      @[simp]
                      theorem TauCeti.DynkinType.f4ShortRootEndBasis_range (i : Fin (f4ShortRootRepresentedIdealRank + 26)) :
                      f4ShortRootEndBasis (Fin.castAdd f4ShortRootRepresentedComplementRank i) = ↑(f4ShortRootRepresentedRangeBasis i)

                      The first two blocks of the adapted endomorphism basis equal the represented-range basis.

                      source
                      theorem TauCeti.DynkinType.f4ShortRootCotangentFlagBasis_range (i : Fin (f4ShortRootRepresentedIdealRank + 26)) :
                      f4ShortRootCotangentFlagBasis (Fin.castAdd f4ShortRootRepresentedComplementRank i) = f4ShortRootEndEquivCotangentDual ↑(f4ShortRootRepresentedRangeBasis i)

                      The first two cotangent-flag blocks are the image of the represented-range basis.

                      source
                      theorem TauCeti.DynkinType.f4ShortRootCotangentFlagBasis_ideal (i : Fin f4ShortRootRepresentedIdealRank) :
                      f4ShortRootCotangentFlagBasis (Fin.castAdd f4ShortRootRepresentedComplementRank (Fin.castAdd 26 i)) = f4ShortRootEndEquivCotangentDual (f4ShortRootRepresentedRange.subtype ↑(f4ShortRootRepresentedIdealBasis i))

                      The first cotangent-flag block is the image of the represented-ideal basis.

                      source
                      @[simp]
                      theorem TauCeti.DynkinType.f4ShortRootCotangentFlagWeight_ideal (i : Fin f4ShortRootRepresentedIdealRank) :
                      f4ShortRootCotangentFlagWeight (Fin.castAdd f4ShortRootRepresentedComplementRank (Fin.castAdd 26 i)) = 2
                      source
                      @[simp]
                      theorem TauCeti.DynkinType.f4ShortRootCotangentFlagWeight_quotient (a : Fin 26) :
                      f4ShortRootCotangentFlagWeight (Fin.castAdd f4ShortRootRepresentedComplementRank (Fin.natAdd f4ShortRootRepresentedIdealRank a)) = 1
                      source
                      @[simp]
                      theorem TauCeti.DynkinType.f4ShortRootCotangentFlagWeight_complement (i : Fin f4ShortRootRepresentedComplementRank) :
                      f4ShortRootCotangentFlagWeight (Fin.natAdd (f4ShortRootRepresentedIdealRank + 26) i) = 0