The integral and modular Chevalley lattice in type F₄

The full integral Chevalley lattice of the chosen rational F₄ Chevalley system is reduced modulo two. Its root--simple-coroot basis retains the pinned root labels. This file supplies root and coroot vectors, their bracket formulas, and integral root exponentials before selecting the short-root ideal.

This full integral reduction need not equal the Lie algebra generated by the reduced simple matrices in bad characteristic.

References

• R. Steinberg, Endomorphisms of linear algebraic groups, Memoirs AMS 80 (1968), §11.
• R. W. Carter, Simple Groups of Lie Type, §12.3.

@[reducible, inline]

noncomputable abbrev TauCeti.DynkinType.f4KillingBase : (LieAlgebra.IsKilling.rootSystem (F4.cartanSubalgebra valid_F4)).Base

The base of the Killing root system selected by the distinguished F₄ Lie-algebra basis.

Equations

• TauCeti.DynkinType.f4KillingBase = (TauCeti.DynkinType.F4.lieBasis TauCeti.DynkinType.valid_F4).base

@[reducible, inline]

noncomputable abbrev TauCeti.DynkinType.f4ChevalleyLieLattice : LieSubalgebra ℤ ↥(F4.lieAlgebra valid_F4)

The integral Chevalley Lie lattice for the chosen F₄ root-vector system.

Equations

• TauCeti.DynkinType.f4ChevalleyLieLattice = TauCeti.DynkinType.f4ChevalleyRootVector_isChevalleySystem.chevalleyLieLattice

@[reducible, inline]

abbrev TauCeti.DynkinType.f4ChevalleyIndex : Type

Integral Chevalley coordinates: one coordinate for every root and one for every simple coroot.

Equations

• TauCeti.DynkinType.f4ChevalleyIndex = (↥LieSubalgebra.root ⊕ ↥TauCeti.DynkinType.f4KillingBase.support)

noncomputable def TauCeti.DynkinType.f4ChevalleyBasis : Module.Basis f4ChevalleyIndex ℤ ↥f4ChevalleyLieLattice

The root-vector--simple-coroot basis of the integral F₄ Chevalley lattice.

Equations

• TauCeti.DynkinType.f4ChevalleyBasis = TauCeti.DynkinType.f4ChevalleyRootVector_isChevalleySystem.rootSimpleCorootBasis TauCeti.DynkinType.f4KillingBase

@[reducible, inline]

abbrev TauCeti.DynkinType.f4ModularChevalleyLieAlgebra : Type

The Chevalley lattice reduced modulo two.

Equations

• TauCeti.DynkinType.f4ModularChevalleyLieAlgebra = TensorProduct ℤ (ZMod 2) ↥TauCeti.DynkinType.f4ChevalleyLieLattice

noncomputable def TauCeti.DynkinType.f4ModularChevalleyBasis : Module.Basis f4ChevalleyIndex (ZMod 2) f4ModularChevalleyLieAlgebra

The integral root--simple-coroot coordinates, retained after reduction modulo two.

Equations

• TauCeti.DynkinType.f4ModularChevalleyBasis = Module.Basis.baseChange (ZMod 2) TauCeti.DynkinType.f4ChevalleyBasis

noncomputable def TauCeti.DynkinType.f4IntegralRootVector (i : Fin 48) : ↥f4ChevalleyLieLattice

A root vector as an element of the integral Chevalley lattice.

Equations

• TauCeti.DynkinType.f4IntegralRootVector i = TauCeti.DynkinType.f4ChevalleyBasis (Sum.inl (TauCeti.DynkinType.f4KillingRootLabel i))

noncomputable def TauCeti.DynkinType.f4ModularRootVector (i : Fin 48) : f4ModularChevalleyLieAlgebra

A root vector in the Chevalley lattice reduced modulo two.

Equations

• TauCeti.DynkinType.f4ModularRootVector i = TauCeti.DynkinType.f4ModularChevalleyBasis (Sum.inl (TauCeti.DynkinType.f4KillingRootLabel i))

noncomputable def TauCeti.DynkinType.f4IntegralCoroot (i : Fin 48) : ↥f4ChevalleyLieLattice

