CRT coordinates of the characters of ℤ/12

Under ℤ/12 ≅ ℤ/3 × ℤ/4, the character χ_k = dftChar k (j ↦ exp(2πi·jk/12)) factors through the projection to ℤ/3 exactly when k ∈ {0, 4, 8} and through the projection to ℤ/4 exactly when k ∈ {0, 3, 6, 9}. So χ_4 generates the augmented (ℤ/3) axis, χ_3 the diminished (ℤ/4) axis, and the tritone χ_6 is the element of order 2 of the ℤ/4 part: the indices 3 and 4 swap.

Main results

• dftChar_eq_dftChar_iff: two values of a character agree iff x * k = y * k in ZMod N.
• factorsThrough_three_iff: χ_k factors through ℤ/12 → ℤ/3 iff k ∈ {0, 4, 8}.
• factorsThrough_four_iff: χ_k factors through ℤ/12 → ℤ/4 iff k ∈ {0, 3, 6, 9}.
• three_axis_eq_multiples_four, four_axis_eq_multiples_three, six_order_two: the two axes are generated by 4 and by 3, and 6 has order 2.

References

• C. Marín, The Tonnetz spectrum is the generating triad's Fourier balance profile, Zenodo (2026), doi:10.5281/zenodo.20862821, Proposition 2.

theorem MusicTheory.CRTCharacters.dftChar_eq_dftChar_iff {N : ℕ} [NeZero N] (k x y : ZMod N) : CycleGraphSpectrum.dftChar k x = CycleGraphSpectrum.dftChar k y ↔ x * k = y * k

Two values of the character dftChar k agree iff x * k = y * k: stdAddChar is injective.

def MusicTheory.CRTCharacters.FactorsThrough {M : Type u_1} (f : ZMod 12 → M) (k : ZMod 12) : Prop

The character χ_k of ℤ/12 factors through the map f: it is constant on the fibres of f.

Equations

• MusicTheory.CRTCharacters.FactorsThrough f k = ∀ (x y : ZMod 12), f x = f y → MusicTheory.CycleGraphSpectrum.dftChar k x = MusicTheory.CycleGraphSpectrum.dftChar k y

@[reducible, inline]

abbrev MusicTheory.CRTCharacters.toThree : ZMod 12 →+* ZMod 3

The projection ℤ/12 → ℤ/3.

Equations

• MusicTheory.CRTCharacters.toThree = ZMod.castHom MusicTheory.CRTCharacters.toThree._proof_1 (ZMod 3)

@[reducible, inline]

abbrev MusicTheory.CRTCharacters.toFour : ZMod 12 →+* ZMod 4

The projection ℤ/12 → ℤ/4.

Equations

• MusicTheory.CRTCharacters.toFour = ZMod.castHom MusicTheory.CRTCharacters.toFour._proof_1 (ZMod 4)

theorem MusicTheory.CRTCharacters.factorsThrough_iff {R : Type u_1} [CommRing R] (f : ZMod 12 →+* R) (k : ZMod 12) : FactorsThrough (⇑f) k ↔ ∀ (d : ZMod 12), f d = 0 → d * k = 0

For a ring homomorphism f, χ_k factors through f iff k kills the kernel of f.

theorem MusicTheory.CRTCharacters.factorsThrough_three_iff (k : ZMod 12) : FactorsThrough (⇑toThree) k ↔ k ∈ {0, 4, 8}

Proposition 2, first half. χ_k factors through ℤ/3 iff k ∈ {0, 4, 8}.

theorem MusicTheory.CRTCharacters.factorsThrough_four_iff (k : ZMod 12) : FactorsThrough (⇑toFour) k ↔ k ∈ {0, 3, 6, 9}

Proposition 2, second half. χ_k factors through ℤ/4 iff k ∈ {0, 3, 6, 9}.

theorem MusicTheory.CRTCharacters.three_axis_eq_multiples_four : Finset.image (fun (j : ZMod 12) => j * 4) Finset.univ = {0, 4, 8}

The ℤ/3 axis is generated by 4.

theorem MusicTheory.CRTCharacters.four_axis_eq_multiples_three : Finset.image (fun (j : ZMod 12) => j * 3) Finset.univ = {0, 3, 6, 9}

The ℤ/4 axis is generated by 3.

theorem MusicTheory.CRTCharacters.six_order_two : 6 ≠ 0 ∧ 2 * 6 = 0 ∧ 6 ∈ {0, 3, 6, 9}

The tritone 6 is the element of order 2 of the ℤ/4 axis.