Symmetries of the integral root--coroot lattice #
The Chevalley--Demazure construction starts from the integral lattice spanned by a normalized family of root vectors and by the coroots. A symmetry of the pinned Lie algebra does not usually fix those generators pointwise: it permutes the roots and can change both root vectors and coroots by signs. This file proves that these equations preserve the integral root--coroot span exactly.
The result is first stated at the natural module-theoretic level for an arbitrary family of root vectors. It is then specialized to the Lie lattice of a Chevalley system, where the restriction is packaged as an integral Lie algebra automorphism. The characteristic equations say that the restriction and its inverse are the original ambient automorphism and its inverse on underlying vectors.
This is the integral descent step used by the graph-automorphism lane of the pinned
Chevalley--Demazure construction. The signs are essential: graph automorphisms need not carry every
non-simple root vector with sign +1, while both signs are units over ℤ and hence preserve the
lattice.
Main declarations #
TauCeti.map_rootCorootSpan_eq_of_map_root_eq_or_eq_neg: a signed permutation of the root vectors and coroots preserves the integral root--coroot span.TauCeti.rootCorootSpanEquiv: the resulting integral linear automorphism.TauCeti.IsChevalleySystem.chevalleyLieLatticeEquiv: its restriction to the Chevalley Lie lattice as an integral Lie algebra automorphism.
References #
- J. E. Humphreys, Introduction to Lie Algebras and Representation Theory, §§25--27.
- R. W. Carter, Simple Groups of Lie Type, §§4.1 and 12.2.
This advances the pinning and pinned-isomorphism targets of Layer 9 of
TauCetiRoadmap/ReductiveGroups/README.md. Those targets are consumed by milestones L0 and L1 of
TauCetiRoadmap/CFSGStatement/README.md, which require the explicit pinned ambient groups and their
graph automorphisms.
A signed permutation of the root vectors and coroots along the same root permutation preserves the integral root--coroot span.
Both inclusions are recorded: the forward one uses closure under negation, while the reverse one
uses preimages under σ and changes the sign of the source vector when necessary. Thus this is an
equality of integral lattices, not only forward stability.
Membership in the root--coroot span is invariant under a compatible signed root permutation. This is the form used when an ambient automorphism must be shown to preserve an admissible lattice.
This is not a simp lemma: the permutation σ occurs only in the hypotheses, so simp could
never infer it from the left-hand side.
The integral linear automorphism of the root--coroot span induced by a compatible signed permutation of its root vectors and coroots.
Equations
- TauCeti.rootCorootSpanEquiv g σ hroot hcoroot = (LinearEquiv.restrictScalars ℤ g).ofSubmodules (TauCeti.rootCorootSpan x) (TauCeti.rootCorootSpan x) ⋯
Instances For
The restricted integral automorphism acts as the ambient automorphism on underlying vectors.
The inverse restricted integral automorphism acts as the inverse ambient automorphism on underlying vectors.
The ambient Lie automorphism maps the Chevalley Lie lattice onto itself.
Membership in the Chevalley Lie lattice is invariant under the ambient Lie automorphism.
As for map_mem_rootCorootSpan_iff, this is not a simp lemma: simp cannot infer σ from the
left-hand side, which it would in any case rewrite through mem_chevalleyLieLattice_iff.
A compatible signed root permutation restricts to an integral Lie automorphism of the Chevalley lattice. This is the integral automorphism descended from the pinned Lie algebra symmetry.
Equations
- One or more equations did not get rendered due to their size.
Instances For
The restricted integral Lie automorphism acts as the ambient Lie automorphism on underlying vectors.
The inverse restricted integral Lie automorphism acts as the inverse ambient Lie automorphism on underlying vectors.