The coroot of a pinned root as an element of the integral Chevalley lattice.

Equations

• TauCeti.DynkinType.f4IntegralCoroot i = ⟨↑(LieAlgebra.IsKilling.coroot (TauCeti.DynkinType.f4KillingRoot i)), ⋯⟩

noncomputable def TauCeti.DynkinType.f4IntegralSimpleCoroot (i : Fin F4.rank) : ↥f4ChevalleyLieLattice

A simple coroot as a named integral Chevalley basis vector.

Equations

• TauCeti.DynkinType.f4IntegralSimpleCoroot i = TauCeti.DynkinType.f4ChevalleyBasis (Sum.inr ((TauCeti.DynkinType.F4.lieBasis TauCeti.DynkinType.valid_F4).baseSupportEquiv i))

noncomputable def TauCeti.DynkinType.f4ModularSimpleCoroot (i : Fin F4.rank) : f4ModularChevalleyLieAlgebra

A simple coroot basis vector after reduction modulo two.

Equations

• TauCeti.DynkinType.f4ModularSimpleCoroot i = TauCeti.DynkinType.f4ModularChevalleyBasis (Sum.inr ((TauCeti.DynkinType.F4.lieBasis TauCeti.DynkinType.valid_F4).baseSupportEquiv i))

noncomputable def TauCeti.DynkinType.f4ModularCoroot (i : Fin 48) : f4ModularChevalleyLieAlgebra

An arbitrary coroot after reduction modulo two.

Equations

• TauCeti.DynkinType.f4ModularCoroot i = 1 ⊗ₜ[ℤ] TauCeti.DynkinType.f4IntegralCoroot i

theorem TauCeti.DynkinType.f4ModularRootVector_eq_basis (i : Fin 48) : f4ModularRootVector i = f4ModularChevalleyBasis (Sum.inl (f4KillingRootLabel i))

A modular root vector is the Chevalley basis vector with its Killing-root label.

theorem TauCeti.DynkinType.f4ModularSimpleCoroot_eq_basis (i : Fin F4.rank) : f4ModularSimpleCoroot i = f4ModularChevalleyBasis (Sum.inr ((F4.lieBasis valid_F4).baseSupportEquiv i))

A modular simple coroot is the Chevalley basis vector with its simple-root support label.

@[simp]

theorem TauCeti.DynkinType.f4ModularChevalleyBasis_inr_eq_simpleCoroot (j : ↥f4KillingBase.support) : f4ModularChevalleyBasis (Sum.inr j) = f4ModularSimpleCoroot ((F4.lieBasis valid_F4).baseSupportEquiv.symm j)

A simple-coroot basis label reduces to its named modular coroot.

@[simp]

theorem TauCeti.DynkinType.coe_f4IntegralRootVector (i : Fin 48) : ↑(f4IntegralRootVector i) = f4ChevalleyRootVector (f4KillingRoot i)

@[simp]

theorem TauCeti.DynkinType.coe_f4IntegralCoroot (i : Fin 48) : ↑(f4IntegralCoroot i) = ↑(LieAlgebra.IsKilling.coroot (f4KillingRoot i))

@[simp]

theorem TauCeti.DynkinType.coe_f4IntegralSimpleCoroot (i : Fin F4.rank) : ↑(f4IntegralSimpleCoroot i) = ↑(LieAlgebra.IsKilling.coroot ↑↑((F4.lieBasis valid_F4).baseSupportEquiv i))

theorem TauCeti.DynkinType.f4ModularRootVector_eq (i : Fin 48) : f4ModularRootVector i = 1 ⊗ₜ[ℤ] f4IntegralRootVector i

theorem TauCeti.DynkinType.f4ModularSimpleCoroot_eq (i : Fin F4.rank) : f4ModularSimpleCoroot i = 1 ⊗ₜ[ℤ] f4IntegralSimpleCoroot i

theorem TauCeti.DynkinType.f4Integral_lie_simpleCoroot_rootVector (i : Fin F4.rank) (α : Fin 48) : ⁅f4IntegralSimpleCoroot i, f4IntegralRootVector α⁆ = RootPairing.pairing f4SimplyConnectedRootDatum α (Fin.castAdd 44 (Fin.cast rank_F4 i)) • f4IntegralRootVector α

