The coordinate-difference root datum

For a finite coordinate type σ, this file constructs the root datum whose roots and coroots are the vectors e_i - e_j, indexed by ordered pairs i ≠ j. The character and cocharacter lattices are the standard split-torus coordinate lattices

σ →₀ ℤ,    σ → ℤ,

with SplitTorus.dotPairing. Reflections act by transposing the two coordinates that index the reflecting root. The construction is independent of any choice of an enumeration of σ.

Main declarations

• TauCeti.SplitTorus.CoordinateRootIndex: ordered pairs of distinct coordinates.
• TauCeti.SplitTorus.coordinatePermRootIndex: simultaneous application of a coordinate permutation to both entries of a root index.
• TauCeti.SplitTorus.coordinateRoot and coordinateCoroot: the vectors e_i - e_j, defined for arbitrary pairs of coordinates.
• TauCeti.SplitTorus.coordinateRootDatum: the resulting reduced root datum.
• TauCeti.SplitTorus.coordinateRootDatum_pairing_apply: the closed formula for its Cartan integers.
• TauCeti.SplitTorus.coordinateRootDatum_reflection_apply and coordinateRootDatum_coreflection_apply: reflections transpose arbitrary character and cocharacter coordinates.
• TauCeti.SplitTorus.coordinateRootDatum_reflectionPerm: reflections transpose coordinates.

References

• J. S. Milne, Algebraic Groups (2017), Example 19.7.
• J. E. Humphreys, Linear Algebraic Groups (1975), Sections 16.1 and 26.3.

The ordered-pair construction and its proof plan are adapted from the formal template in TauCeti.LinearAlgebra.RootSystem.SimplyConnectedRootDatum.A.

This is the coordinate-lattice construction used by the diagonal-torus root datum of GL_n in Layer 7 of the ReductiveGroups roadmap.

@[reducible, inline]

abbrev TauCeti.SplitTorus.CoordinateRootIndex (σ : Type u_2) : Type u_2

Ordered pairs of distinct coordinates, indexing the roots e_i - e_j.

Equations

