The full-weight type-B spin carrier

This file specializes the type-Bₙ₊₁ spin representation to the canonical split quadratic space (M* × M) × ℚ, where M = Fin (n + 1) → ℚ. Its exterior coordinate lattice has a basis indexed by Finset (Fin (n + 1)); the simple-root Kostant form preserves this lattice, and the resulting spin weights span the full simply connected character lattice.

These data define an explicit affine group scheme over ℤ: the smallest closed subgroup of GL_(2^(n+1)) containing the represented numbered root subgroups and the spin weight torus. The same data provide its matrix-valued points and the conjugation equation expressing the Cartan action on each numbered root subgroup.

No smoothness, reductivity, Borel subgroup, or comparison with an all-root Kostant form is asserted. In particular, constructing and comparing the remaining nonsimple type-B root subgroups is separate from this carrier construction.

Main declarations

• TauCeti.TypeBSpinCarrier.groupScheme: the full-weight type-B spin carrier over ℤ.
• TauCeti.TypeBSpinCarrier.rootSubgroup: its numbered simple-root subgroup morphisms.
• TauCeti.TypeBSpinCarrier.weightTorus: its closed split weight torus.
• TauCeti.TypeBSpinCarrier.points: its matrix-valued points over a commutative ring.
• TauCeti.TypeBSpinCarrier.weightTorusPoints_conj_rootSubgroupPoints: the torus conjugation equation on matrix-valued points.
• TauCeti.TypeBSpinCarrier.rep_rootGenerator_inl_castSucc and its three siblings: each numbered simple generator acts on the spin module by creation and contraction of exterior coordinates.
• TauCeti.TypeBSpinCarrier.pow_two_rep_rootGenerator_eq_zero: each numbered simple generator squares to zero on the spin module.

References

• C. Chevalley, The Algebraic Theory of Spinors, Chapter II.
• J. E. Humphreys, Introduction to Lie Algebras and Representation Theory, §§25--27.
• N. Bourbaki, Groupes et algèbres de Lie, Chapters 4--6, Plate II.
• TauCeti.Algebra.Lie.Orthogonal.TypeD.SpinCarrier.Basic, for the corresponding type-D carrier. The type-B carrier instead uses the split odd representation, type-B lattice, and type-B root data.

The split spin representation and its lattice

@[reducible, inline]

noncomputable abbrev TauCeti.TypeBSpinCarrier.polarization (n : ℕ) : SpinPolarizationData (splitOddForm ℚ (n + 1))

The canonical split polarization used by the type-Bₙ₊₁ spin carrier.

Equations

• TauCeti.TypeBSpinCarrier.polarization n = TauCeti.splitOddPolarization ℚ (n + 1)

@[reducible, inline]

noncomputable abbrev TauCeti.TypeBSpinCarrier.polarizationBasis (n : ℕ) : Module.Basis (Fin (n + 1)) ℚ ↥(splitOddPolarization ℚ (n + 1)).W

The coordinate basis of the first isotropic summand.

Equations

• TauCeti.TypeBSpinCarrier.polarizationBasis n = TauCeti.splitOddBasis ℚ (n + 1)

@[reducible, inline]

noncomputable abbrev TauCeti.TypeBSpinCarrier.remainderOne (n : ℕ) : ↥(splitOddPolarization ℚ (n + 1)).line

The distinguished norm-one vector in the orthogonal remainder.

Equations

• TauCeti.TypeBSpinCarrier.remainderOne n = TauCeti.splitOddRemainderOne ℚ (n + 1)

@[reducible, inline]

noncomputable abbrev TauCeti.TypeBSpinCarrier.rep (n : ℕ) : UniversalEnvelopingAlgebra ℚ ↥(LieAlgebra.Orthogonal.typeB (Fin (n + 1)) ℚ) →ₐ[ℚ] Module.End ℚ (ExteriorAlgebra ℚ ↥(polarization n).W)

The rational spin representation of the numbered type-Bₙ₊₁ generators.

Equations

• TauCeti.TypeBSpinCarrier.rep n = (TauCeti.TypeBSpinCarrier.polarization n).typeBSpinRep (TauCeti.TypeBSpinCarrier.polarizationBasis n) (TauCeti.TypeBSpinCarrier.remainderOne n) ⋯

@[reducible, inline]

noncomputable abbrev TauCeti.TypeBSpinCarrier.lattice (n : ℕ) : Submodule ℤ (ExteriorAlgebra ℚ ↥(splitOddPolarization ℚ (n + 1)).W)

