Documentation

TauCeti.Algebra.Lie.F4.ShortRoot.Modular.Exponential

Integral root exponentials on the modular F₄ short-root ideal #

This file identifies the ambient integral root exponential on the modular short-root ideal with the existing sparse linear and divided-square matrices.

References #

source
noncomputable def TauCeti.DynkinType.f4ShortRootExponential {A : Type u_1} [CommRing A] [Algebra (ZMod 2) A] (k : Fin 4 ⊕ Fin 4) (t : A) :
Module.End A (TensorProduct (ZMod 2) A ↥f4ShortRootLieIdeal)

The three-term root polynomial on the scalar extension of the modular short-root ideal.

Equations
  • One or more equations did not get rendered due to their size.
Instances For
    source
    @[simp]
    theorem TauCeti.DynkinType.f4ShortRootExponential_apply {A : Type u_1} [CommRing A] [Algebra (ZMod 2) A] (k : Fin 4 ⊕ Fin 4) (t : A) (z : ↥f4ShortRootLieIdeal) :
    (f4ShortRootExponential k t) (1 ⊗ₜ[ZMod 2] z) = 1 ⊗ₜ[ZMod 2] z + t • 1 ⊗ₜ[ZMod 2] (f4ShortRootSignedSimpleAdjoint k) z + t ^ 2 • 1 ⊗ₜ[ZMod 2] (f4ShortRootDividedAdjointSquare k) z

    On pure tensors, the restricted root action is its three-term divided-power polynomial.

    source
    noncomputable def TauCeti.DynkinType.f4ShortRootBaseChangeInclusion {A : Type u_1} [CommRing A] [Algebra (ZMod 2) A] :
    TensorProduct (ZMod 2) A ↥f4ShortRootLieIdeal →ₗ[A] TensorProduct ℤ A ↥f4ChevalleyLieLattice

    Include the scalar-extended short-root ideal in the integral Chevalley lattice after canceling the intermediate base change through ZMod 2.

    Equations
    • One or more equations did not get rendered due to their size.
    Instances For
      source
      theorem TauCeti.DynkinType.f4ShortRootBaseChangeInclusion_apply {A : Type u_1} [CommRing A] [Algebra (ZMod 2) A] (z : TensorProduct (ZMod 2) A ↥f4ShortRootLieIdeal) :
      f4ShortRootBaseChangeInclusion z = (cancelBaseChange ℤ (ZMod 2) A ↥f4ChevalleyLieLattice) ((LinearMap.baseChange A ↑f4ShortRootLieIdeal.incl) z)

      Evaluate the scalar-extended ideal inclusion as inclusion followed by cancellation.

      source
      @[simp]
      theorem TauCeti.DynkinType.f4ShortRootBaseChangeInclusion_tmul {A : Type u_1} [CommRing A] [Algebra (ZMod 2) A] (a : A) (z : ↥f4ShortRootLieIdeal) :
      f4ShortRootBaseChangeInclusion (a ⊗ₜ[ZMod 2] z) = (cancelBaseChange ℤ (ZMod 2) A ↥f4ChevalleyLieLattice) (a ⊗ₜ[ZMod 2] ↑z)

      On a pure tensor, the scalar-extended ideal inclusion is the scalar-tower cancellation of the underlying modular vector.

      source
      theorem TauCeti.DynkinType.f4ShortRootBaseChangeInclusion_injective {A : Type u_1} [CommRing A] [Algebra (ZMod 2) A] :
      Function.Injective ⇑f4ShortRootBaseChangeInclusion

      Scalar extension preserves the injection of the short-root ideal into the Chevalley lattice.

      source
      noncomputable def TauCeti.DynkinType.f4ShortRootBaseChangeAdjoint {A : Type u_1} [CommRing A] [Algebra (ZMod 2) A] :
      TensorProduct ℤ A ↥f4ChevalleyLieLattice →ₗ[A] Module.End A (TensorProduct (ZMod 2) A ↥f4ShortRootLieIdeal)

      The scalar-extended adjoint action on the modular short-root ideal, with the ambient Chevalley lattice written directly as A ⊗[ℤ] Lℤ.

      Equations
      • One or more equations did not get rendered due to their size.
      Instances For
        source
        @[simp]
        theorem TauCeti.DynkinType.f4ShortRootBaseChangeAdjoint_apply {A : Type u_1} [CommRing A] [Algebra (ZMod 2) A] (x : TensorProduct ℤ A ↥f4ChevalleyLieLattice) (z : TensorProduct (ZMod 2) A ↥f4ShortRootLieIdeal) :
        (f4ShortRootBaseChangeAdjoint x) z = ((LieModule.toEnd A (TensorProduct (ZMod 2) A f4ModularChevalleyLieAlgebra) (TensorProduct (ZMod 2) A ↥f4ShortRootLieIdeal)) ((cancelBaseChange ℤ (ZMod 2) A ↥f4ChevalleyLieLattice).symm x)) z

        The scalar-extended adjoint acts through cancellation of the two scalar extensions.

        source
        theorem TauCeti.DynkinType.f4ShortRootBaseChangeInclusion_adjoint {A : Type u_1} [CommRing A] [Algebra (ZMod 2) A] (x : TensorProduct ℤ A ↥f4ChevalleyLieLattice) (z : TensorProduct (ZMod 2) A ↥f4ShortRootLieIdeal) :
        f4ShortRootBaseChangeInclusion ((f4ShortRootBaseChangeAdjoint x) z) = ⁅x, f4ShortRootBaseChangeInclusion z⁆

        Evaluating the scalar-extended adjoint action and then including the ideal is the ambient Lie bracket.

        source
        theorem TauCeti.DynkinType.f4ShortRootBaseChangeAdjoint_cancel_tmul {A : Type u_1} [CommRing A] [Algebra (ZMod 2) A] (x : f4ModularChevalleyLieAlgebra) :
        f4ShortRootBaseChangeAdjoint ((cancelBaseChange ℤ (ZMod 2) A ↥f4ChevalleyLieLattice) (1 ⊗ₜ[ZMod 2] x)) = LinearMap.baseChange A (f4ShortRootAdjoint x)

        On a scalar-extended pure tensor, the ambiently indexed adjoint action is the base change of the original modular adjoint action.

        source
        theorem TauCeti.DynkinType.f4ShortRootBaseChangeAdjoint_toMatrix_cancel_tmul {A : Type u_1} [CommRing A] [Algebra (ZMod 2) A] (x : f4ModularChevalleyLieAlgebra) :
        (LinearMap.toMatrix (Module.Basis.baseChange A f4ShortRootLieIdealBasis) (Module.Basis.baseChange A f4ShortRootLieIdealBasis)) (f4ShortRootBaseChangeAdjoint ((cancelBaseChange ℤ (ZMod 2) A ↥f4ChevalleyLieLattice) (1 ⊗ₜ[ZMod 2] x))) = (f4ShortRootAdjointMatrix x).map ⇑(algebraMap (ZMod 2) A)

        The matrix of the scalar-extended adjoint action on a pure tensor is obtained by applying the coefficient map entrywise to the original modular matrix.

        source
        theorem TauCeti.DynkinType.f4ShortRootBaseChangeInclusion_tmul_of_coe_eq {A : Type u_1} [CommRing A] [Algebra (ZMod 2) A] (a : A) (z : ↥f4ShortRootLieIdeal) (y : ↥f4ChevalleyLieLattice) (h : ↑z = 1 ⊗ₜ[ℤ] y) :
        f4ShortRootBaseChangeInclusion (a ⊗ₜ[ZMod 2] z) = a ⊗ₜ[ℤ] y

        A modular ideal vector with an integral lift maps to that lift after scalar extension.

        source
        theorem TauCeti.DynkinType.f4RootExponential_intertwines_tmul_of_coe_eq {A : Type u_1} [CommRing A] [Algebra (ZMod 2) A] (k : Fin 4 ⊕ Fin 4) (t : A) (z : ↥f4ShortRootLieIdeal) (y : ↥f4ChevalleyLieLattice) (hz : ↑z = 1 ⊗ₜ[ℤ] y) (hd1 : ↑((f4ShortRootSignedSimpleAdjoint k) z) = 1 ⊗ₜ[ℤ] ⁅f4IntegralRootVector (f4SignedSimpleRootIndex k), y⁆) (hd2 : ↑((f4ShortRootDividedAdjointSquare k) z) = 1 ⊗ₜ[ℤ] (f4IntegralDividedAdjointSquare k) y) :
        (f4RootExponential k t) (f4ShortRootBaseChangeInclusion (1 ⊗ₜ[ZMod 2] z)) = f4ShortRootBaseChangeInclusion ((f4ShortRootExponential k t) (1 ⊗ₜ[ZMod 2] z))

        On any ideal vector represented by a single integral tensor, the integral root exponential intertwines the modular three-term polynomial with the scalar-tower inclusion.

        source
        theorem TauCeti.DynkinType.f4RootExponential_intertwines_basis {A : Type u_1} [CommRing A] [Algebra (ZMod 2) A] (k : Fin 4 ⊕ Fin 4) (t : A) (b : Fin 26) :
        (f4RootExponential k t) (f4ShortRootBaseChangeInclusion (1 ⊗ₜ[ZMod 2] f4ShortRootLieIdealBasis b)) = f4ShortRootBaseChangeInclusion ((f4ShortRootExponential k t) (1 ⊗ₜ[ZMod 2] f4ShortRootLieIdealBasis b))

        The integral root exponential preserves the scalar-extended modular short-root ideal on every canonical basis column, where its action is the base-changed sparse three-term polynomial.

        source
        theorem TauCeti.DynkinType.f4RootExponential_intertwines {A : Type u_1} [CommRing A] [Algebra (ZMod 2) A] (k : Fin 4 ⊕ Fin 4) (t : A) (x : TensorProduct (ZMod 2) A ↥f4ShortRootLieIdeal) :
        (f4RootExponential k t) (f4ShortRootBaseChangeInclusion x) = f4ShortRootBaseChangeInclusion ((f4ShortRootExponential k t) x)

        The scalar-extended modular short-root ideal is preserved by every signed-simple integral root exponential, and the induced action is the sparse three-term polynomial.

        source
        @[simp]
        theorem TauCeti.DynkinType.f4ShortRootExponential_zero {A : Type u_1} [CommRing A] [Algebra (ZMod 2) A] (k : Fin 4 ⊕ Fin 4) :
        f4ShortRootExponential k 0 = 1

        The restricted root action at zero is the identity.

        source
        theorem TauCeti.DynkinType.f4ShortRootExponential_toMatrix {A : Type u_1} [CommRing A] [Algebra (ZMod 2) A] (k : Fin 4 ⊕ Fin 4) (t : A) :
        (LinearMap.toMatrix (Module.Basis.baseChange A f4ShortRootLieIdealBasis) (Module.Basis.baseChange A f4ShortRootLieIdealBasis)) (f4ShortRootExponential k t) = 1 + t • (F4ShortRoot.rootMatrix k).map Int.cast + t ^ 2 • (F4ShortRoot.rootDividedSquareMatrix k).map Int.cast

        In the scalar-extended canonical basis, the modular root exponential is the existing sparse root matrix plus its divided-square term.

        source
        theorem TauCeti.DynkinType.f4ShortRootExponential_toMatrix_eq_rootSubgroupPoints {A : Type u_1} [CommRing A] [Algebra (ZMod 2) A] (k : Fin 4 ⊕ Fin 4) (u : Multiplicative A) :
        (LinearMap.toMatrix (Module.Basis.baseChange A f4ShortRootLieIdealBasis) (Module.Basis.baseChange A f4ShortRootLieIdealBasis)) (f4ShortRootExponential k (Multiplicative.toAdd u)) = ↑↑((F4ShortRoot.rootSubgroupPoints k A) u)

        The induced root exponential is exactly the existing carrier root-subgroup point.

        source
        theorem TauCeti.DynkinType.f4ShortRootExponential_add {A : Type u_1} [CommRing A] [Algebra (ZMod 2) A] (k : Fin 4 ⊕ Fin 4) (t u : A) :
        f4ShortRootExponential k (t + u) = f4ShortRootExponential k t * f4ShortRootExponential k u

        Restricted root actions compose by addition of their parameters.

        source
        @[simp]
        theorem TauCeti.DynkinType.f4ShortRootExponential_neg_mul {A : Type u_1} [CommRing A] [Algebra (ZMod 2) A] (k : Fin 4 ⊕ Fin 4) (t : A) :
        f4ShortRootExponential k (-t) * f4ShortRootExponential k t = 1

        The action with opposite parameter is a left inverse.

        source
        @[simp]
        theorem TauCeti.DynkinType.f4ShortRootExponential_mul_neg {A : Type u_1} [CommRing A] [Algebra (ZMod 2) A] (k : Fin 4 ⊕ Fin 4) (t : A) :
        f4ShortRootExponential k t * f4ShortRootExponential k (-t) = 1

        The action with opposite parameter is a right inverse.

        source
        theorem TauCeti.DynkinType.f4ShortRootExponential_adjoint_intertwines {A : Type u_1} [CommRing A] [Algebra (ZMod 2) A] (k : Fin 4 ⊕ Fin 4) (t : A) (x : TensorProduct ℤ A ↥f4ChevalleyLieLattice) (z : TensorProduct (ZMod 2) A ↥f4ShortRootLieIdeal) :
        (f4ShortRootExponential k t) ((f4ShortRootBaseChangeAdjoint x) z) = (f4ShortRootBaseChangeAdjoint ((f4RootExponential k t) x)) ((f4ShortRootExponential k t) z)

        Conjugation by a signed-simple root exponential carries the scalar-extended adjoint action to the adjoint action of the transformed ambient vector.

        source
        theorem TauCeti.DynkinType.f4ShortRootExponential_mul_adjoint {A : Type u_1} [CommRing A] [Algebra (ZMod 2) A] (k : Fin 4 ⊕ Fin 4) (t : A) (x : TensorProduct ℤ A ↥f4ChevalleyLieLattice) :
        f4ShortRootExponential k t * f4ShortRootBaseChangeAdjoint x = f4ShortRootBaseChangeAdjoint ((f4RootExponential k t) x) * f4ShortRootExponential k t

        The pointwise adjoint intertwining identity as an equality in the endomorphism algebra.

        source
        theorem TauCeti.DynkinType.f4ShortRootExponential_toMatrix_mul_adjoint {A : Type u_1} [CommRing A] [Algebra (ZMod 2) A] (k : Fin 4 ⊕ Fin 4) (t : A) (x : TensorProduct ℤ A ↥f4ChevalleyLieLattice) :
        have B := Module.Basis.baseChange A f4ShortRootLieIdealBasis; (LinearMap.toMatrix B B) (f4ShortRootExponential k t) * (LinearMap.toMatrix B B) (f4ShortRootBaseChangeAdjoint x) = (LinearMap.toMatrix B B) (f4ShortRootBaseChangeAdjoint ((f4RootExponential k t) x)) * (LinearMap.toMatrix B B) (f4ShortRootExponential k t)

        In the canonical matrix coordinates, left multiplication by a root exponential intertwines the represented adjoint operator with the operator of the transformed ambient vector.