The special length-exchanging map of the pinned type F₄ root datum

In characteristic two, the Ree construction of the families ²F₄ and the Tits group uses a special isogeny of the simply connected group of type F₄. At the root-datum level its character-lattice map reverses the four Bourbaki nodes and multiplies in the long-root direction. In the fundamental-weight coordinates of TauCeti.DynkinType.f4Root, that map is

A = !![0, 0, 0, 1; 0, 0, 1, 0; 0, 2, 0, 0; 2, 0, 0, 0].

This file computes the action of A on every root and of Aᵀ on every coroot. The induced permutation of the forty-eight root indices exchanges long roots with short ones, preserves positivity, and commutes with root negation. The rescaling exponent is the squared-length table TauCeti.DynkinType.f4Length: it is 1 on short roots and 2 on long roots. Applying the data twice multiplies both lattices by 2, and the two exponents along each orbit multiply to 2. The dual map on torus points, its character evaluation, and transport of root-addition edges are computed here as well.

These equations are the explicit F₄ input for the root-datum special-isogeny construction, the last of the three beside the type B₂ case of TauCeti/LinearAlgebra/RootSystem/SimplyConnectedRootDatum/B/SpecialMap.lean and the same-shape G₂ implementation proposed in Tau Ceti PR #4116. They do not yet construct a group-scheme morphism; Layer 9 of the reductive-groups roadmap requires that later lift, together with its action on root subgroups, before the Suzuki--Ree lane can use it.

Main definitions

• TauCeti.DynkinType.f4SpecialIsogenyMatrix: the character-lattice matrix.
• TauCeti.DynkinType.f4SpecialIsogenyIndex: the induced permutation of the forty-eight root indices, and TauCeti.DynkinType.f4SpecialIsogenyIndexEquiv the same permutation as an Equiv.Perm.

The rescaling exponent needs no definition of its own here. The pinned F₄ datum is tabulated on its own root indices, so TauCeti.DynkinType.f4Length already is that exponent; the rank-two type B datum is indexed uniformly in the rank instead, which is why its exponent carries a name of its own.

Main results

• TauCeti.DynkinType.f4SpecialIsogenyMatrix_mulVec_root and TauCeti.DynkinType.f4SpecialIsogenyMatrix_transpose_mulVec_coroot: the equations on the pinned datum.
• TauCeti.DynkinType.f4SpecialIsogenyMatrix_mul_self and its transpose counterpart: applying the lattice map twice is multiplication by 2.
• TauCeti.DynkinType.det_f4SpecialIsogenyMatrix: the map has determinant 4, so it is an isogeny and not a lattice automorphism.
• TauCeti.DynkinType.f4Length_mul_f4Length_specialIsogenyIndex: the two rescaling exponents on an orbit multiply to the defining characteristic.
• TauCeti.DynkinType.f4SpecialIsogenyIndex_castAdd: on the four simple roots the index permutation is TauCeti.lengthPermF4, the pinned length-exchanging permutation of the diagram.
• TauCeti.DynkinType.f4Length_mul_pairing_f4SpecialIsogenyIndex: the Cartan integers transform by the rule a special isogeny forces.
• TauCeti.DynkinType.f4_root_add_smul_iff_specialIsogenyIndexEquiv_root_add: root-addition edges transported by the special map.

References

The node numbering and coordinates follow Bourbaki, Lie Groups and Lie Algebras, Chapters 4--6, Plate VIII. The special-isogeny equations follow R. Steinberg, Endomorphisms of Linear Algebraic Groups, §11; the Ree convention is also described in R. W. Carter, Simple Groups of Lie Type, §§12.3--12.4. The exponent is 1 on long root subgroups and the characteristic on short root subgroups when the group-scheme map is read contravariantly on its root datum. Here the lattice map consequently rescales a root by its own squared length before exchanging its index.

The lattice map and the root permutation

def TauCeti.DynkinType.f4SpecialIsogenyMatrix : Matrix (Fin 4) (Fin 4) ℤ