A simple integral coroot acts on an integral root vector by the pinned Cartan integer.

theorem TauCeti.DynkinType.f4Modular_lie_simpleCoroot_rootVector (i : Fin F4.rank) (α : Fin 48) : ⁅f4ModularSimpleCoroot i, f4ModularRootVector α⁆ = ↑(RootPairing.pairing f4SimplyConnectedRootDatum α (Fin.castAdd 44 (Fin.cast rank_F4 i))) • f4ModularRootVector α

A modular simple coroot acts on a modular root vector by the reduced pinned Cartan integer.

theorem TauCeti.DynkinType.f4Modular_lie_rootVector_simpleCoroot (α : Fin 48) (i : Fin F4.rank) : ⁅f4ModularRootVector α, f4ModularSimpleCoroot i⁆ = -↑(RootPairing.pairing f4SimplyConnectedRootDatum α (Fin.castAdd 44 (Fin.cast rank_F4 i))) • f4ModularRootVector α

A modular root vector acts on a simple coroot by the negative reduced Cartan integer.

theorem TauCeti.DynkinType.f4IntegralCoroot_eq_sum_simple (β : Fin 48) : f4IntegralCoroot β = ∑ i : Fin F4.rank, f4Coroot β (Fin.cast rank_F4 i) • f4IntegralSimpleCoroot i

Integral coroot coordinates in the Chevalley basis are the pinned coroot coordinates.

theorem TauCeti.DynkinType.f4ModularCoroot_eq_sum_simple (β : Fin 48) : f4ModularCoroot β = ∑ i : Fin F4.rank, ↑(f4Coroot β (Fin.cast rank_F4 i)) • f4ModularSimpleCoroot i

Reduction modulo two preserves the pinned simple-coroot coordinate expansion.

@[simp]

theorem TauCeti.DynkinType.f4ModularCoroot_castAdd (i : Fin 4) : f4ModularCoroot (Fin.castAdd 44 i) = f4ModularSimpleCoroot (Fin.cast ⋯ i)

The modular coroot at a pinned simple-root index is the corresponding simple-coroot basis vector.

theorem TauCeti.DynkinType.exists_f4Integral_lie_rootVector_eq_zsmul_of_add (α β γ : Fin 48) (h : f4SimplyConnectedRootDatum.root γ = f4SimplyConnectedRootDatum.root β + f4SimplyConnectedRootDatum.root α) : ∃ (z : ℤ), z.natAbs = RootPairing.chainBotCoeff α β + 1 ∧ ⁅f4IntegralRootVector α, f4IntegralRootVector β⁆ = z • f4IntegralRootVector γ

The exact integral root-edge bracket inherited by the Chevalley lattice.

theorem TauCeti.DynkinType.exists_f4Modular_lie_rootVector_eq_smul_of_add (α β γ : Fin 48) (h : f4SimplyConnectedRootDatum.root γ = f4SimplyConnectedRootDatum.root β + f4SimplyConnectedRootDatum.root α) : ∃ (z : ℤ), z.natAbs = RootPairing.chainBotCoeff α β + 1 ∧ ⁅f4ModularRootVector α, f4ModularRootVector β⁆ = ↑z • f4ModularRootVector γ

Every modular root-edge bracket is the reduction of its exact integral Chevalley coefficient.

theorem TauCeti.DynkinType.f4Modular_lie_rootVector_of_add_of_chainBotCoeff_eq_zero (α β γ : Fin 48) (h : f4SimplyConnectedRootDatum.root γ = f4SimplyConnectedRootDatum.root β + f4SimplyConnectedRootDatum.root α) (hbot : RootPairing.chainBotCoeff α β = 0) : ⁅f4ModularRootVector α, f4ModularRootVector β⁆ = f4ModularRootVector γ

A root edge with zero descending coefficient has unit modular bracket coefficient; its integral sign disappears modulo two.

