Keyboard shortcuts

Press ← or → to navigate between chapters

Press ? to show this help

Press Esc to hide this help

Complete Support for Toral Character Triples

Abstract

Exactly C₂ × C₆ supports faithful pointwise projective character matches without a global match in the stated cyclic-product family.

Definition 1.1 (Actual character triples).

Formalization. D5/S3/FiniteGroups/ToralCharacterSupport.Triple (✓ std3).

Source. Repository-derived.

Commentary.

A triple is a function from Fin 3 to the homomorphisms G →* ℂˣ. The coordinates are actual complex-unit characters, indexed by 0, 1 and 2. Character multiplication below is pointwise multiplication.

Definition 1.2 (Trivial projective kernel).

Formalization. D5/S3/FiniteGroups/ToralCharacterSupport.ProjectivelyFaithful (✓ std3).

Source. Repository-derived.

Commentary.

A triple is projectively faithful when the only group element at which all three coordinate values coincide is the identity. Equivalently, the kernels of the two ratios X₁/X₀ and X₂/X₀ intersect trivially.

Definition 1.3 (A scalar and permutation at each element).

Formalization. D5/S3/FiniteGroups/ToralCharacterSupport.PointwiseMatched (✓ std3).

Source. Repository-derived.

Commentary.

For every element g, a nonzero complex scalar and a permutation match the three values. Both choices may depend on g. The definition permits equal coordinate values and repeated characters.

Definition 1.4 (One character and one permutation).

Formalization. D5/S3/FiniteGroups/ToralCharacterSupport.GloballyMatched (✓ std3).

Source. Repository-derived.

Commentary.

A global match uses one homomorphism G →* ℂˣ and one permutation of Fin 3 for all elements. The displayed equalities are equalities of characters.

Definition 1.5 (The support predicate).

Formalization. D5/S3/FiniteGroups/ToralCharacterSupport.Supports (✓ std3).

Source. Repository-derived.

Commentary.

Support requires two projectively faithful triples, pointwise matching, and the absence of a global match. No normalization or compatibility hypothesis is included in this predicate.

Definition 1.6 (The actual source groups).

Formalization. D5/S3/FiniteGroups/ToralCharacterSupport.Source (✓ std3).

Source. Repository-derived.

Commentary.

Cyclic n is the existing CyclicPrimePowerAction.Cyclic abbreviation for Multiplicative (ZMod n). For positive n this is a cyclic group of order n; Cyclic 1 is trivial. Source a b m is their actual direct product. The complete support theorem assumes a ≤ b, positive m and odd m.

Theorem 1.7 (The complete support classification).

Proof. Machine-checked in Lean as D5/S3/FiniteGroups/ToralCharacterSupport.support_iff (✓ std3). ∎

Source. Repository-derived.

Commentary.

For every natural a, b and m with a ≤ b and positive odd m, Source a b m supports the specified pairs exactly when a=b=1 and m=3. The statement quantifies over all actual character triples through Supports. It includes a=0, trivial factors, m=1, repeated eigenvalues, and every higher power of two.

When a=0 the source is cyclic. Match at a generator and choose the twisting character as a quotient of two coordinate characters. Equality at the generator gives equality everywhere, including for the trivial group. For a≥1, the Chinese remainder equivalence ZMod.chineseRemainder gives Source a b m ≃ (Cyclic (2^a) × Cyclic (2^b)) × Cyclic m. Support is transported along this actual group equivalence.

Write P=Cyclic (2^a) × Cyclic (2^b) and O=Cyclic m. On P, a matching scalar has order dividing 2^b and its cube is the determinant quotient. Inverting 3 modulo 2^b therefore constructs a single character twist removing these scalars. A faithful triple on a noncyclic finite group has distinct coordinate characters: equality of two coordinates would make a remaining ratio an injective character into a finite cyclic group of roots of unity. The pinned linearIndependent_monoidHom theorem then turns equality of character sums into one permutation aligning the restrictions on P.

After this alignment, at every mixed element (p,o) the matching scalar has order dividing 2^b m. Its cube has order dividing m, because the determinant quotient is trivial on P. Coprimality forces its mth power to be one. Taking mth powers in each coordinate equality and using coprimality again proves that the pointwise permutation preserves the three values on P. These conclusions hold for every odd m.

If b≥2, P is noncyclic and has an element whose square is nonidentity. Faithfulness implies that one of the coordinate ratios has a value whose square is nonidentity. Three successive translates give three distinct values, so one avoids any two forbidden values. Applying this observation to the two ratios constructs one element p₀ on which the three coordinate values are distinct. At every (p₀,o), preservation of those values forces the permutation to be the identity. The odd-factor coordinate quotients consequently agree, supplying a global twisting character. This excludes all b≥2 for every odd m directly.

The remaining noncyclic primary group is C₂². Its faithful ratio map to μ₂ × μ₂ is injective and both groups have four elements, hence it is surjective. This supplies each singleton sign pattern. At an odd cyclic generator, a permitted permutation fixing the singleton is the identity or the complementary transposition. The identity would give a global match. After twisting the first odd coordinate to one, the transpositions for singleton coordinates 0 and 1 force both remaining coordinate values to have cube one. Faithfulness makes the generator’s cube the identity, so m divides 3. For m=1 alignment already gives a global match, leaving precisely m=3.

For sufficiency use Γ=(μ₂ × μ₂) × μ₃ and the actual characters X(s,t,z)=(1,sz,tz⁻¹) and Y(s,t,z)=(1,sz⁻¹,tz). Their projective kernels are trivial since μ₂∩μ₃={1}. When s=t, interchange coordinates 1 and 2 with scalar one. When (s,t)=(1,−1), interchange coordinates 0 and 1 with scalar z⁻¹; when (s,t)=(−1,1), interchange coordinates 0 and 2 with scalar z. These exhaust the sign patterns. A global twist is trivial on μ₂² by its square and cube constraints; the distinct restricted characters force its permutation to be the identity. The first coordinate then forces the whole twist to be trivial, which would identify z and z⁻¹ for every cube root, contradicting that μ₃ has three elements. Cyclic/root-of-unity equivalences transport this pair to Source 1 1 3.

References