The identity forced by the character-lattice matrix of a special map

At the level of a root datum, a special isogeny is pinned by a square matrix A together with a permutation σ of the root indices and a rescaling exponent ℓ, subject to the two equations

A *ᵥ root i = ℓ i • root (σ i),    Aᵀ *ᵥ coroot (σ j) = ℓ j • coroot j

The Cartan-integer identity that these equations imply without using the root datum is collected here once, so that the per-type files record only the tables and the equations themselves.

Main results

• TauCeti.mul_dotProduct_eq_of_mulVec_eq_smul: the two displayed equations force the Cartan integers, computed as dot products, to transform by ℓ i ⟨root (σ i), coroot (σ j)⟩ = ℓ j ⟨root i, coroot j⟩.

References

The lattice-level special-isogeny equations this lemma abstracts are those of R. Steinberg, Endomorphisms of Linear Algebraic Groups, §11. The statement is the type-independent core of the per-type files TauCeti/LinearAlgebra/RootSystem/SimplyConnectedRootDatum/B/SpecialMap.lean and TauCeti/LinearAlgebra/RootSystem/SimplyConnectedRootDatum/G2/SpecialMap.lean, where they were first proved.

theorem TauCeti.mul_dotProduct_eq_of_mulVec_eq_smul {n : Type u_1} [Fintype n] {R : Type u_2} [CommSemiring R] {A : Matrix n n R} {ι : Type u_3} {σ : ι → ι} {l : ι → R} {v w : ι → n → R} (hv : ∀ (i : ι), A.mulVec (v i) = l i • v (σ i)) (hw : ∀ (j : ι), A.transpose.mulVec (w (σ j)) = l j • w j) (i j : ι) : l i * v (σ i) ⬝ᵥ w (σ j) = l j * v i ⬝ᵥ w j

The Cartan integers transform by the rule the special-isogeny equations force. If a matrix A carries each member of a family v to a rescaled member, and its transpose carries the correspondingly indexed member of a family w back with the same scalar, then the dot products of the two families satisfy ℓ i ⟨v (σ i), w (σ j)⟩ = ℓ j ⟨v i, w j⟩. Applied to the roots and coroots of a pinned root datum, this is the identity that separates a special isogeny from a diagram automorphism, for which every ℓ is 1.