theorem TauCeti.DynkinType.f4Modular_lie_rootVector_of_add_of_length_eq (α β γ : Fin 48) (hβγ : f4Length β = f4Length γ) (h : f4SimplyConnectedRootDatum.root γ = f4SimplyConnectedRootDatum.root β + f4SimplyConnectedRootDatum.root α) : ⁅f4ModularRootVector α, f4ModularRootVector β⁆ = f4ModularRootVector γ

A root edge between two roots of equal length has unit modular bracket coefficient.

theorem TauCeti.DynkinType.f4Modular_lie_rootVector_eq_zero_of_rootSpace_add_eq_bot (α β : Fin 48) (hbot : LieAlgebra.rootSpace (F4.cartanSubalgebra valid_F4) (⇑(f4KillingRoot α) + ⇑(f4KillingRoot β)) = ⊥) : ⁅f4ModularRootVector α, f4ModularRootVector β⁆ = 0

Modular root vectors bracket to zero when their rational root-space sum is absent.

@[reducible, inline]

noncomputable abbrev TauCeti.DynkinType.f4PinnedRootIndex (α : ↥LieSubalgebra.root) : Fin 48

Recover the pinned integral root label of a Killing root.

Equations

• TauCeti.DynkinType.f4PinnedRootIndex α = Fin.cast TauCeti.DynkinType.numRoots_F4 ((↑(TauCeti.DynkinType.F4.rationalRootSystemEquiv TauCeti.DynkinType.valid_F4)).indexEquiv.symm α)

@[simp]

theorem TauCeti.DynkinType.f4KillingRootLabel_f4PinnedRootIndex (α : ↥LieSubalgebra.root) : f4KillingRootLabel (f4PinnedRootIndex α) = α

@[simp]

theorem TauCeti.DynkinType.f4PinnedRootIndex_f4KillingRootLabel (i : Fin 48) : f4PinnedRootIndex (f4KillingRootLabel i) = i

@[simp]

theorem TauCeti.DynkinType.f4ModularChevalleyBasis_inl_eq_rootVector (α : ↥LieSubalgebra.root) : f4ModularChevalleyBasis (Sum.inl α) = f4ModularRootVector (f4PinnedRootIndex α)

@[simp]

theorem TauCeti.DynkinType.f4OppositeRootIndex_castAdd (i : Fin 4) : f4OppositeRootIndex (Fin.castAdd 44 i) = (Fin.castAdd 20 i).addNat 24

In the pinned F₄ table the root opposite to a simple root is the corresponding entry in the second half of the table.

noncomputable def TauCeti.DynkinType.f4SignedSimpleRootIndex : Fin 4 ⊕ Fin 4 → Fin 48

The pinned root index of a positive or negative simple root.

Equations

• TauCeti.DynkinType.f4SignedSimpleRootIndex (Sum.inl i) = Fin.castAdd 44 i
• TauCeti.DynkinType.f4SignedSimpleRootIndex (Sum.inr i) = TauCeti.DynkinType.f4OppositeRootIndex (Fin.castAdd 44 i)

@[simp]

theorem TauCeti.DynkinType.f4SignedSimpleRootIndex_inl (i : Fin 4) : f4SignedSimpleRootIndex (Sum.inl i) = Fin.castAdd 44 i

A positive simple-root label is its pinned root index.

@[simp]

theorem TauCeti.DynkinType.f4SignedSimpleRootIndex_inr (i : Fin 4) : f4SignedSimpleRootIndex (Sum.inr i) = f4OppositeRootIndex (Fin.castAdd 44 i)

A negative simple-root label is the index opposite to the corresponding positive root.

noncomputable def TauCeti.DynkinType.f4ModularSignedSimpleRootVector (k : Fin 4 ⊕ Fin 4) : f4ModularChevalleyLieAlgebra

A pinned positive or negative simple root vector in the reduced Chevalley lattice.

Equations

• TauCeti.DynkinType.f4ModularSignedSimpleRootVector k = TauCeti.DynkinType.f4ModularRootVector (TauCeti.DynkinType.f4SignedSimpleRootIndex k)

@[simp]

theorem TauCeti.DynkinType.f4ModularSignedSimpleRootVector_eq (k : Fin 4 ⊕ Fin 4) : f4ModularSignedSimpleRootVector k = f4ModularRootVector (f4SignedSimpleRootIndex k)