The integral exterior coordinate lattice in the split spin module.

Equations

• TauCeti.TypeBSpinCarrier.lattice n = TauCeti.ExteriorAlgebra.integralLattice (TauCeti.TypeBSpinCarrier.polarizationBasis n)

@[reducible, inline]

abbrev TauCeti.TypeBSpinCarrier.dimension (n : ℕ) : ℕ

The dimension of the spin module, expressed as the cardinality of its exterior basis.

Equations

• TauCeti.TypeBSpinCarrier.dimension n = Fintype.card (Finset (Fin (n + 1)))

noncomputable def TauCeti.TypeBSpinCarrier.latticeBasis (n : ℕ) : Module.Basis (Fin (dimension n)) ℤ ↥(lattice n).toAddSubgroup

The exterior coordinate basis, reindexed by a finite ordinal for the general-linear carrier.

Equations

• TauCeti.TypeBSpinCarrier.latticeBasis n = (TauCeti.ExteriorAlgebra.integralLatticeBasis (TauCeti.TypeBSpinCarrier.polarizationBasis n)).reindex (Fintype.equivFin (Finset (Fin (n + 1))))

@[reducible, inline]

noncomputable abbrev TauCeti.TypeBSpinCarrier.signSet (n : ℕ) (i : Fin (dimension n)) : Finset (Fin (n + 1))

The sign set represented by a finite-ordinal spin-basis index.

Equations

• TauCeti.TypeBSpinCarrier.signSet n i = (Fintype.equivFin (Finset (Fin (n + 1)))).symm i

@[reducible, inline]

noncomputable abbrev TauCeti.TypeBSpinCarrier.basisWeight (n : ℕ) (i : Fin (dimension n)) : Fin (n + 1) → ℤ

The simply connected type-Bₙ₊₁ weight of a spin-basis vector.

Equations

• TauCeti.TypeBSpinCarrier.basisWeight n i = TauCeti.DynkinType.typeBSpinWeight (TauCeti.TypeBSpinCarrier.signSet n i)

noncomputable def TauCeti.TypeBSpinCarrier.basisReflection (n : ℕ) (i : Fin (n + 1)) (a : Fin (dimension n)) : Fin (dimension n)

The i-th simple reflection on the finite-ordinal spin-basis indices.

Equations

• TauCeti.TypeBSpinCarrier.basisReflection n i a = (Fintype.equivFin (Finset (Fin (n + 1)))) ((TauCeti.DynkinType.typeBSpinReflection i) (TauCeti.TypeBSpinCarrier.signSet n a))

theorem TauCeti.TypeBSpinCarrier.signSet_basisReflection (n : ℕ) (i : Fin (n + 1)) (a : Fin (dimension n)) : signSet n (basisReflection n i a) = (DynkinType.typeBSpinReflection i) (signSet n a)

Enumerating a reflected basis index recovers the reflected sign set.

@[simp]

theorem TauCeti.TypeBSpinCarrier.basisReflection_eq_self_iff (n : ℕ) (i : Fin (n + 1)) (a : Fin (dimension n)) : basisReflection n i a = a ↔ basisWeight n a i = 0

A simple reflection fixes a spin-basis index exactly when its coroot pairing vanishes.

theorem TauCeti.TypeBSpinCarrier.basisReflection_involutive (n : ℕ) (i : Fin (n + 1)) : Function.Involutive (basisReflection n i)

Each simple reflection on enumerated spin-basis indices is an involution.

theorem TauCeti.TypeBSpinCarrier.foldl_basisReflection (n : ℕ) (l : List (Fin (n + 1))) (t : Finset (Fin (n + 1))) : List.foldl (fun (b : Fin (dimension n)) (j : Fin (n + 1)) => basisReflection n j b) ((Fintype.equivFin (Finset (Fin (n + 1)))) t) l = (Fintype.equivFin (Finset (Fin (n + 1)))) (List.foldl (fun (t : Finset (Fin (n + 1))) (j : Fin (n + 1)) => (DynkinType.typeBSpinReflection j) t) t l)

Enumeration transports a sequence of sign-set reflections to basis-index reflections.

@[simp]

theorem TauCeti.TypeBSpinCarrier.coe_latticeBasis (n : ℕ) (i : Fin (dimension n)) : ↑((latticeBasis n) i) = (polarizationBasis n).ExteriorAlgebra (signSet n i)