The character-lattice matrix of the special length-exchanging map of the pinned F₄ root datum, in the fundamental-weight basis.

Equations

• TauCeti.DynkinType.f4SpecialIsogenyMatrix = !![0, 0, 0, 1; 0, 0, 1, 0; 0, 2, 0, 0; 2, 0, 0, 0]

theorem TauCeti.DynkinType.f4SpecialIsogenyMatrix_def : f4SpecialIsogenyMatrix = !![0, 0, 0, 1; 0, 0, 1, 0; 0, 2, 0, 0; 2, 0, 0, 0]

The explicit entries of the character-lattice special-isogeny matrix.

def TauCeti.DynkinType.f4SpecialIsogenyIndex : Fin 48 → Fin 48

The permutation of the forty-eight F₄ roots induced by TauCeti.DynkinType.f4SpecialIsogenyMatrix. It exchanges long roots with short roots and commutes with root negation.

Equations

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

theorem TauCeti.DynkinType.f4SpecialIsogenyIndex_involutive : Function.Involutive f4SpecialIsogenyIndex

The special root permutation is an involution.

def TauCeti.DynkinType.f4SpecialIsogenyIndexEquiv : Equiv.Perm (Fin 48)

The special permutation of the root indices of the pinned type F₄ datum.

Equations

• TauCeti.DynkinType.f4SpecialIsogenyIndexEquiv = Function.Involutive.toPerm TauCeti.DynkinType.f4SpecialIsogenyIndex TauCeti.DynkinType.f4SpecialIsogenyIndex_involutive

@[simp]

theorem TauCeti.DynkinType.f4SpecialIsogenyIndexEquiv_apply (i : Fin 48) : f4SpecialIsogenyIndexEquiv i = f4SpecialIsogenyIndex i

The bundled special permutation acts by the tabulated one.

theorem TauCeti.DynkinType.f4SpecialIsogenyIndexEquiv_f4SpecialIsogenyIndexEquiv (i : Fin 48) : f4SpecialIsogenyIndexEquiv (f4SpecialIsogenyIndexEquiv i) = i

Applying the special root permutation twice restores the pinned index.

@[simp]

theorem TauCeti.DynkinType.f4SpecialIsogenyIndex_add_twentyFour (i : Fin 48) : f4SpecialIsogenyIndex (i + 24) = f4SpecialIsogenyIndex i + 24

The special root permutation commutes with passing to the negative root.

@[simp]

theorem TauCeti.DynkinType.f4SpecialIsogenyIndex_lt_twentyFour_iff (i : Fin 48) : ↑(f4SpecialIsogenyIndex i) < 24 ↔ ↑i < 24

The special root permutation preserves positivity: it maps the twenty-four positive roots, which are the first twenty-four indices, among themselves.

@[simp]

theorem TauCeti.DynkinType.f4SpecialIsogenyIndex_castAdd (i : Fin 4) : f4SpecialIsogenyIndex (Fin.castAdd 44 i) = Fin.castAdd 44 (lengthPermF4 i)

On the four simple roots the special permutation is the pinned length-exchanging permutation of the diagram, namely reversal of the four-node chain.

Action on the pinned root datum

theorem TauCeti.DynkinType.f4SpecialIsogenyMatrix_mulVec_root (i : Fin 48) : f4SpecialIsogenyMatrix.mulVec (f4SimplyConnectedRootDatum.root i) = f4Length i • f4SimplyConnectedRootDatum.root (f4SpecialIsogenyIndexEquiv i)

The special matrix carries every root of the pinned datum to its indexed image with the prescribed exponent.

theorem TauCeti.DynkinType.f4SpecialIsogenyMatrix_transpose_mulVec_coroot (i : Fin 48) : f4SpecialIsogenyMatrix.transpose.mulVec (f4SimplyConnectedRootDatum.coroot (f4SpecialIsogenyIndexEquiv i)) = f4Length i • f4SimplyConnectedRootDatum.coroot i

The transposed special matrix satisfies the contragredient equation on every coroot of the pinned datum.