A signed simple root vector is the modular root vector at its pinned root index.

@[simp]

theorem TauCeti.DynkinType.f4ModularCoroot_f4OppositeRootIndex (α : Fin 48) : f4ModularCoroot (f4OppositeRootIndex α) = f4ModularCoroot α

Opposite roots have the same coroot after reduction modulo two.

@[simp]

theorem TauCeti.DynkinType.f4ModularCoroot_addNat_castAdd (i : Fin 4) : f4ModularCoroot ((Fin.castAdd 20 i).addNat 24) = f4ModularSimpleCoroot (Fin.cast ⋯ i)

In characteristic two the negative of a pinned simple root has the same modular coroot.

theorem TauCeti.DynkinType.f4Modular_lie_rootVector_eq_zero_of_chainTopCoeff_eq_zero (α β : Fin 48) (hopp : α ≠ f4OppositeRootIndex β) (htop : RootPairing.chainTopCoeff α β = 0) : ⁅f4ModularRootVector α, f4ModularRootVector β⁆ = 0

If the pinned root string from β in direction α has no positive step, then the corresponding modular Chevalley bracket vanishes.

theorem TauCeti.DynkinType.f4Integral_lie_rootVector_opposite (α : Fin 48) : ⁅f4IntegralRootVector α, f4IntegralRootVector (f4OppositeRootIndex α)⁆ = f4IntegralCoroot α

Opposite integral root vectors bracket to the corresponding integral coroot.

theorem TauCeti.DynkinType.f4Modular_lie_rootVector_opposite (α : Fin 48) : ⁅f4ModularRootVector α, f4ModularRootVector (f4OppositeRootIndex α)⁆ = f4ModularCoroot α

Opposite modular root vectors bracket to the corresponding modular coroot.

@[reducible, inline]

noncomputable abbrev TauCeti.DynkinType.f4PinnedSimpleIndexEquiv : ↥f4KillingBase.support ≃ Fin 4

The pinned numbering of simple Killing-root support labels.

Equations

• TauCeti.DynkinType.f4PinnedSimpleIndexEquiv = (TauCeti.DynkinType.F4.lieBasis TauCeti.DynkinType.valid_F4).baseSupportEquiv.symm.trans (finCongr TauCeti.DynkinType.rank_F4)

theorem TauCeti.DynkinType.f4PinnedSimpleIndexEquiv_apply (i : ↥f4KillingBase.support) : f4PinnedSimpleIndexEquiv i = Fin.cast rank_F4 ((F4.lieBasis valid_F4).baseSupportEquiv.symm i)

Evaluate the pinned simple-index equivalence.

theorem TauCeti.DynkinType.f4PinnedSimpleIndexEquiv_symm_apply (k : Fin 4) : f4PinnedSimpleIndexEquiv.symm k = (F4.lieBasis valid_F4).baseSupportEquiv (Fin.cast ⋯ k)

Evaluate the inverse pinned simple-index equivalence.

theorem TauCeti.DynkinType.f4PinnedSimpleIndexEquiv_baseSupportEquiv (i : Fin F4.rank) : f4PinnedSimpleIndexEquiv ((F4.lieBasis valid_F4).baseSupportEquiv i) = Fin.cast rank_F4 i

theorem TauCeti.DynkinType.f4ModularChevalleyBasis_inr_f4PinnedSimpleIndexEquiv_symm (k : Fin 4) : f4ModularChevalleyBasis (Sum.inr (f4PinnedSimpleIndexEquiv.symm k)) = f4ModularSimpleCoroot (Fin.cast ⋯ k)

A pinned simple-index coordinate is the corresponding modular simple coroot.

theorem TauCeti.DynkinType.f4Modular_lie_simpleCoroot_simpleCoroot_eq_zero (i j : Fin F4.rank) : ⁅f4ModularSimpleCoroot i, f4ModularSimpleCoroot j⁆ = 0

Modular simple coroots commute.

@[simp]

theorem TauCeti.DynkinType.f4ModularChevalleyBasis_repr_simpleCoroot_inl (i : Fin F4.rank) (γ : Fin 48) : (f4ModularChevalleyBasis.repr (f4ModularSimpleCoroot i)) (Sum.inl (f4KillingRootLabel γ)) = 0