A reindexed lattice-basis vector is the exterior basis vector of its sign set.

theorem TauCeti.TypeBSpinCarrier.pow_two_rep_rootGenerator_eq_zero (n : ℕ) (k : Fin (n + 1) ⊕ Fin (n + 1)) : (rep n) ((UniversalEnvelopingAlgebra.ι ℚ) (typeBSimpleRootGeneratorFamily k)) ^ 2 = 0

Every represented numbered root generator squares to zero. The simple root strings through the spin weights have length at most two, so no numbered generator raises a weight twice.

theorem TauCeti.TypeBSpinCarrier.isNilpotent_rep_rootGenerator (n : ℕ) (k : Fin (n + 1) ⊕ Fin (n + 1)) : IsNilpotent ((rep n) ((UniversalEnvelopingAlgebra.ι ℚ) (typeBSimpleRootGeneratorFamily k)))

Every represented numbered root generator is nilpotent.

theorem TauCeti.TypeBSpinCarrier.nilpotencyClass_rep_rootGenerator_le_two (n : ℕ) (k : Fin (n + 1) ⊕ Fin (n + 1)) : nilpotencyClass ((rep n) ((UniversalEnvelopingAlgebra.ι ℚ) (typeBSimpleRootGeneratorFamily k))) ≤ 2

Every represented numbered root generator has nilpotency class at most two.

theorem TauCeti.TypeBSpinCarrier.rep_kostantForm_mem_lattice (n : ℕ) (u : UniversalEnvelopingAlgebra ℚ ↥(LieAlgebra.Orthogonal.typeB (Fin (n + 1)) ℚ)) (hu : u ∈ UniversalEnvelopingAlgebra.kostantForm typeBSimpleRootGeneratorFamily typeBSimpleCorootGenerator) (v : ExteriorAlgebra ℚ ↥(polarization n).W) (hv : v ∈ lattice n) : ((rep n) u) v ∈ lattice n

The simple-generator type-B Kostant form preserves the exterior coordinate lattice.

The represented simple generators as exterior operators

theorem TauCeti.TypeBSpinCarrier.rep_rootGenerator_inl_castSucc (n : ℕ) (j : Fin n) (x : ExteriorAlgebra ℚ ↥(polarization n).W) : ((rep n) ((UniversalEnvelopingAlgebra.ι ℚ) (typeBSimpleRootGeneratorFamily (Sum.inl j.castSucc)))) x = (ExteriorAlgebra.ι ℚ) ((polarizationBasis n) j.castSucc) * (CliffordAlgebra.contractLeft ((polarizationBasis n).coord j.succ)) x

A nonterminal raising generator contracts the next exterior coordinate and creates its own.

theorem TauCeti.TypeBSpinCarrier.rep_rootGenerator_inr_castSucc (n : ℕ) (j : Fin n) (x : ExteriorAlgebra ℚ ↥(polarization n).W) : ((rep n) ((UniversalEnvelopingAlgebra.ι ℚ) (typeBSimpleRootGeneratorFamily (Sum.inr j.castSucc)))) x = (ExteriorAlgebra.ι ℚ) ((polarizationBasis n) j.succ) * (CliffordAlgebra.contractLeft ((polarizationBasis n).coord j.castSucc)) x

A nonterminal lowering generator contracts its own exterior coordinate and creates the next one.

theorem TauCeti.TypeBSpinCarrier.rep_rootGenerator_inl_last (n : ℕ) (x : ExteriorAlgebra ℚ ↥(polarization n).W) : ((rep n) ((UniversalEnvelopingAlgebra.ι ℚ) (typeBSimpleRootGeneratorFamily (Sum.inl (Fin.last n))))) x = (ExteriorAlgebra.ι ℚ) ((polarizationBasis n) (Fin.last n)) * CliffordAlgebra.involute x

The terminal raising generator creates the final exterior coordinate after the grade involution.

theorem TauCeti.TypeBSpinCarrier.rep_rootGenerator_inr_last (n : ℕ) (x : ExteriorAlgebra ℚ ↥(polarization n).W) : ((rep n) ((UniversalEnvelopingAlgebra.ι ℚ) (typeBSimpleRootGeneratorFamily (Sum.inr (Fin.last n))))) x = CliffordAlgebra.involute ((CliffordAlgebra.contractLeft ((polarizationBasis n).coord (Fin.last n))) x)

The terminal lowering generator contracts the final exterior coordinate and applies the grade involution.

