Integral matrices acting on a rational coordinate space

An explicit Chevalley carrier starts from a representation of a Serre presentation by matrices with integer entries, extends it to the rational Serre algebra, and shows that the integral coordinate lattice of the rational module is preserved. This file collects the facts that step needs, stated for an arbitrary index type so that every such carrier shares them.

Entrywise coercion of integer matrices is a homomorphism of Lie rings for the commutator brackets, so it carries a Serre system over ℤ to one over the target ring. A coerced integer matrix then sends integral coordinate vectors to integral coordinate vectors, which is what keeps the lattice stable under the resulting action.

Main declarations

• TauCeti.matrixIntCastLieHom: entrywise coercion of integer matrices, as a homomorphism of Lie rings.

Main results

• TauCeti.matrixIntCastLieHom_apply and TauCeti.matrixIntCastLieHom_mul: the coercion acts entrywise and is multiplicative.
• Matrix.intCastLieHom_mulVec_mem_coordinateLattice: a coerced integer matrix preserves the integral coordinate lattice.

References

• J. E. Humphreys, Introduction to Lie Algebras and Representation Theory, §§18 and 26.
• J. C. Jantzen, Representations of Algebraic Groups, II.1.

Entrywise coercion of integer matrices

noncomputable def TauCeti.matrixIntCastLieHom {n : Type u_1} [Fintype n] [DecidableEq n] (R : Type u_2) [Ring R] : Matrix n n ℤ →ₗ⁅ℤ⁆ Matrix n n R

Entrywise coercion of integer matrices into a ring, as a homomorphism of Lie rings for the commutator brackets.

Equations

• TauCeti.matrixIntCastLieHom R = (Int.castRingHom R).mapMatrix.toIntAlgHom.toLieHom

@[simp]

theorem TauCeti.matrixIntCastLieHom_apply {n : Type u_1} [Fintype n] [DecidableEq n] (R : Type u_2) [Ring R] (M : Matrix n n ℤ) (a b : n) : (matrixIntCastLieHom R) M a b = ↑(M a b)

Entrywise coercion of integer matrices acts on entries by the integer cast.

theorem TauCeti.matrixIntCastLieHom_eq_map {n : Type u_1} [Fintype n] [DecidableEq n] (R : Type u_2) [Ring R] (M : Matrix n n ℤ) : (matrixIntCastLieHom R) M = M.map Int.cast

Entrywise coercion through matrixIntCastLieHom is the usual matrix map by integer cast.

@[simp]

theorem TauCeti.matrixIntCastLieHom_mul {n : Type u_1} [Fintype n] [DecidableEq n] (R : Type u_2) [Ring R] (M N : Matrix n n ℤ) : (matrixIntCastLieHom R) (M * N) = (matrixIntCastLieHom R) M * (matrixIntCastLieHom R) N

Entrywise coercion of integer matrices is multiplicative, being a ring homomorphism read as a homomorphism of Lie rings.

theorem Matrix.intCastLieHom_mulVec_mem_coordinateLattice {n : Type u_1} [Fintype n] [DecidableEq n] (M : Matrix n n ℤ) {v : n → ℚ} (hv : v ∈ TauCeti.coordinateLattice n) : ((TauCeti.matrixIntCastLieHom ℚ) M).mulVec v ∈ TauCeti.coordinateLattice n

A coerced integer matrix preserves the integral coordinate lattice, each coordinate of the image being an integer combination of the coordinates of the argument.

theorem Matrix.intCast_mulVec_coordinateLatticeBasis_eq_sum {m : Type u_1} {n : Type u_2} [Fintype m] [Fintype n] (M : Matrix m n ℤ) (s : n) : (M.map ⇑(Int.castRingHom ℚ)).mulVec ↑((TauCeti.coordinateLatticeBasis n) s) = ∑ r : m, M r s • ↑((TauCeti.coordinateLatticeBasis m) r)

An integral matrix acts on a coordinate-lattice basis vector by its corresponding column.