A simple coroot has no root-vector coordinate.

@[simp]

theorem TauCeti.DynkinType.f4ModularChevalleyBasis_repr_coroot_inl (β γ : Fin 48) : (f4ModularChevalleyBasis.repr (f4ModularCoroot β)) (Sum.inl (f4KillingRootLabel γ)) = 0

A modular coroot has no root-vector coordinate.

@[simp]

theorem TauCeti.DynkinType.f4ModularChevalleyBasis_repr_rootVector_inl_eq_zero (ε γ : Fin 48) (hεγ : f4KillingRootLabel ε ≠ f4KillingRootLabel γ) : (f4ModularChevalleyBasis.repr (f4ModularRootVector ε)) (Sum.inl (f4KillingRootLabel γ)) = 0

A root vector has zero coordinate at any different root label.

@[simp]

theorem TauCeti.DynkinType.f4ModularChevalleyBasis_repr_rootVector_self (β : Fin 48) : (f4ModularChevalleyBasis.repr (f4ModularRootVector β)) (Sum.inl (f4KillingRootLabel β)) = 1

The coordinate of a root vector at its own root label is one.

theorem TauCeti.DynkinType.f4_root_eq_add_of_repr_lie_rootVector_ne_zero (δ β γ : Fin 48) (hne : (f4ModularChevalleyBasis.repr ⁅f4ModularRootVector δ, f4ModularRootVector β⁆) (Sum.inl (f4KillingRootLabel γ)) ≠ 0) : f4SimplyConnectedRootDatum.root γ = f4SimplyConnectedRootDatum.root β + f4SimplyConnectedRootDatum.root δ

A nonzero root coordinate in a modular root-vector bracket has the expected integral root label, even though the bracket itself is reduced modulo two.

@[simp]

theorem TauCeti.DynkinType.f4ModularChevalleyBasis_repr_lie_simpleCoroot_rootVector_self (i : Fin F4.rank) (β : Fin 48) : (f4ModularChevalleyBasis.repr ⁅f4ModularSimpleCoroot i, f4ModularRootVector β⁆) (Sum.inl (f4KillingRootLabel β)) = ↑(f4Root β (Fin.cast rank_F4 i))

The root-vector coordinate of a simple-coroot bracket is its reduced Cartan integer.

@[simp]

theorem TauCeti.DynkinType.f4ModularChevalleyBasis_repr_lie_rootVector_eq_zero (δ β γ : Fin 48) (h : f4Root γ ≠ f4Root β + f4Root δ) : (f4ModularChevalleyBasis.repr ⁅f4ModularRootVector δ, f4ModularRootVector β⁆) (Sum.inl (f4KillingRootLabel γ)) = 0

A root-vector bracket has no coordinate at an unrelated root label.

@[simp]

theorem TauCeti.DynkinType.f4ModularChevalleyBasis_repr_lie_simpleCoroot_rootVector_eq_zero (i : Fin F4.rank) (β γ : Fin 48) (hβγ : f4KillingRootLabel β ≠ f4KillingRootLabel γ) : (f4ModularChevalleyBasis.repr ⁅f4ModularSimpleCoroot i, f4ModularRootVector β⁆) (Sum.inl (f4KillingRootLabel γ)) = 0

A simple-coroot bracket has no coordinate away from its root label.

@[simp]

theorem TauCeti.DynkinType.f4ModularChevalleyBasis_repr_lie_rootVector_self_eq_zero (δ β : Fin 48) : (f4ModularChevalleyBasis.repr ⁅f4ModularRootVector δ, f4ModularRootVector β⁆) (Sum.inl (f4KillingRootLabel β)) = 0

A root-vector bracket has zero coordinate at the second factor's root label.

Integral root exponentials

noncomputable def TauCeti.DynkinType.f4RootAdjointDerivation (k : Fin 4 ⊕ Fin 4) : LieDerivation ℚ ↥(F4.lieAlgebra valid_F4) ↥(F4.lieAlgebra valid_F4)

The signed-root adjoint derivation.

