The rank-two spin carrier is the rank-two symplectic carrier

The diagrams B₂ and C₂ are the same, and the spin representation of Spin₅ is the standard representation of Sp₄. This file makes the corresponding statement about the two explicit carriers Tau Ceti builds for that diagram: the full-weight type-B spin carrier TauCeti.TypeBSpinCarrier.groupScheme 1, built on the exterior algebra of a rank-two isotropic space, and the full-weight type-C standard carrier TauCeti.SpStd.groupScheme 1, built on the four-dimensional symplectic module. A signed permutation of the two four-element lattice bases conjugates the numbered simple root subgroups of the first onto those of the second and the weight torus of the first onto the weight torus of the second, so conjugation by it identifies the two carriers' points over every commutative ring.

Both carriers use the Bourbaki numbering of their own diagram, which disagree: node 0 of B₂ is the long simple root ε₀ - ε₁ and node 1 the short one ε₁, while node 0 of C₂ is the short root and node 1 the long one. The identification therefore exchanges the two nodes, both on the root subgroups and on the coordinates of the weight torus. In the exterior basis indexed by subsets of {0, 1} and the symplectic basis e₀, e₁, f₀, f₁, the change of basis is

{0, 1} ↦ e₀,    {0} ↦ e₁,    {1} ↦ f₁,    ∅ ↦ -f₀,

which carries each spin weight to the corresponding symplectic weight with its two coordinates exchanged. The spin lattice basis is enumerated by Fin (dimension 1), which is Fin 4 only after computing dimension 1, so the identification first reindexes along TauCeti.TypeBSpinCarrier.dimension_one and then conjugates.

Nothing here asserts that either carrier is the pinned simply connected group scheme of its diagram.

Main definitions

• TauCeti.TypeBSpinCarrier.rankTwoRootMatrix and TauCeti.TypeBSpinCarrier.rankTwoRootIntMatrix: the integral matrices of the four numbered simple root generators on the rank-two exterior basis and on the enumerated lattice basis.
• TauCeti.TypeBSpinCarrier.symplecticNode and TauCeti.TypeBSpinCarrier.symplecticRootIndex: the exchange of the two nodes, from the B₂ numbering of the spin carrier to the C₂ numbering of the symplectic carrier.
• TauCeti.TypeBSpinCarrier.symplecticBasisChange and TauCeti.TypeBSpinCarrier.symplecticChangeOfBasis: the signed permutation matrix above, on the unenumerated and on the enumerated coordinates.
• TauCeti.TypeBSpinCarrier.pointsMulEquivSymplecticPoints: the resulting identification of the rank-two spin carrier points with the rank-two symplectic carrier points.

Main results

• TauCeti.TypeBSpinCarrier.rep_rootGenerator_exteriorBasis_rankTwo: the action of the numbered simple root generators on the rank-two exterior basis.
• TauCeti.TypeBSpinCarrier.coe_rootSubgroupPoints_eq_one_add_smul_rankTwo: each root subgroup point of the rank-two spin carrier is 1 + u X for the integral generator matrix X.
• TauCeti.TypeBSpinCarrier.coe_pointsMulEquivSymplecticPoints_apply: the identification is conjugation by the change of basis, after reindexing the four spin coordinates.
• TauCeti.TypeBSpinCarrier.pointsMulEquivSymplecticPoints_rootSubgroupPoints and TauCeti.TypeBSpinCarrier.pointsMulEquivSymplecticPoints_weightTorusPoints: the identification carries the numbered root subgroups and the weight torus of the spin carrier to those of the symplectic carrier, exchanging the two nodes.
• TauCeti.TypeBSpinCarrier.pointsMulEquivSymplecticPoints_frobenius: the identification commutes with the Frobenius maps of the two carriers.

References

• C. Chevalley, The Algebraic Theory of Spinors, Chapter II.
• N. Bourbaki, Lie Groups and Lie Algebras, Chapters 4--6, Plates II and III.
• R. W. Carter, Simple Groups of Lie Type, §§11.3 and 13.4.

The generators on the rank-two exterior basis

def TauCeti.TypeBSpinCarrier.rankTwoRootMatrix : Fin (1 + 1) ⊕ Fin (1 + 1) → Matrix (Finset (Fin (1 + 1))) (Finset (Fin (1 + 1))) ℤ

The integral matrices of the numbered simple root generators on the rank-two exterior basis, with rows and columns indexed by subsets of {0, 1}. The long raising generator moves {1} to {0}, the short raising generator moves ∅ to {1} and {0} to {0, 1}, and the lowering generators reverse these moves.

Equations

