Documentation

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

The represented flag as a comodule of the prime-field F4 carrier #

The adjoint cotangent comodule of GL₂₆ corestricts to the generated prime-field carrier. The root and torus generator calculations make its adapted 2, 1, 0 flag into actual subcomodules of that carrier. The middle subquotient retains the prescribed Fin 26 basis.

source
@[reducible, inline]
noncomputable abbrev TauCeti.DynkinType.f4ShortRootCarrierCoordinateHopfAlgebra :
CommHopfAlgCat (ZMod 2)

The coordinate Hopf algebra of the generated prime-field short-root F4 carrier.

Equations
  • One or more equations did not get rendered due to their size.
Instances For
    source
    @[instance_reducible]
    noncomputable instance TauCeti.DynkinType.f4ShortRootCarrierCotangentComodule :
    Comodule (ZMod 2) (↑f4ShortRootCarrierCoordinateHopfAlgebra) f4ShortRootCotangentDual

    The adjoint cotangent comodule of GL₂₆, corestricted to the generated carrier.

    Equations
    • One or more equations did not get rendered due to their size.
    source
    theorem TauCeti.DynkinType.f4ShortRootPrimeField_generator_blockTriangular (j : (Fin 4 ⊕ Fin 4) ⊕ Unit) :
    ((Comodule.coefficientMatrix f4ShortRootCotangentFlagBasis).map ⇑(CommHopfAlgCat.Hom.hom (F4ShortRoot.PrimeField.generator j))).BlockTriangular (⇑OrderDual.toDual ∘ f4ShortRootCotangentFlagWeight)

    Every member of the generating family acts block triangularly on the adapted flag.

    source
    theorem TauCeti.DynkinType.f4ShortRootCarrier_coefficientMatrix_blockTriangular :
    (Comodule.coefficientMatrix f4ShortRootCotangentFlagBasis).BlockTriangular (⇑OrderDual.toDual ∘ f4ShortRootCotangentFlagWeight)

    The coefficient matrix of the cotangent representation corestricted to the generated carrier is block triangular for the adapted 2, 1, 0 weights.

    source
    noncomputable def TauCeti.DynkinType.f4ShortRootCarrierCotangentIdeal :
    Subcomodule (ZMod 2) (↑f4ShortRootCarrierCoordinateHopfAlgebra) f4ShortRootCotangentDual

    The ideal step of the adapted cotangent flag as a carrier subcomodule.

    Equations
    • One or more equations did not get rendered due to their size.
    Instances For
      source
      noncomputable def TauCeti.DynkinType.f4ShortRootCarrierCotangentRange :
      Subcomodule (ZMod 2) (↑f4ShortRootCarrierCoordinateHopfAlgebra) f4ShortRootCotangentDual

      The represented-range step of the adapted cotangent flag as a carrier subcomodule.

      Equations
      • One or more equations did not get rendered due to their size.
      Instances For
        source
        @[simp]
        theorem TauCeti.DynkinType.f4ShortRootCarrierCotangentIdeal_toSubmodule_span :
        f4ShortRootCarrierCotangentIdeal.toSubmodule = Submodule.span (ZMod 2) (⇑f4ShortRootCotangentFlagBasis '' {i : Fin (f4ShortRootRepresentedIdealRank + 26 + f4ShortRootRepresentedComplementRank) | 2 ≤ f4ShortRootCotangentFlagWeight i})
        source
        @[simp]
        theorem TauCeti.DynkinType.f4ShortRootCarrierCotangentRange_toSubmodule_span :
        f4ShortRootCarrierCotangentRange.toSubmodule = Submodule.span (ZMod 2) (⇑f4ShortRootCotangentFlagBasis '' {i : Fin (f4ShortRootRepresentedIdealRank + 26 + f4ShortRootRepresentedComplementRank) | 1 ≤ f4ShortRootCotangentFlagWeight i})
        source
        @[reducible, inline]
        noncomputable abbrev TauCeti.DynkinType.f4ShortRootRepresentedIdealAmbient :
        Submodule (ZMod 2) (Module.End (ZMod 2) ↥f4ShortRootLieIdeal)

        The image of the represented ideal inside the ambient endomorphism space.

        Equations
        • One or more equations did not get rendered due to their size.
        Instances For
          source
          noncomputable def TauCeti.DynkinType.f4ShortRootCarrierIdealInRange :
          Subcomodule (ZMod 2) ↑f4ShortRootCarrierCoordinateHopfAlgebra ↥f4ShortRootCarrierCotangentRange

          The represented-ideal step, regarded as a subcomodule of the represented-range step.

          Equations
          Instances For
            source
            @[simp]
            theorem TauCeti.DynkinType.mem_f4ShortRootCarrierIdealInRange (x : ↥f4ShortRootCarrierCotangentRange) :
            x ∈ f4ShortRootCarrierIdealInRange ↔ ↑x ∈ f4ShortRootCarrierCotangentIdeal
            source
            @[instance_reducible]
            noncomputable instance TauCeti.DynkinType.f4ShortRootCarrierCotangentRangeAddCommGroup :
            AddCommGroup ↥f4ShortRootCarrierCotangentRange

            The carrier cotangent range is an additive group, inheriting additive inverses from its module structure over 𝔽₂.

            Equations
            source
            @[reducible, inline]
            abbrev TauCeti.DynkinType.f4ShortRootCarrierMiddle :
            Type

            The middle subquotient of the represented carrier flag.

            Equations
            Instances For
              source
              noncomputable def TauCeti.DynkinType.f4ShortRootCarrierMiddleEquivQuotient :
              f4ShortRootCarrierMiddle ≃ₗ[ZMod 2] f4ModularChevalleyLieAlgebra ⧸ f4ShortRootSubspace

              The middle carrier subquotient is the modular quotient L / I, through its represented realization M / J.

              Equations
              • One or more equations did not get rendered due to their size.
              Instances For
                source
                @[instance_reducible]
                noncomputable instance TauCeti.DynkinType.f4ShortRootQuotientCarrierComodule :
                Comodule (ZMod 2) (↑f4ShortRootCarrierCoordinateHopfAlgebra) (f4ModularChevalleyLieAlgebra ⧸ f4ShortRootSubspace)

                Transport the carrier subquotient comodule to the modular quotient L / I.

                Equations
                source
                noncomputable def TauCeti.DynkinType.f4ShortRootCarrierRepresentedMap :
                f4ModularChevalleyLieAlgebra →ₗ[ZMod 2] ↥f4ShortRootCarrierCotangentRange

                The represented adjoint image, regarded as a vector in the carrier-stable cotangent range.

                Equations
                Instances For
                  source
                  @[simp]
                  theorem TauCeti.DynkinType.f4ShortRootCarrierRepresentedMap_apply (X : f4ModularChevalleyLieAlgebra) :
                  ↑(f4ShortRootCarrierRepresentedMap X) = f4ShortRootEndEquivCotangentDual (f4ShortRootAdjoint X)
                  source
                  noncomputable def TauCeti.DynkinType.f4ShortRootCarrierQuotientProjection :
                  Comodule.Hom (ZMod 2) (↑f4ShortRootCarrierCoordinateHopfAlgebra) (↥f4ShortRootCarrierCotangentRange) (f4ModularChevalleyLieAlgebra ⧸ f4ShortRootSubspace)

                  Project the carrier-stable represented range onto its transported modular quotient.

                  Equations
                  • One or more equations did not get rendered due to their size.
                  Instances For
                    source
                    @[simp]
                    theorem TauCeti.DynkinType.f4ShortRootCarrierMiddleEquivQuotient_symm_mk (X : f4ModularChevalleyLieAlgebra) :
                    f4ShortRootCarrierMiddleEquivQuotient.symm (Submodule.Quotient.mk X) = Submodule.Quotient.mk (f4ShortRootCarrierRepresentedMap X)
                    source
                    @[simp]
                    theorem TauCeti.DynkinType.f4ShortRootCarrierQuotientProjection_representedMap (X : f4ModularChevalleyLieAlgebra) :
                    f4ShortRootCarrierQuotientProjection (f4ShortRootCarrierRepresentedMap X) = Submodule.Quotient.mk X

                    Projecting a represented adjoint vector to the carrier middle block is its modular quotient class.

                    source
                    theorem TauCeti.DynkinType.f4ShortRootCarrierQuotientProjection_baseChange_comp_representedMap {A : Type u_1} [Semiring A] [Algebra (ZMod 2) A] :
                    LinearMap.baseChange A f4ShortRootCarrierQuotientProjection.toLinearMap ∘ₗ LinearMap.baseChange A f4ShortRootCarrierRepresentedMap = LinearMap.baseChange A f4ShortRootSubspace.mkQ

                    The represented adjoint map followed by the carrier quotient projection remains the ordinary quotient map after arbitrary scalar extension.

                    source
                    noncomputable def TauCeti.DynkinType.f4ShortRootQuotientCoordinateBialgHom :
                    ↑(GeneralLinear.coordinateHopfAlgebra (ZMod 2) 26) →ₐc[ZMod 2] ↑f4ShortRootCarrierCoordinateHopfAlgebra

                    The coordinate morphism of the 26-dimensional represented carrier subquotient.

                    Equations
                    Instances For
                      source
                      @[simp]
                      theorem TauCeti.DynkinType.f4ShortRootQuotientCoordinateBialgHom_X (i j : Fin 26) :
                      f4ShortRootQuotientCoordinateBialgHom ((GeneralLinear.coordinateHopfAlgebraAlgEquiv (ZMod 2) 26) ((GeneralLinear.coordinateRingMap (ZMod 2) 26) (MvPolynomial.X (i, j)))) = Comodule.coefficientMatrix f4ShortRootQuotientBasis i j