Equations

• One or more equations did not get rendered due to their size.

@[simp]

theorem TauCeti.DynkinType.f4RootAdjointDerivation_apply (k : Fin 4 ⊕ Fin 4) (x : ↥(F4.lieAlgebra valid_F4)) : (f4RootAdjointDerivation k) x = ⁅f4ChevalleyRootVector (f4KillingRoot (f4SignedSimpleRootIndex k)), x⁆

The root derivation acts by the rational Lie bracket.

theorem TauCeti.DynkinType.f4RootAdjointDerivation_toLinearMap (k : Fin 4 ⊕ Fin 4) : ↑(f4RootAdjointDerivation k) = (LieAlgebra.ad ℚ ↥(F4.lieAlgebra valid_F4)) (f4ChevalleyRootVector (f4KillingRoot (f4SignedSimpleRootIndex k)))

The underlying linear map is the adjoint endomorphism of the rational root vector.

theorem TauCeti.DynkinType.f4RootAdjointDerivation_dividedPower_mem (k : Fin 4 ⊕ Fin 4) (n : ℕ) (y : ↥(F4.lieAlgebra valid_F4)) (hy : y ∈ f4ChevalleyLieLattice) : (Associative.dividedPower n ↑(f4RootAdjointDerivation k)) y ∈ f4ChevalleyLieLattice

All divided powers of the root adjoint derivation preserve the integral Chevalley lattice.

theorem TauCeti.DynkinType.isNilpotent_f4RootAdjointDerivation (k : Fin 4 ⊕ Fin 4) : IsNilpotent ↑(f4RootAdjointDerivation k)

The root adjoint derivation is nilpotent.

noncomputable def TauCeti.DynkinType.f4RootExponential {A : Type u_1} [CommRing A] [Algebra ℤ A] (k : Fin 4 ⊕ Fin 4) (t : A) : Module.End A (TensorProduct ℤ A ↥f4ChevalleyLieLattice)

The integral root exponential after extension to an arbitrary parameter ring.

Equations

• TauCeti.DynkinType.f4RootExponential k t = TauCeti.baseChangeExp (↑(TauCeti.DynkinType.f4RootAdjointDerivation k)) TauCeti.DynkinType.f4ChevalleyLieLattice ⋯ t

noncomputable def TauCeti.DynkinType.f4IntegralDividedAdjointSquare (k : Fin 4 ⊕ Fin 4) : Module.End ℤ ↥f4ChevalleyLieLattice

The second divided adjoint power of a signed simple root on the integral Chevalley lattice.

Equations

• TauCeti.DynkinType.f4IntegralDividedAdjointSquare k = TauCeti.integralDividedPower (↑(TauCeti.DynkinType.f4RootAdjointDerivation k)) TauCeti.DynkinType.f4ChevalleyLieLattice 2 ⋯

@[simp]

theorem TauCeti.DynkinType.coe_f4IntegralDividedAdjointSquare_apply (k : Fin 4 ⊕ Fin 4) (y : ↥f4ChevalleyLieLattice) : ↑((f4IntegralDividedAdjointSquare k) y) = Associative.dividedPower 2 ((LieAlgebra.ad ℚ ↥(F4.lieAlgebra valid_F4)) (f4ChevalleyRootVector (f4KillingRoot (f4SignedSimpleRootIndex k)))) • ↑y

The integral divided square acts in the ambient Lie algebra by the second divided adjoint power.

theorem TauCeti.DynkinType.f4RootAdjointDerivation_pow_three_integralRootVector (k : Fin 4 ⊕ Fin 4) (i : Fin 48) : (↑(f4RootAdjointDerivation k) ^ 3) ↑(f4IntegralRootVector i) = 0

The third adjoint power vanishes on every integral root vector.

theorem TauCeti.DynkinType.f4RootAdjointDerivation_pow_three_integralSimpleCoroot (k : Fin 4 ⊕ Fin 4) (i : Fin F4.rank) : (↑(f4RootAdjointDerivation k) ^ 3) ↑(f4IntegralSimpleCoroot i) = 0

The third adjoint power vanishes on each integral simple coroot.