theorem TauCeti.TypeBSpinCarrier.exists_rep_rootGenerator_inl_exteriorBasis (n : ℕ) (i : Fin (n + 1)) (s t : Finset (Fin (n + 1))) (hs : DynkinType.typeBSpinWeight s i = -1) (ht : (DynkinType.typeBSpinReflection i) s = t) : ∃ (c : ℤˣ), ((rep n) ((UniversalEnvelopingAlgebra.ι ℚ) (typeBSimpleRootGeneratorFamily (Sum.inl i)))) ((polarizationBasis n).ExteriorAlgebra s) = c • (polarizationBasis n).ExteriorAlgebra t

A positive numbered simple root generator moves an exterior basis vector whose spin weight pairs to -1 with the simple coroot to the basis vector of the reflected sign set, up to sign.

theorem TauCeti.TypeBSpinCarrier.exists_rep_rootGenerator_inr_exteriorBasis (n : ℕ) (i : Fin (n + 1)) (s t : Finset (Fin (n + 1))) (hs : DynkinType.typeBSpinWeight s i = 1) (ht : (DynkinType.typeBSpinReflection i) s = t) : ∃ (c : ℤˣ), ((rep n) ((UniversalEnvelopingAlgebra.ι ℚ) (typeBSimpleRootGeneratorFamily (Sum.inr i)))) ((polarizationBasis n).ExteriorAlgebra s) = c • (polarizationBasis n).ExteriorAlgebra t

A negative numbered simple root generator moves an exterior basis vector whose spin weight pairs to 1 with the simple coroot to the basis vector of the reflected sign set, up to sign.

theorem TauCeti.TypeBSpinCarrier.isCartanWeightVector_latticeBasis (n : ℕ) (i : Fin (dimension n)) : UniversalEnvelopingAlgebra.IsCartanWeightVector typeBSimpleCorootGenerator (rep n) (basisWeight n i) ↑((latticeBasis n) i)

Every exterior basis vector has its named integral type-B spin weight.

theorem TauCeti.TypeBSpinCarrier.span_range_basisWeight_eq_top (n : ℕ) : Submodule.span ℤ (Set.range (basisWeight n)) = ⊤

The full spin weights span the simply connected type-B character lattice.

theorem TauCeti.TypeBSpinCarrier.isSl2Triple_rep_rootGenerator (n : ℕ) (i : Fin (n + 1)) : IsSl2Triple ((rep n) ((UniversalEnvelopingAlgebra.ι ℚ) (typeBSimpleCorootGenerator i))) ((rep n) ((UniversalEnvelopingAlgebra.ι ℚ) (typeBSimpleRootGeneratorFamily (Sum.inl i)))) ((rep n) ((UniversalEnvelopingAlgebra.ι ℚ) (typeBSimpleRootGeneratorFamily (Sum.inr i))))

The represented positive and negative simple generators at a common type-B node, together with the represented simple coroot, form an sl_2 triple.

The closed carrier and its pinned generators

noncomputable def TauCeti.TypeBSpinCarrier.definingIdeal (n : ℕ) : HopfIdeal ℤ ↑(GeneralLinear.coordinateHopfAlgebra ℤ (dimension n))

The Hopf ideal cutting out the full-weight type-Bₙ₊₁ spin carrier.

Equations

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

theorem TauCeti.TypeBSpinCarrier.definingIdeal_def (n : ℕ) : definingIdeal n = UniversalEnvelopingAlgebra.kostantToralDefiningIdeal typeBSimpleRootGeneratorFamily typeBSimpleCorootGenerator (rep n) (lattice n).toAddSubgroup ⋯ ⋯ (latticeBasis n) (basisWeight n)

The type-Bₙ₊₁ carrier ideal is the generic Kostant toral-closure ideal specialized to the spin representation and its exterior coordinate lattice.

noncomputable def TauCeti.TypeBSpinCarrier.groupScheme (n : ℕ) : CategoryTheory.Grp (CategoryTheory.Over (AlgebraicGeometry.Spec ↧ℤ))

The full-weight type-Bₙ₊₁ spin carrier over ℤ.

Equations

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

theorem TauCeti.TypeBSpinCarrier.groupScheme_def (n : ℕ) : groupScheme n = CommHopfAlgCat.quotientSpec (GeneralLinear.coordinateHopfAlgebra ℤ (dimension n)) (definingIdeal n)

The quotient-spectrum presentation of the type-Bₙ₊₁ spin carrier.