• TauCeti.SplitTorus.CoordinateRootIndex σ = { p : σ × σ // p.1 ≠ p.2 }

noncomputable def TauCeti.SplitTorus.coordinatePermRootIndex {σ : Type u_1} (e : Equiv.Perm σ) : CoordinateRootIndex σ ≃ CoordinateRootIndex σ

A coordinate permutation acts on a root index by applying it to both entries.

Equations

• TauCeti.SplitTorus.coordinatePermRootIndex e = (Equiv.prodCongr e e).subtypeEquiv ⋯

@[simp]

theorem TauCeti.SplitTorus.coordinatePermRootIndex_coe {σ : Type u_1} (e : Equiv.Perm σ) (p : CoordinateRootIndex σ) : ↑((coordinatePermRootIndex e) p) = (e (↑p).1, e (↑p).2)

A coordinate permutation acts componentwise on an ordered root index.

@[simp]

theorem TauCeti.SplitTorus.coordinatePermRootIndex_symm {σ : Type u_1} (e : Equiv.Perm σ) : (coordinatePermRootIndex e).symm = coordinatePermRootIndex (Equiv.symm e)

Inverting a coordinate permutation inverts its action on root indices.

@[simp]

theorem TauCeti.SplitTorus.coordinatePermRootIndex_one {σ : Type u_1} : coordinatePermRootIndex 1 = 1

The identity coordinate permutation acts trivially on root indices.

@[simp]

theorem TauCeti.SplitTorus.coordinatePermRootIndex_mul {σ : Type u_1} (e f : Equiv.Perm σ) : coordinatePermRootIndex (e * f) = coordinatePermRootIndex e * coordinatePermRootIndex f

Products of coordinate permutations act by the corresponding product on root indices.

noncomputable def TauCeti.SplitTorus.coordinatePermRootIndexHom {σ : Type u_1} : Equiv.Perm σ →* Equiv.Perm (CoordinateRootIndex σ)

Coordinate permutations acting on the ordered root indices, as a homomorphism.

Equations

• TauCeti.SplitTorus.coordinatePermRootIndexHom = { toFun := TauCeti.SplitTorus.coordinatePermRootIndex, map_one' := ⋯, map_mul' := ⋯ }

@[simp]

theorem TauCeti.SplitTorus.coordinatePermRootIndexHom_apply {σ : Type u_1} (e : Equiv.Perm σ) : coordinatePermRootIndexHom e = coordinatePermRootIndex e

theorem TauCeti.SplitTorus.coordinatePermRootIndexHom_injective {σ : Type u_1} : Function.Injective ⇑coordinatePermRootIndexHom

The action of coordinate permutations on ordered root indices is faithful, including when there are fewer than two coordinates.

noncomputable def TauCeti.SplitTorus.coordinateRoot {σ : Type u_1} (i j : σ) : σ →₀ ℤ

The character-lattice vector e_i - e_j, defined for any two coordinates.

Equations

• TauCeti.SplitTorus.coordinateRoot i j = Finsupp.single i 1 - Finsupp.single j 1

noncomputable def TauCeti.SplitTorus.coordinateCoroot {σ : Type u_1} (i j : σ) : σ → ℤ

The cocharacter-lattice vector e_i - e_j, defined for any two coordinates.

Equations

• TauCeti.SplitTorus.coordinateCoroot i j = ⇑(TauCeti.SplitTorus.coordinateRoot i j)

@[simp]

theorem TauCeti.SplitTorus.coordinateRoot_apply {σ : Type u_1} (i j a : σ) : (coordinateRoot i j) a = (if a = i then 1 else 0) - if a = j then 1 else 0

Evaluation of a coordinate root.

@[simp]

theorem TauCeti.SplitTorus.coordinateCoroot_apply {σ : Type u_1} (i j a : σ) : coordinateCoroot i j a = (if a = i then 1 else 0) - if a = j then 1 else 0

A coordinate coroot is the function underlying the corresponding finitely supported root.

theorem TauCeti.SplitTorus.coe_coordinateRoot {σ : Type u_1} (i j : σ) : ⇑(coordinateRoot i j) = coordinateCoroot i j

The coordinate coroot is the coercion of the coordinate root to a function.

theorem TauCeti.SplitTorus.dotPairing_coordinateRoot_coordinateCoroot {σ : Type u_1} (i j a b : σ) : (dotPairing (coordinateRoot i j)) (coordinateCoroot a b) = ((if i = a then 1 else 0) - if i = b then 1 else 0) - ((if j = a then 1 else 0) - if j = b then 1 else 0)

The split-torus pairing of two coordinate differences, in closed form.

noncomputable def TauCeti.SplitTorus.coordinateRootDatum (σ : Type u_2) [Finite σ] : RootDatum (CoordinateRootIndex σ) (σ →₀ ℤ) (σ → ℤ)

The reduced root datum of all coordinate differences e_i - e_j on a finite coordinate type σ, paired by the split-torus dot product.

Equations

• TauCeti.SplitTorus.coordinateRootDatum σ = RootPairing.mk' TauCeti.SplitTorus.dotPairing TauCeti.SplitTorus.coordinateRootEmbedding✝ TauCeti.SplitTorus.coordinateCorootEmbedding✝ ⋯ ⋯ ⋯

@[simp]

theorem TauCeti.SplitTorus.coordinateRootDatum_toLinearMap {σ : Type u_1} [Finite σ] : (coordinateRootDatum σ).toLinearMap = dotPairing

The underlying bilinear map of the coordinate root datum is the split-torus dot pairing.

@[simp]

theorem TauCeti.SplitTorus.coordinateRootDatum_root {σ : Type u_1} [Finite σ] (p : CoordinateRootIndex σ) : (coordinateRootDatum σ).root p = coordinateRoot (↑p).1 (↑p).2

The roots of the coordinate root datum are the vectors e_i - e_j.

@[simp]

theorem TauCeti.SplitTorus.coordinateRootDatum_coroot {σ : Type u_1} [Finite σ] (p : CoordinateRootIndex σ) : (coordinateRootDatum σ).coroot p = coordinateCoroot (↑p).1 (↑p).2

The coroots of the coordinate root datum are the vectors e_i - e_j.

theorem TauCeti.SplitTorus.coordinateRootDatum_pairing {σ : Type u_1} [Finite σ] (p q : CoordinateRootIndex σ) : RootPairing.pairing (coordinateRootDatum σ) p q = (dotPairing (coordinateRoot (↑p).1 (↑p).2)) (coordinateCoroot (↑q).1 (↑q).2)

The root-datum pairing is the split-torus coordinate dot product. This bridge is not a simp lemma; coordinateRootDatum_pairing_apply is the normal-form simp theorem.

@[simp]

theorem TauCeti.SplitTorus.coordinateRootDatum_pairing_apply {σ : Type u_1} [Finite σ] (p q : CoordinateRootIndex σ) : RootPairing.pairing (coordinateRootDatum σ) p q = ((if (↑p).1 = (↑q).1 then 1 else 0) - if (↑p).1 = (↑q).2 then 1 else 0) - ((if (↑p).2 = (↑q).1 then 1 else 0) - if (↑p).2 = (↑q).2 then 1 else 0)

Closed formula for the Cartan integers of the coordinate root datum.

theorem TauCeti.SplitTorus.coordinateRootDatum_pairing_comm {σ : Type u_1} [Finite σ] (p q : CoordinateRootIndex σ) : RootPairing.pairing (coordinateRootDatum σ) p q = RootPairing.pairing (coordinateRootDatum σ) q p

The root--coroot pairing of the coordinate root datum is symmetric.

instance TauCeti.SplitTorus.isReduced_coordinateRootDatum {σ : Type u_1} [Finite σ] : RootPairing.IsReduced (coordinateRootDatum σ)

The coordinate-difference root datum is reduced.

@[simp]

theorem TauCeti.SplitTorus.coordinateRootDatum_reflection_apply {σ : Type u_1} [Finite σ] (p : CoordinateRootIndex σ) (x : σ →₀ ℤ) (a : σ) : ((RootPairing.reflection (coordinateRootDatum σ) p) x) a = x ((Equiv.swap (↑p).1 (↑p).2) a)

Reflection in the coordinate root indexed by p precomposes an arbitrary character with the transposition of the two coordinates of p.

@[simp]

theorem TauCeti.SplitTorus.coordinateRootDatum_coreflection_apply {σ : Type u_1} [Finite σ] (p : CoordinateRootIndex σ) (x : σ → ℤ) (a : σ) : (RootPairing.coreflection (coordinateRootDatum σ) p) x a = x ((Equiv.swap (↑p).1 (↑p).2) a)

Coreflection in the coordinate root indexed by p precomposes an arbitrary cocharacter with the transposition of the two coordinates of p.

@[simp]

theorem TauCeti.SplitTorus.coordinateRootDatum_reflectionPerm {σ : Type u_1} [Finite σ] [DecidableEq σ] (p q : CoordinateRootIndex σ) : ((coordinateRootDatum σ).reflectionPerm p) q = (coordinatePermRootIndex (Equiv.swap (↑p).1 (↑p).2)) q

Reflections in the coordinate root datum transpose both coordinates of the root index.