The integral matrices of the numbered root generators

Each numbered root generator of the full-weight type-C carrier squares to zero in the standard representation, so its divided-power exponential is 1 + u X for X the integral matrix TauCeti.SpStd.rootIntMatrix of the generator. This file writes that matrix out in the enumerated coordinate basis and reads the root-subgroup points off it.

In the enumerated basis the matrix is the single unit E_{i,m+i} at the final node and the difference E_{i,i+1} - E_{m+i+1,m+i} of two units at a nonfinal one. Those are the matrices of the symplectic group's long-root transvection at the terminal coordinate and of its difference short-root element at an adjacent pair, which is what TauCeti/Algebra/Lie/Symplectic/StandardCarrier/Generation.lean uses to identify the two point groups.

Main results

• TauCeti.SpStd.rootIntMatrix_inl_last and its three siblings: the integral matrix of each numbered root generator, written out.
• TauCeti.SpStd.coe_rootSubgroupPoints_eq_one_add_smul: a root-subgroup point is 1 + u X.

@[simp]

theorem TauCeti.SpStd.rootIntMatrix_inl_last (n : ℕ) : rootIntMatrix n (Sum.inl (Fin.last n)) = Matrix.single (finSumFinEquiv (Sum.inl (Fin.last n))) (finSumFinEquiv (Sum.inr (Fin.last n))) 1

The integral matrix of the final raising generator is a single matrix unit.

@[simp]

theorem TauCeti.SpStd.rootIntMatrix_inr_last (n : ℕ) : rootIntMatrix n (Sum.inr (Fin.last n)) = Matrix.single (finSumFinEquiv (Sum.inr (Fin.last n))) (finSumFinEquiv (Sum.inl (Fin.last n))) 1

The integral matrix of the final lowering generator is a single matrix unit.

@[simp]

theorem TauCeti.SpStd.rootIntMatrix_inl_of_ne_last (n : ℕ) (i : Fin (n + 1)) (hi : i ≠ Fin.last n) : rootIntMatrix n (Sum.inl i) = Matrix.single (finSumFinEquiv (Sum.inl i)) (finSumFinEquiv (Sum.inl (Order.succ i))) 1 - Matrix.single (finSumFinEquiv (Sum.inr (Order.succ i))) (finSumFinEquiv (Sum.inr i)) 1

The integral matrix of a nonfinal raising generator is a difference of two matrix units.

@[simp]

theorem TauCeti.SpStd.rootIntMatrix_inr_of_ne_last (n : ℕ) (i : Fin (n + 1)) (hi : i ≠ Fin.last n) : rootIntMatrix n (Sum.inr i) = Matrix.single (finSumFinEquiv (Sum.inl (Order.succ i))) (finSumFinEquiv (Sum.inl i)) 1 - Matrix.single (finSumFinEquiv (Sum.inr i)) (finSumFinEquiv (Sum.inr (Order.succ i))) 1

The integral matrix of a nonfinal lowering generator is a difference of two matrix units.

theorem TauCeti.SpStd.coe_rootSubgroupPoints_eq_one_add_smul (n : ℕ) (k : Fin (n + 1) ⊕ Fin (n + 1)) (A : Type v) [CommRing A] (u : Multiplicative A) : ↑↑((rootSubgroupPoints n k A) u) = 1 + Multiplicative.toAdd u • (rootIntMatrix n k).map Int.cast

The matrix of a carrier root subgroup point is 1 + u X for the integral matrix X of the corresponding root generator.