theorem TauCeti.TypeBSpinCarrier.groupScheme_eq_kostantToralGroupScheme (n : ℕ) : groupScheme n = UniversalEnvelopingAlgebra.kostantToralGroupScheme typeBSimpleRootGeneratorFamily typeBSimpleCorootGenerator (rep n) (lattice n).toAddSubgroup ⋯ ⋯ (latticeBasis n) (basisWeight n)

The type-Bₙ₊₁ carrier is the generic Kostant toral closure for its spin representation.

noncomputable def TauCeti.TypeBSpinCarrier.carrierι (n : ℕ) : groupScheme n ⟶ GeneralLinear.groupScheme ℤ (dimension n)

The canonical inclusion of the type-Bₙ₊₁ spin carrier into its general-linear carrier.

Equations

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

instance TauCeti.TypeBSpinCarrier.isClosedImmersion_carrierι (n : ℕ) : AlgebraicGeometry.IsClosedImmersion (CategoryTheory.Over.Hom.left (carrierι n).hom.hom)

The spin carrier is a closed subgroup scheme of its ambient general linear group.

noncomputable def TauCeti.TypeBSpinCarrier.rootSubgroup (n : ℕ) (k : Fin (n + 1) ⊕ Fin (n + 1)) : AdditiveGroup.groupScheme ℤ ⟶ groupScheme n

A positive or negative numbered simple-root subgroup of the spin carrier.

Equations

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

theorem TauCeti.TypeBSpinCarrier.rootSubgroup_def (n : ℕ) (k : Fin (n + 1) ⊕ Fin (n + 1)) : rootSubgroup n k = CategoryTheory.CategoryStruct.comp (UniversalEnvelopingAlgebra.kostantRootSubgroupToToral typeBSimpleRootGeneratorFamily typeBSimpleCorootGenerator (rep n) (lattice n).toAddSubgroup ⋯ ⋯ (latticeBasis n) (basisWeight n) k) (CategoryTheory.eqToHom ⋯)

The root subgroup is the generic Kostant root subgroup transported to the type-Bₙ₊₁ carrier.

@[simp]

theorem TauCeti.TypeBSpinCarrier.rootSubgroup_comp_carrierι (n : ℕ) (k : Fin (n + 1) ⊕ Fin (n + 1)) : CategoryTheory.CategoryStruct.comp (rootSubgroup n k) (carrierι n) = UniversalEnvelopingAlgebra.kostantRootSubgroup typeBSimpleRootGeneratorFamily typeBSimpleCorootGenerator (rep n) (lattice n).toAddSubgroup ⋯ k ⋯ (latticeBasis n)

Including a root subgroup into the ambient general linear group gives its exponential.

noncomputable def TauCeti.TypeBSpinCarrier.weightTorus (n : ℕ) : SplitTorus.groupScheme ℤ (Fin (n + 1)) ⟶ groupScheme n

The represented split weight torus in the type-Bₙ₊₁ spin carrier.

Equations

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

theorem TauCeti.TypeBSpinCarrier.weightTorus_def (n : ℕ) : weightTorus n = CategoryTheory.CategoryStruct.comp (UniversalEnvelopingAlgebra.kostantWeightTorusToToral typeBSimpleRootGeneratorFamily typeBSimpleCorootGenerator (rep n) (lattice n).toAddSubgroup ⋯ ⋯ (latticeBasis n) (basisWeight n)) (CategoryTheory.eqToHom ⋯)

The weight torus is the generic factored Kostant torus transported to the type-Bₙ₊₁ carrier.

@[simp]

theorem TauCeti.TypeBSpinCarrier.weightTorus_comp_carrierι (n : ℕ) : CategoryTheory.CategoryStruct.comp (weightTorus n) (carrierι n) = GeneralLinear.weightTorus (basisWeight n)

Including the weight torus recovers the diagonal torus of spin weights.

instance TauCeti.TypeBSpinCarrier.isClosedImmersion_weightTorus (n : ℕ) : AlgebraicGeometry.IsClosedImmersion (CategoryTheory.Over.Hom.left (weightTorus n).hom.hom)

The full spin weights make the represented torus a closed subgroup scheme.