• TauCeti.TypeBSpinCarrier.rankTwoRootMatrix (Sum.inl 0) = Matrix.single {0} {1} 1
• TauCeti.TypeBSpinCarrier.rankTwoRootMatrix (Sum.inl 1) = Matrix.single {1} ∅ 1 + Matrix.single {0, 1} {0} 1
• TauCeti.TypeBSpinCarrier.rankTwoRootMatrix (Sum.inr 0) = Matrix.single {1} {0} 1
• TauCeti.TypeBSpinCarrier.rankTwoRootMatrix (Sum.inr 1) = Matrix.single ∅ {1} 1 + Matrix.single {0} {0, 1} 1

theorem TauCeti.TypeBSpinCarrier.rep_rootGenerator_exteriorBasis_rankTwo (k : Fin (1 + 1) ⊕ Fin (1 + 1)) (S : Finset (Fin (1 + 1))) : ((rep 1) ((UniversalEnvelopingAlgebra.ι ℚ) (typeBSimpleRootGeneratorFamily k))) ((polarizationBasis 1).ExteriorAlgebra S) = ∑ T : Finset (Fin (1 + 1)), ↑(rankTwoRootMatrix k T S) • (polarizationBasis 1).ExteriorAlgebra T

The numbered simple root generators on the rank-two exterior basis. Each acts on the basis vector indexed by S through the column S of TauCeti.TypeBSpinCarrier.rankTwoRootMatrix.

The generators in the lattice basis

noncomputable def TauCeti.TypeBSpinCarrier.rankTwoRootIntMatrix (k : Fin (1 + 1) ⊕ Fin (1 + 1)) : Matrix (Fin (dimension 1)) (Fin (dimension 1)) ℤ

The integral matrix of a numbered simple root generator of the rank-two spin carrier in the enumerated lattice basis TauCeti.TypeBSpinCarrier.latticeBasis 1.

Equations

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

theorem TauCeti.TypeBSpinCarrier.rootIntMatrix_rankTwo (k : Fin (1 + 1) ⊕ Fin (1 + 1)) : rootIntMatrix 1 k = rankTwoRootIntMatrix k

The general spin-generator matrix specializes to the explicit rank-two matrix.

theorem TauCeti.TypeBSpinCarrier.rep_rootGenerator_latticeBasis_eq_sum_rankTwo (k : Fin (1 + 1) ⊕ Fin (1 + 1)) (s : Fin (dimension 1)) : ((rep 1) ((UniversalEnvelopingAlgebra.ι ℚ) (typeBSimpleRootGeneratorFamily k))) ↑((latticeBasis 1) s) = ∑ r : Fin (dimension 1), rankTwoRootIntMatrix k r s • ↑((latticeBasis 1) r)

A rank-two root generator acts on an enumerated lattice basis vector by its matrix column.

theorem TauCeti.TypeBSpinCarrier.coe_rootSubgroupPoints_eq_one_add_smul_rankTwo (k : Fin (1 + 1) ⊕ Fin (1 + 1)) (A : Type v) [CommRing A] (u : Multiplicative A) : ↑↑((rootSubgroupPoints 1 k A) u) = 1 + Multiplicative.toAdd u • (rankTwoRootIntMatrix k).map Int.cast

Each numbered root subgroup point of the rank-two spin carrier is 1 + u X for X the integral matrix of the corresponding generator.

The change of basis to the symplectic carrier

def TauCeti.TypeBSpinCarrier.symplecticNode : Equiv.Perm (Fin (1 + 1))

The node exchange between the two rank-two numberings. Node 0 of B₂, the long simple root of the spin carrier, is node 1 of C₂, the long simple root of the symplectic carrier, and the short nodes correspond likewise.

Equations

• TauCeti.TypeBSpinCarrier.symplecticNode = Equiv.swap 0 1

def TauCeti.TypeBSpinCarrier.symplecticRootIndex (k : Fin (1 + 1) ⊕ Fin (1 + 1)) : Fin (1 + 1) ⊕ Fin (1 + 1)

The numbered root generator of the symplectic carrier corresponding to a numbered root generator of the spin carrier: raising goes to raising and lowering to lowering, at the exchanged node.

Equations

• TauCeti.TypeBSpinCarrier.symplecticRootIndex k = Sum.map (⇑TauCeti.TypeBSpinCarrier.symplecticNode) (⇑TauCeti.TypeBSpinCarrier.symplecticNode) k

@[simp]

theorem TauCeti.TypeBSpinCarrier.symplecticNode_zero : symplecticNode 0 = 1

@[simp]

theorem TauCeti.TypeBSpinCarrier.symplecticNode_one : symplecticNode 1 = 0

@[simp]

theorem TauCeti.TypeBSpinCarrier.symplecticRootIndex_inl (i : Fin (1 + 1)) : symplecticRootIndex (Sum.inl i) = Sum.inl (symplecticNode i)

@[simp]

theorem TauCeti.TypeBSpinCarrier.symplecticRootIndex_inr (i : Fin (1 + 1)) : symplecticRootIndex (Sum.inr i) = Sum.inr (symplecticNode i)