theorem TauCeti.DynkinType.f4SpecialIsogenyMatrix_mul_self : f4SpecialIsogenyMatrix * f4SpecialIsogenyMatrix = 2 • 1

The square of the character-lattice special matrix is twice the identity matrix.

theorem TauCeti.DynkinType.f4SpecialIsogenyMatrix_transpose_mul_self : f4SpecialIsogenyMatrix.transpose * f4SpecialIsogenyMatrix.transpose = 2 • 1

The square of the cocharacter-lattice special matrix is twice the identity matrix.

theorem TauCeti.DynkinType.f4SpecialIsogenyMatrix_mulVec_self (x : Fin 4 → ℤ) : f4SpecialIsogenyMatrix.mulVec (f4SpecialIsogenyMatrix.mulVec x) = 2 • x

Applying the character-lattice special map twice is multiplication by the characteristic 2.

theorem TauCeti.DynkinType.f4SpecialIsogenyMatrix_transpose_mulVec_self (x : Fin 4 → ℤ) : f4SpecialIsogenyMatrix.transpose.mulVec (f4SpecialIsogenyMatrix.transpose.mulVec x) = 2 • x

Applying the cocharacter-lattice special map twice is multiplication by the characteristic 2.

theorem TauCeti.DynkinType.f4SpecialIsogenyMatrix_mulVecLin_comp_self : f4SpecialIsogenyMatrix.mulVecLin ∘ₗ f4SpecialIsogenyMatrix.mulVecLin = 2 • LinearMap.id

The square relation for the character-lattice map, as an equality of linear maps.

theorem TauCeti.DynkinType.f4SpecialIsogenyMatrix_transpose_mulVecLin_comp_self : f4SpecialIsogenyMatrix.transpose.mulVecLin ∘ₗ f4SpecialIsogenyMatrix.transpose.mulVecLin = 2 • LinearMap.id

The square relation for the cocharacter-lattice map, as an equality of linear maps.

@[simp]

theorem TauCeti.DynkinType.det_f4SpecialIsogenyMatrix : f4SpecialIsogenyMatrix.det = 4

The special map is an isogeny and not an automorphism of the character lattice: its determinant is 4, the square of the characteristic, matching the two long simple directions in which it multiplies.

Length and exponent conventions

@[simp]

theorem TauCeti.DynkinType.f4Length_mul_f4Length_specialIsogenyIndex (i : Fin 48) : f4Length i * f4Length (f4SpecialIsogenyIndex i) = 2

The exponents at a root index and its image multiply to the characteristic 2.

@[simp]

theorem TauCeti.DynkinType.f4Length_specialIsogenyIndex_eq_one_iff (i : Fin 48) : f4Length (f4SpecialIsogenyIndex i) = 1 ↔ f4Length i = 2

The special permutation exchanges long roots with short ones.

@[simp]

theorem TauCeti.DynkinType.f4Length_specialIsogenyIndex_eq_two_iff (i : Fin 48) : f4Length (f4SpecialIsogenyIndex i) = 2 ↔ f4Length i = 1

The special permutation sends a short root to a long root.

theorem TauCeti.DynkinType.f4Length_f4SpecialIsogenyIndexEquiv_eq_one_iff (i : Fin 48) : f4Length (f4SpecialIsogenyIndexEquiv i) = 1 ↔ f4Length i = 2

The special permutation sends a long root to a short root.

theorem TauCeti.DynkinType.f4Length_f4SpecialIsogenyIndexEquiv_eq_two_iff (i : Fin 48) : f4Length (f4SpecialIsogenyIndexEquiv i) = 2 ↔ f4Length i = 1

The special permutation sends a short root to a long root.

theorem TauCeti.DynkinType.f4Length_mul_pairing_f4SpecialIsogenyIndex (i j : Fin 48) : f4Length i * RootPairing.pairing f4SimplyConnectedRootDatum (f4SpecialIsogenyIndexEquiv i) (f4SpecialIsogenyIndexEquiv j) = f4Length j * RootPairing.pairing f4SimplyConnectedRootDatum i j