theorem TauCeti.TypeBSpinCarrier.groupScheme_hom_ext (n : ℕ) {Y : CommHopfAlgCat ℤ} (f g : groupScheme n ⟶ (AlgebraicGeometry.hopfSpec ↧ℤ).obj (Opposite.op Y)) (hroot : ∀ (k : Fin (n + 1) ⊕ Fin (n + 1)), CategoryTheory.CategoryStruct.comp (rootSubgroup n k) f = CategoryTheory.CategoryStruct.comp (rootSubgroup n k) g) (htorus : CategoryTheory.CategoryStruct.comp (weightTorus n) f = CategoryTheory.CategoryStruct.comp (weightTorus n) g) : f = g

Morphisms out of the carrier agree on its root subgroups and weight torus.

theorem TauCeti.TypeBSpinCarrier.groupScheme_hom_ext_iff {n : ℕ} {Y : CommHopfAlgCat ℤ} {f g : groupScheme n ⟶ (AlgebraicGeometry.hopfSpec ↧ℤ).obj (Opposite.op Y)} : f = g ↔ (∀ (k : Fin (n + 1) ⊕ Fin (n + 1)), CategoryTheory.CategoryStruct.comp (rootSubgroup n k) f = CategoryTheory.CategoryStruct.comp (rootSubgroup n k) g) ∧ CategoryTheory.CategoryStruct.comp (weightTorus n) f = CategoryTheory.CategoryStruct.comp (weightTorus n) g

Matrix-valued points

noncomputable def TauCeti.TypeBSpinCarrier.points (n : ℕ) (A : Type v) [CommRing A] : Subgroup (GL (Fin (dimension n)) A)

The matrix-valued points of the type-Bₙ₊₁ spin carrier.

Equations

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

theorem TauCeti.TypeBSpinCarrier.points_def (n : ℕ) (A : Type v) [CommRing A] : points n A = GeneralLinear.hopfIdealPointsSubgroup (dimension n) (definingIdeal n) A

The carrier points are exactly the matrices cut out by the defining Hopf ideal.

@[simp]

theorem TauCeti.TypeBSpinCarrier.mem_points_iff (n : ℕ) (A : Type v) [CommRing A] (g : GL (Fin (dimension n)) A) : g ∈ points n A ↔ ∀ x ∈ definingIdeal n, ((GeneralLinear.pointsMulEquiv (dimension n)).symm g).ofConv x = 0

A matrix is a carrier point exactly when its associated convolution point kills the defining Hopf ideal.

noncomputable def TauCeti.TypeBSpinCarrier.rootSubgroupPoints (n : ℕ) (k : Fin (n + 1) ⊕ Fin (n + 1)) (A : Type v) [CommRing A] : Multiplicative A →* ↥(points n A)

A numbered root-subgroup homomorphism on matrix-valued points.

Equations

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

@[simp]

theorem TauCeti.TypeBSpinCarrier.coe_rootSubgroupPoints (n : ℕ) (k : Fin (n + 1) ⊕ Fin (n + 1)) (A : Type v) [CommRing A] (u : Multiplicative A) : ↑((rootSubgroupPoints n k A) u) = (UniversalEnvelopingAlgebra.kostantRootSubgroupMatrix typeBSimpleRootGeneratorFamily typeBSimpleCorootGenerator (rep n) (lattice n).toAddSubgroup ⋯ k ⋯ (latticeBasis n)) (AdditiveGroup.gaPointsMulEquiv.symm u)

A numbered root-subgroup point is its represented divided-power exponential matrix.

noncomputable def TauCeti.TypeBSpinCarrier.weightTorusPoints (n : ℕ) (A : Type v) [CommRing A] : (Fin (n + 1) → Aˣ) →* ↥(points n A)

The split spin weight torus on matrix-valued carrier points.

Equations

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

@[simp]

theorem TauCeti.TypeBSpinCarrier.coe_weightTorusPoints (n : ℕ) (A : Type v) [CommRing A] (s : Fin (n + 1) → Aˣ) : ↑((weightTorusPoints n A) s) = (UniversalEnvelopingAlgebra.kostantTorusMatrix (lattice n).toAddSubgroup (latticeBasis n) (basisWeight n)) s

A weight-torus point is the diagonal matrix obtained by evaluating each spin weight.

The Cartan action and pinning equation

def TauCeti.TypeBSpinCarrier.rootWeight (n : ℕ) : Fin (n + 1) ⊕ Fin (n + 1) → Fin (n + 1) → ℤ

The Cartan weight of a positive or negative numbered simple-root generator.

Equations

• TauCeti.TypeBSpinCarrier.rootWeight n (Sum.inl i) = CartanMatrix.B (n + 1) i
• TauCeti.TypeBSpinCarrier.rootWeight n (Sum.inr i) = -CartanMatrix.B (n + 1) i

