Keyboard shortcuts

Press ← or → to navigate between chapters

Press ? to show this help

Press Esc to hide this help

Finite-group orbit fixed lines and orbit count

Abstract

Finite-group orbit spans have orbit-sum fixed lines, with rank equal to orbit count.

A finite group acting through linear equivalences on linearly independent indexed orbits has a fixed subspace generated by one orbit sum per orbit. This turns group action into an exact finite-dimensional count for charged lattice orbit sectors; it does not identify a whole C2 quotient.

Theorem 1.1 (The fixed orbit submodule is the orbit-sum line).

Lean statement: D5/S3/VertexAlgebra/Lattice/FiniteGroupOrbitFixedLine.fixedOrbit_eq_span_orbitSum

Proof. Machine-checked in Lean. ∎

Source. Repository-derived.

Commentary.

The hypotheses give a finite group, a representation by invertible linear maps, permutation of the indexed orbit, and linear independence of the orbit vectors. The conclusion is an equality of submodules: the intersection of the orbit span with the representation fixed submodule equals the span of the finite orbit sum.

Theorem 1.2 (The orbit sum is nonzero).

Lean statement: D5/S3/VertexAlgebra/Lattice/FiniteGroupOrbitFixedLine.orbitSum_ne_zero

Proof. Machine-checked in Lean. ∎

Commentary.

Linear independence of the orbit vectors makes the all-one finite linear combination nonzero. Thus the fixed submodule identified above is a genuine one-dimensional line.

Theorem 1.3 (The fixed space is spanned by one sum per independent orbit).

Lean statement: D5/S3/VertexAlgebra/Lattice/FiniteGroupOrbitFixedLine.multiOrbitFixed_eq_span_sums

Proof. Machine-checked in Lean. ∎

Source. Repository-derived.

Commentary.

For a finite family of linearly independent G-orbits, the coefficient-shift argument forces each invariant coefficient function to be constant along its orbit. The fixed submodule is therefore exactly the span of the corresponding orbit sums.

Theorem 1.4 (The fixed-space rank equals the orbit count).

Lean statement: D5/S3/VertexAlgebra/Lattice/FiniteGroupOrbitFixedLine.multiOrbitFixed_finrank_eq_card

Proof. Machine-checked in Lean. ∎

Source. Repository-derived.

Commentary.

The orbit sums remain linearly independent because the original orbit vectors are independent and have disjoint index supports. Consequently the invariant submodule has dimension exactly the cardinality of the orbit index type, including in characteristics dividing the group order.

References