The Cartan integers transform by the rule a special isogeny forces. Writing α' for the image of a root α under the special permutation, pairing the root equation against the coroot equation gives ℓ(α) ⟨α', β'∨⟩ = ℓ(β) ⟨α, β∨⟩. No diagram automorphism satisfies this, since the two lengths differ.

def TauCeti.DynkinType.f4SpecialIsogenyTorusMap {A : Type u_1} [CommRing A] (s : Fin 4 → Aˣ) : Fin 4 → Aˣ

The torus-point map contravariant to the F4 special character-lattice map.

Equations

• TauCeti.DynkinType.f4SpecialIsogenyTorusMap s = ![s 3 ^ 2, s 2 ^ 2, s 1, s 0]

@[simp]

theorem TauCeti.DynkinType.f4SpecialIsogenyTorusMap_apply_apply {A : Type u_1} [CommRing A] (s : Fin 4 → Aˣ) : f4SpecialIsogenyTorusMap (f4SpecialIsogenyTorusMap s) = fun (i : Fin 4) => s i ^ 2

Applying the special torus map twice is coordinatewise squaring.

theorem TauCeti.DynkinType.torusCharacter_f4SpecialIsogenyTorusMap {A : Type u_1} [CommRing A] (s : Fin 4 → Aˣ) (μ : Fin 4 → ℤ) : torusCharacter (f4SpecialIsogenyTorusMap s) μ = torusCharacter s (f4SpecialIsogenyMatrix.mulVec μ)

Evaluation after the special torus map is evaluation after applying the special character-lattice matrix.

Transport of root-addition edges

theorem TauCeti.DynkinType.f4_root_add_smul_iff_specialIsogenyIndexEquiv_root_add (α β γ : Fin 48) (hβ : f4Length β = 2) (hγ : f4Length γ = 2) : f4SimplyConnectedRootDatum.root γ = f4SimplyConnectedRootDatum.root β + f4Length (f4SpecialIsogenyIndexEquiv α) • f4SimplyConnectedRootDatum.root α ↔ f4SimplyConnectedRootDatum.root (f4SpecialIsogenyIndexEquiv γ) = f4SimplyConnectedRootDatum.root (f4SpecialIsogenyIndexEquiv β) + f4SimplyConnectedRootDatum.root (f4SpecialIsogenyIndexEquiv α)

Root-addition edges transport through the F4 special root permutation. If β and γ are long, applying the special matrix removes their exponent and leaves exactly the exponent of the possibly short root α.

theorem TauCeti.DynkinType.f4_root_add_iff_specialIsogenyIndexEquiv_root_add_of_long (α β γ : Fin 48) (hα : f4Length α = 2) (hβ : f4Length β = 2) (hγ : f4Length γ = 2) : f4SimplyConnectedRootDatum.root γ = f4SimplyConnectedRootDatum.root β + f4SimplyConnectedRootDatum.root α ↔ f4SimplyConnectedRootDatum.root (f4SpecialIsogenyIndexEquiv γ) = f4SimplyConnectedRootDatum.root (f4SpecialIsogenyIndexEquiv β) + f4SimplyConnectedRootDatum.root (f4SpecialIsogenyIndexEquiv α)

A long root direction transports an ordinary first-order root edge.

theorem TauCeti.DynkinType.f4_root_add_two_iff_specialIsogenyIndexEquiv_root_add_of_short (α β γ : Fin 48) (hα : f4Length α = 1) (hβ : f4Length β = 2) (hγ : f4Length γ = 2) : f4SimplyConnectedRootDatum.root γ = f4SimplyConnectedRootDatum.root β + 2 • f4SimplyConnectedRootDatum.root α ↔ f4SimplyConnectedRootDatum.root (f4SpecialIsogenyIndexEquiv γ) = f4SimplyConnectedRootDatum.root (f4SpecialIsogenyIndexEquiv β) + f4SimplyConnectedRootDatum.root (f4SpecialIsogenyIndexEquiv α)

A short root direction transports a second-order source edge to a target root edge.