@[simp]

theorem TauCeti.TypeBSpinCarrier.rootWeight_inl (n : ℕ) (i : Fin (n + 1)) : rootWeight n (Sum.inl i) = CartanMatrix.B (n + 1) i

The weight of a positive numbered simple-root generator is its row of the Cartan matrix.

@[simp]

theorem TauCeti.TypeBSpinCarrier.rootWeight_inr (n : ℕ) (i : Fin (n + 1)) : rootWeight n (Sum.inr i) = -CartanMatrix.B (n + 1) i

The weight of a negative numbered simple-root generator is the negated Cartan row.

theorem TauCeti.TypeBSpinCarrier.lie_coroot_rootGenerator (n : ℕ) (k : Fin (n + 1) ⊕ Fin (n + 1)) (j : Fin (n + 1)) : ⁅typeBSimpleCorootGenerator j, typeBSimpleRootGeneratorFamily k⁆ = ↑(rootWeight n k j) • typeBSimpleRootGeneratorFamily k

Each numbered root generator is a weight vector for the simple coroots.

@[simp]

theorem TauCeti.TypeBSpinCarrier.weightTorusPoints_conj_rootSubgroupPoints (n : ℕ) (k : Fin (n + 1) ⊕ Fin (n + 1)) (A : Type v) [CommRing A] (s : Fin (n + 1) → Aˣ) (u : Multiplicative A) : (weightTorusPoints n A) s * (rootSubgroupPoints n k A) u * ((weightTorusPoints n A) s)⁻¹ = (rootSubgroupPoints n k A) (Multiplicative.ofAdd (↑(torusCharacter s (rootWeight n k)) * Multiplicative.toAdd u))

Conjugation by the spin weight torus rescales each root-subgroup parameter by its root character, on matrix-valued points.

@[simp]

theorem TauCeti.TypeBSpinCarrier.weightTorus_conj_rootSubgroup (n : ℕ) (k : Fin (n + 1) ⊕ Fin (n + 1)) (A : Type) [CommRing A] (s : (AlgebraicGeometry.Spec ↧A).asOver (AlgebraicGeometry.Spec ↧ℤ) ⟶ (SplitTorus.groupScheme ℤ (Fin (n + 1))).X) (u : A) : CategoryTheory.CategoryStruct.comp s (weightTorus n).hom.hom * CategoryTheory.CategoryStruct.comp ((AdditiveGroup.groupSchemePointMulEquiv A) (AdditiveGroup.gaPointsMulEquiv.symm (Multiplicative.ofAdd u))) (rootSubgroup n k).hom.hom * (CategoryTheory.CategoryStruct.comp s (weightTorus n).hom.hom)⁻¹ = CategoryTheory.CategoryStruct.comp ((AdditiveGroup.schemePointsMulEquiv A).symm (Multiplicative.ofAdd (↑(torusCharacter (SplitTorus.schemePointsMulEquiv s) (rootWeight n k)) * u))) (rootSubgroup n k).hom.hom

Conjugation by the spin weight torus rescales each root subgroup by its root character.

Identification with the named simple roots

theorem TauCeti.TypeBSpinCarrier.rootWeight_inl_eq_root_simpleIndex (n : ℕ) (ht : (DynkinType.B (n + 1)).Valid) (i : Fin (n + 1)) : rootWeight n (Sum.inl i) = ((DynkinType.B (n + 1)).simplyConnectedRootDatum ht).root ((DynkinType.B (n + 1)).simpleIndex ht i)

The raising-generator weight is the corresponding simple root of the uniform pinned type-Bₙ₊₁ datum.

theorem TauCeti.TypeBSpinCarrier.rootWeight_inr_eq_neg_root_simpleIndex (n : ℕ) (ht : (DynkinType.B (n + 1)).Valid) (i : Fin (n + 1)) : rootWeight n (Sum.inr i) = -((DynkinType.B (n + 1)).simplyConnectedRootDatum ht).root ((DynkinType.B (n + 1)).simpleIndex ht i)

The lowering-generator weight is the negative of the corresponding pinned simple root.