@[simp]

theorem TauCeti.TypeBSpinCarrier.symplecticRootIndex_symplecticRootIndex (k : Fin (1 + 1) ⊕ Fin (1 + 1)) : symplecticRootIndex (symplecticRootIndex k) = k

The node exchange is an involution on the numbered root generators.

def TauCeti.TypeBSpinCarrier.symplecticBasisChange : Matrix (Fin (1 + 1) ⊕ Fin (1 + 1)) (Finset (Fin (1 + 1))) ℤ

The change of basis from the rank-two exterior basis to the symplectic coordinates, with rows indexed by the symplectic coordinates e₀, e₁, f₀, f₁ and columns by subsets of {0, 1}: {0, 1} ↦ e₀, {0} ↦ e₁, {1} ↦ f₁ and ∅ ↦ -f₀.

Equations

• TauCeti.TypeBSpinCarrier.symplecticBasisChange = Matrix.single (Sum.inl 0) {0, 1} 1 + Matrix.single (Sum.inl 1) {0} 1 + Matrix.single (Sum.inr 1) {1} 1 - Matrix.single (Sum.inr 0) ∅ 1

The identification with the symplectic carrier

theorem TauCeti.TypeBSpinCarrier.dimension_one : dimension 1 = 1 + 1 + (1 + 1)

The rank-two spin module and the rank-two symplectic module both have four basis vectors.

noncomputable def TauCeti.TypeBSpinCarrier.symplecticChangeOfBasis : GL (Fin (1 + 1 + (1 + 1))) ℤ

The change of basis from the spin lattice basis to the symplectic lattice basis, as an invertible integral matrix on the symplectic coordinates: the spin lattice basis is reindexed along TauCeti.TypeBSpinCarrier.dimension_one and then carried to the symplectic basis by TauCeti.TypeBSpinCarrier.symplecticBasisChange. It is a signed permutation matrix, inverted by its transpose.

Equations

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

noncomputable def TauCeti.TypeBSpinCarrier.pointsMulEquivSymplecticPoints (A : Type v) [CommRing A] : ↥(points 1 A) ≃* ↥(SpStd.points 1 A)

The rank-two spin carrier is the rank-two symplectic carrier. Over every commutative ring A, reindexing the spin lattice basis to the symplectic coordinates and conjugating by TauCeti.TypeBSpinCarrier.symplecticChangeOfBasis identifies the points of TauCeti.TypeBSpinCarrier.groupScheme 1 with the points of TauCeti.SpStd.groupScheme 1.

Equations

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

theorem TauCeti.TypeBSpinCarrier.coe_pointsMulEquivSymplecticPoints_apply (A : Type v) [CommRing A] (g : ↥(points 1 A)) : ↑((pointsMulEquivSymplecticPoints A) g) = (Matrix.GeneralLinearGroup.map (algebraMap ℤ A)) symplecticChangeOfBasis * ((finCongr dimension_one).reindexGL A) ↑g * ((Matrix.GeneralLinearGroup.map (algebraMap ℤ A)) symplecticChangeOfBasis)⁻¹

The identification of the rank-two carriers reindexes and conjugates by TauCeti.TypeBSpinCarrier.symplecticChangeOfBasis.

@[simp]

theorem TauCeti.TypeBSpinCarrier.pointsMulEquivSymplecticPoints_rootSubgroupPoints (k : Fin (1 + 1) ⊕ Fin (1 + 1)) (A : Type v) [CommRing A] (u : Multiplicative A) : (pointsMulEquivSymplecticPoints A) ((rootSubgroupPoints 1 k A) u) = (SpStd.rootSubgroupPoints 1 (symplecticRootIndex k) A) u

The identification carries each numbered spin root subgroup to the symplectic root subgroup at the exchanged node, with the same parameter.

@[simp]

theorem TauCeti.TypeBSpinCarrier.pointsMulEquivSymplecticPoints_weightTorusPoints (A : Type v) [CommRing A] (s : Fin (1 + 1) → Aˣ) : (pointsMulEquivSymplecticPoints A) ((weightTorusPoints 1 A) s) = (SpStd.weightTorusPoints 1 A) (s ∘ ⇑symplecticNode)

The identification carries the spin weight torus to the symplectic weight torus, with the two torus coordinates exchanged.

@[simp]

theorem TauCeti.TypeBSpinCarrier.pointsMulEquivSymplecticPoints_frobenius (p k : ℕ) (A : Type v) [CommRing A] [ExpChar A p] (g : ↥(points 1 A)) : (pointsMulEquivSymplecticPoints A) ((frobenius 1 p k A) g) = (SpStd.frobenius 1 p k A) ((pointsMulEquivSymplecticPoints A) g)

The identification commutes with the p ^ k-power Frobenius maps of the two carriers, since the change of basis is integral.