theorem TauCeti.DynkinType.f4RootAdjointDerivation_pow_three_integral (k : Fin 4 ⊕ Fin 4) (y : ↥f4ChevalleyLieLattice) : (↑(f4RootAdjointDerivation k) ^ 3) ↑y = 0

The third signed-root adjoint power vanishes on the whole integral Chevalley lattice.

theorem TauCeti.DynkinType.integralDividedPower_f4RootAdjointDerivation_one_apply_eq_lie (k : Fin 4 ⊕ Fin 4) (y : ↥f4ChevalleyLieLattice) : (integralDividedPower (↑(f4RootAdjointDerivation k)) f4ChevalleyLieLattice 1 ⋯) y = ⁅f4IntegralRootVector (f4SignedSimpleRootIndex k), y⁆

The first integral divided power is the Lie bracket in the Chevalley lattice.

theorem TauCeti.DynkinType.f4RootExponential_tmul {A : Type u_1} [CommRing A] [Algebra ℤ A] (k : Fin 4 ⊕ Fin 4) (t : A) (y : ↥f4ChevalleyLieLattice) : (f4RootExponential k t) (1 ⊗ₜ[ℤ] y) = 1 ⊗ₜ[ℤ] y + t • 1 ⊗ₜ[ℤ] ⁅f4IntegralRootVector (f4SignedSimpleRootIndex k), y⁆ + t ^ 2 • 1 ⊗ₜ[ℤ] (f4IntegralDividedAdjointSquare k) y

On every integral pure tensor, the root exponential is its three-term divided-power polynomial over any parameter ring.

noncomputable def TauCeti.DynkinType.f4RootExponentialLieEquiv {A : Type u_1} [CommRing A] [Algebra ℤ A] (k : Fin 4 ⊕ Fin 4) (t : A) : TensorProduct ℤ A ↥f4ChevalleyLieLattice ≃ₗ⁅A⁆ TensorProduct ℤ A ↥f4ChevalleyLieLattice

The integral root exponential as a Lie algebra automorphism after arbitrary scalar extension.

Equations

• TauCeti.DynkinType.f4RootExponentialLieEquiv k t = TauCeti.baseChangeExpLieEquiv (TauCeti.DynkinType.f4RootAdjointDerivation k) TauCeti.DynkinType.f4ChevalleyLieLattice ⋯ ⋯ t

@[simp]

theorem TauCeti.DynkinType.f4RootExponential_zero {A : Type u_1} [CommRing A] [Algebra ℤ A] (k : Fin 4 ⊕ Fin 4) : f4RootExponential k 0 = 1

The root exponential at parameter zero is the identity endomorphism.

theorem TauCeti.DynkinType.f4RootExponential_add {A : Type u_1} [CommRing A] [Algebra ℤ A] (k : Fin 4 ⊕ Fin 4) (t u : A) : f4RootExponential k (t + u) = f4RootExponential k t * f4RootExponential k u

Root exponentials compose by adding their parameters.

@[simp]

theorem TauCeti.DynkinType.f4RootExponentialLieEquiv_zero {A : Type u_1} [CommRing A] [Algebra ℤ A] (k : Fin 4 ⊕ Fin 4) : f4RootExponentialLieEquiv k 0 = LieEquiv.refl

The root Lie automorphism at parameter zero is the identity.

theorem TauCeti.DynkinType.f4RootExponentialLieEquiv_trans {A : Type u_1} [CommRing A] [Algebra ℤ A] (k : Fin 4 ⊕ Fin 4) (t u : A) : (f4RootExponentialLieEquiv k t).trans (f4RootExponentialLieEquiv k u) = f4RootExponentialLieEquiv k (t + u)

Root Lie automorphisms compose by adding their parameters.

@[simp]

theorem TauCeti.DynkinType.f4RootExponentialLieEquiv_apply {A : Type u_1} [CommRing A] [Algebra ℤ A] (k : Fin 4 ⊕ Fin 4) (t : A) (x : TensorProduct ℤ A ↥f4ChevalleyLieLattice) : (f4RootExponentialLieEquiv k t) x = (f4RootExponential k t) x

The Lie equivalence acts by the integral root exponential on every vector.