Other multipliers: the rank of a difference matrix

Let n ≥ 3, ℓ ∈ (ZMod n)ˣ, F a field with 2 ≠ 0, s : ZMod n → F odd, and rows indexed by representatives ρ q of (ZMod n)ˣ / ±1. If the matrix M = [s(u⁻¹ c)] (rows u = ρ q, columns c ∈ ZMod n) has rank |Q| (hypothesis hM), then A = [½ (s(ℓ u⁻¹ c) − s(u⁻¹ c))] has rank d − δ_ℓ, with d = |Q|, 2d = φ(n), δ_ℓ = 0 if −1 ∈ ⟨ℓ⟩ and δ_ℓ = d / ord(ℓ) otherwise. The hypothesis hM (over ℚ a theorem of Kurihara; over 𝔽_p a consequence of Sinnott's index formula when p ∤ n h⁻) is not formalized.

Main results

• Multiplicadores.prop_multiplicadores_of_mem: the case −1 ∈ ⟨ℓ⟩.
• Multiplicadores.prop_multiplicadores_of_not_mem: the case −1 ∉ ⟨ℓ⟩.
• Multiplicadores.finrank_oddSub, Multiplicadores.rank_eq: the dimension count behind them.

References

• C. Marín, Conductors of orders generated by character values of Sp(2m), preprint (2026); programs and outputs: Zenodo, doi:10.5281/zenodo.23090540.
• C. Marín, Where the character values of Sp(2m) at a torsion element fail to generate the ring of integers, Zenodo (2026), doi:10.5281/zenodo.22813216 (a longer preprint of the same work).

Odd functions for a fixed-point-free involution

def Multiplicadores.oddSub {F : Type u_1} [Field F] {Y : Type u_2} (σ : Y → Y) : Submodule F (Y → F)

Functions v with v (σ y) = - v y.

Equations

• Multiplicadores.oddSub σ = { carrier := {v : Y → F | ∀ (y : Y), v (σ y) = -v y}, add_mem' := ⋯, zero_mem' := ⋯, smul_mem' := ⋯ }

def Multiplicadores.evenSub {F : Type u_1} [Field F] {Y : Type u_2} (σ : Y → Y) : Submodule F (Y → F)

Functions v with v (σ y) = v y.

Equations

• Multiplicadores.evenSub σ = { carrier := {v : Y → F | ∀ (y : Y), v (σ y) = v y}, add_mem' := ⋯, zero_mem' := ⋯, smul_mem' := ⋯ }

theorem Multiplicadores.finrank_oddSub {F : Type u_1} [Field F] {Y : Type u_2} [Fintype Y] (hF : 2 ≠ 0) (σ : Y → Y) (hinv : ∀ (y : Y), σ (σ y) = y) (hfree : ∀ (y : Y), σ y ≠ y) : Module.finrank F ↥(oddSub σ) * 2 = Fintype.card Y

For an involution σ without fixed points on a finite set Y and 2 ≠ 0 in F, the odd functions have dimension |Y| / 2.

Rank-nullity along a subspace

theorem Multiplicadores.finrank_map_of_injOn {F : Type u_1} [Field F] {V : Type u_2} {W : Type u_3} [AddCommGroup V] [Module F V] [FiniteDimensional F V] [AddCommGroup W] [Module F W] (f : V →ₗ[F] W) (S : Submodule F V) (h : ∀ v ∈ S, f v = 0 → v = 0) : Module.finrank F ↥(Submodule.map f S) = Module.finrank F ↥S

If f is injective on S, then f(S) has the dimension of S.

theorem Multiplicadores.finrank_map_add_fix {F : Type u_1} [Field F] {V : Type u_2} {W : Type u_3} [AddCommGroup V] [Module F V] [FiniteDimensional F V] [AddCommGroup W] [Module F W] (f : V →ₗ[F] W) (S : Submodule F V) : Module.finrank F ↥(Submodule.map f S) + Module.finrank F ↥(S ⊓ f.ker) = Module.finrank F ↥S

Rank-nullity for f restricted to S.

The setting of prop:multiplicadores

theorem Multiplicadores.neg_ne_self {n : ℕ} (hn : 3 ≤ n) (u : (ZMod n)ˣ) : -u ≠ u

-u ≠ u in (ZMod n)ˣ for n ≥ 3.

def Multiplicadores.Mfull {F : Type u_1} {n : ℕ} (s : ZMod n → F) : Matrix (ZMod n)ˣ (ZMod n) F

The full matrix [s(u⁻¹ c)], rows over all units.

Equations

• Multiplicadores.Mfull s u c = s (↑u⁻¹ * c)

def Multiplicadores.Amat {F : Type u_1} [Field F] {n : ℕ} (s : ZMod n → F) (ℓ : (ZMod n)ˣ) {Q : Type u_2} (ρ : Q → (ZMod n)ˣ) : Matrix Q (ZMod n) F

The matrix of the paper, [½ (s(ℓ u⁻¹ c) - s(u⁻¹ c))], rows u = ρ q.

Equations

• Multiplicadores.Amat s ℓ ρ q c = 1 / 2 * (s (↑ℓ * ↑(ρ q)⁻¹ * c) - s (↑(ρ q)⁻¹ * c))

def Multiplicadores.Mmat {F : Type u_1} {n : ℕ} (s : ZMod n → F) {Q : Type u_2} (ρ : Q → (ZMod n)ˣ) : Matrix Q (ZMod n) F

The matrix M_n = [s(u⁻¹ c)], rows u = ρ q.

Equations

• Multiplicadores.Mmat s ρ q c = s (↑(ρ q)⁻¹ * c)

def Multiplicadores.fixSub {F : Type u_1} [Field F] {n : ℕ} (ℓ : (ZMod n)ˣ) : Submodule F ((ZMod n)ˣ → F)

The fixed space of P_ℓ on odd functions: v odd with v(u ℓ⁻¹) = v(u).

Equations

• Multiplicadores.fixSub ℓ = (Multiplicadores.oddSub fun (u : (ZMod n)ˣ) => -u) ⊓ ((LinearMap.funLeft F F fun (u : (ZMod n)ˣ) => u * ℓ⁻¹) - LinearMap.id).ker

theorem Multiplicadores.mem_fixSub {F : Type u_1} [Field F] {n : ℕ} {ℓ : (ZMod n)ˣ} {v : (ZMod n)ˣ → F} : v ∈ fixSub ℓ ↔ (∀ (u : (ZMod n)ˣ), v (-u) = -v u) ∧ ∀ (u : (ZMod n)ˣ), v (u * ℓ⁻¹) = v u

theorem Multiplicadores.inv_zpow {F : Type u_1} {n : ℕ} {ℓ : (ZMod n)ˣ} {v : (ZMod n)ˣ → F} (h : ∀ (u : (ZMod n)ˣ), v (u * ℓ⁻¹) = v u) (j : ℤ) (u : (ZMod n)ˣ) : v (u * ℓ ^ j) = v u

ℓ⁻¹-invariance gives invariance under all of ⟨ℓ⟩.

theorem Multiplicadores.fixSub_eq_bot {F : Type u_1} [Field F] {n : ℕ} (hF : 2 ≠ 0) {ℓ : (ZMod n)ˣ} (h : -1 ∈ Subgroup.zpowers ℓ) : fixSub ℓ = ⊥

δ_ℓ = 0: if -1 ∈ ⟨ℓ⟩, the fixed space is zero (characteristic ≠ 2).

theorem Multiplicadores.finrank_fixSub {F : Type u_1} [Field F] {n : ℕ} [NeZero n] (hF : 2 ≠ 0) {ℓ : (ZMod n)ˣ} (h : -1 ∉ Subgroup.zpowers ℓ) : Module.finrank F ↥(fixSub ℓ) * 2 * orderOf ℓ = Nat.card (ZMod n)ˣ

δ_ℓ = d / ord(ℓ): if -1 ∉ ⟨ℓ⟩, 2 · dim Fix · ord(ℓ) = φ(n).

prop:multiplicadores

theorem Multiplicadores.rank_eq {F : Type u_1} [Field F] {n : ℕ} [NeZero n] {Q : Type u_2} [Fintype Q] (hF : 2 ≠ 0) (hn : 3 ≤ n) (s : ZMod n → F) (hs : ∀ (x : ZMod n), s (-x) = -s x) (ℓ : (ZMod n)ˣ) (ρ : Q → (ZMod n)ˣ) (hρ : ∀ (u : (ZMod n)ˣ), ∃ (q : Q), ρ q = u ∨ ρ q = -u) (hM : (Mmat s ρ).rank = Fintype.card Q) : Fintype.card Q * 2 = n.totient ∧ (Amat s ℓ ρ).rank + Module.finrank F ↥(fixSub ℓ) = Fintype.card Q

prop:multiplicadores (6.1), core. n ≥ 3, F a field with 2 ≠ 0, s odd, ρ : Q → (ZMod n)ˣ hitting every class of (ZMod n)ˣ/±1, and hM: M_n = [s(u⁻¹ c)] has rank |Q| over F (Kurihara over ℚ; prop:sinnott over 𝔽_p, p ∤ n h⁻). Then 2|Q| = φ(n), and A = [½(s(ℓu⁻¹c) - s(u⁻¹c))] has rank |Q| - δ, where δ is the dimension of the fixed space of P_ℓ on odd functions.

theorem Multiplicadores.prop_multiplicadores_of_mem {F : Type u_1} [Field F] {n : ℕ} [NeZero n] {Q : Type u_2} [Fintype Q] (hF : 2 ≠ 0) (hn : 3 ≤ n) (s : ZMod n → F) (hs : ∀ (x : ZMod n), s (-x) = -s x) (ℓ : (ZMod n)ˣ) (ρ : Q → (ZMod n)ˣ) (hρ : ∀ (u : (ZMod n)ˣ), ∃ (q : Q), ρ q = u ∨ ρ q = -u) (hM : (Mmat s ρ).rank = Fintype.card Q) (h : -1 ∈ Subgroup.zpowers ℓ) : Fintype.card Q * 2 = n.totient ∧ (Amat s ℓ ρ).rank = Fintype.card Q

prop:multiplicadores, case -1 ∈ ⟨ℓ⟩: δ_ℓ = 0, the rank is d = |Q| = φ(n)/2.

theorem Multiplicadores.prop_multiplicadores_of_not_mem {F : Type u_1} [Field F] {n : ℕ} [NeZero n] {Q : Type u_2} [Fintype Q] (hF : 2 ≠ 0) (hn : 3 ≤ n) (s : ZMod n → F) (hs : ∀ (x : ZMod n), s (-x) = -s x) (ℓ : (ZMod n)ˣ) (ρ : Q → (ZMod n)ˣ) (hρ : ∀ (u : (ZMod n)ˣ), ∃ (q : Q), ρ q = u ∨ ρ q = -u) (hM : (Mmat s ρ).rank = Fintype.card Q) (h : -1 ∉ Subgroup.zpowers ℓ) : Fintype.card Q * 2 = n.totient ∧ orderOf ℓ ∣ Fintype.card Q ∧ (Amat s ℓ ρ).rank = Fintype.card Q - Fintype.card Q / orderOf ℓ

prop:multiplicadores, case -1 ∉ ⟨ℓ⟩: δ_ℓ = d / ord_n(ℓ) (and ord_n(ℓ) ∣ d), the rank is d - d / ord_n(ℓ), d = |Q| = φ(n)/2.