theorem TauCeti.TypeBSpinCarrier.weightTorusPoints_conj_rootSubgroupPoints_root_simpleIndex (n : ℕ) (ht : (DynkinType.B (n + 1)).Valid) (i : Fin (n + 1)) (A : Type v) [CommRing A] (s : Fin (n + 1) → Aˣ) (u : Multiplicative A) : (weightTorusPoints n A) s * (rootSubgroupPoints n (Sum.inl i) A) u * ((weightTorusPoints n A) s)⁻¹ = (rootSubgroupPoints n (Sum.inl i) A) (Multiplicative.ofAdd (↑(torusCharacter s (((DynkinType.B (n + 1)).simplyConnectedRootDatum ht).root ((DynkinType.B (n + 1)).simpleIndex ht i))) * Multiplicative.toAdd u))

On matrix-valued points, the i-th raising subgroup transforms through the i-th simple root of the pinned type-Bₙ₊₁ datum.

theorem TauCeti.TypeBSpinCarrier.weightTorusPoints_conj_rootSubgroupPoints_neg_root_simpleIndex (n : ℕ) (ht : (DynkinType.B (n + 1)).Valid) (i : Fin (n + 1)) (A : Type v) [CommRing A] (s : Fin (n + 1) → Aˣ) (u : Multiplicative A) : (weightTorusPoints n A) s * (rootSubgroupPoints n (Sum.inr i) A) u * ((weightTorusPoints n A) s)⁻¹ = (rootSubgroupPoints n (Sum.inr i) A) (Multiplicative.ofAdd (↑(torusCharacter s (-((DynkinType.B (n + 1)).simplyConnectedRootDatum ht).root ((DynkinType.B (n + 1)).simpleIndex ht i))) * Multiplicative.toAdd u))

On matrix-valued points, the i-th lowering subgroup transforms through the negative of the i-th pinned simple root.

theorem TauCeti.TypeBSpinCarrier.weightTorus_conj_rootSubgroup_root_simpleIndex (n : ℕ) (ht : (DynkinType.B (n + 1)).Valid) (i : Fin (n + 1)) (A : Type) [CommRing A] (s : (AlgebraicGeometry.Spec ↧A).asOver (AlgebraicGeometry.Spec ↧ℤ) ⟶ (SplitTorus.groupScheme ℤ (Fin (n + 1))).X) (u : A) : CategoryTheory.CategoryStruct.comp s (weightTorus n).hom.hom * CategoryTheory.CategoryStruct.comp ((AdditiveGroup.groupSchemePointMulEquiv A) (AdditiveGroup.gaPointsMulEquiv.symm (Multiplicative.ofAdd u))) (rootSubgroup n (Sum.inl i)).hom.hom * (CategoryTheory.CategoryStruct.comp s (weightTorus n).hom.hom)⁻¹ = CategoryTheory.CategoryStruct.comp ((AdditiveGroup.schemePointsMulEquiv A).symm (Multiplicative.ofAdd (↑(torusCharacter (SplitTorus.schemePointsMulEquiv s) (((DynkinType.B (n + 1)).simplyConnectedRootDatum ht).root ((DynkinType.B (n + 1)).simpleIndex ht i))) * u))) (rootSubgroup n (Sum.inl i)).hom.hom

The i-th raising subgroup transforms through the i-th simple root on scheme points.

theorem TauCeti.TypeBSpinCarrier.weightTorus_conj_rootSubgroup_neg_root_simpleIndex (n : ℕ) (ht : (DynkinType.B (n + 1)).Valid) (i : Fin (n + 1)) (A : Type) [CommRing A] (s : (AlgebraicGeometry.Spec ↧A).asOver (AlgebraicGeometry.Spec ↧ℤ) ⟶ (SplitTorus.groupScheme ℤ (Fin (n + 1))).X) (u : A) : CategoryTheory.CategoryStruct.comp s (weightTorus n).hom.hom * CategoryTheory.CategoryStruct.comp ((AdditiveGroup.groupSchemePointMulEquiv A) (AdditiveGroup.gaPointsMulEquiv.symm (Multiplicative.ofAdd u))) (rootSubgroup n (Sum.inr i)).hom.hom * (CategoryTheory.CategoryStruct.comp s (weightTorus n).hom.hom)⁻¹ = CategoryTheory.CategoryStruct.comp ((AdditiveGroup.schemePointsMulEquiv A).symm (Multiplicative.ofAdd (↑(torusCharacter (SplitTorus.schemePointsMulEquiv s) (-((DynkinType.B (n + 1)).simplyConnectedRootDatum ht).root ((DynkinType.B (n + 1)).simpleIndex ht i))) * u))) (rootSubgroup n (Sum.inr i)).hom.hom

The i-th lowering subgroup transforms through the negative pinned simple root on scheme points.