A_SU(n) = A_Sp(q−n−1), and the free quadratic extension R ⊕ θR

For q odd and n < q even, the coefficient rings of the segment polynomials satisfy A_SU(n) = A_Sp(q−n−1). The second part treats B = R ⊕ θR with θ² = c (QuadraticAlgebra R c 0): its trace, its trace dual and its Kähler differentials.

Main results

• NotaPuente.A_F_eq_A_Gsp_of_odd: A_SU(n) = A_Sp(q−n−1) for q odd, n < q even.
• NotaPuente.trace_quadraticAlgebra, NotaPuente.trace_B: Tr(x + yω) = 2x + b y.
• NotaPuente.dual_of_mem, NotaPuente.dual_eq: with 2 a unit and c a non-zero-divisor, x ↦ Tr(x ·) identifies (2θ)⁻¹B with Hom_R(B, R), stated without localization (2c · f z = Tr(θ y z) for exactly one y ∈ B).
• NotaPuente.kaehlerEquiv: Ω_{B/R} ≃ B ⧸ (2θ), for every c.

References

• C. Marín, Non-real orders of character values of GL(n), preprint (2026).
• C. Marín, The ring of character values depends only on the segment: SU(n), Sp(2m) and GL(n) at a torsion element, Zenodo (2026), doi:10.5281/zenodo.22847476.

Corollary 2.3

theorem NotaPuente.A_F_eq_A_Gsp_of_odd {K : Type u_1} [Field K] {t : K} {q : ℕ} (hq : 0 < q) (ht : IsPrimitiveRoot t (2 * q)) (hqo : Odd q) {n : ℕ} (hne : Even n) (hn : n < q) : A (F t n) = A (Gsp t ((q - n - 1) / 2))

Corollary 2.3: for q odd and n < q even, A_SU(n) = A_Sp(q-n-1). q - n is odd, q - n = 2m + 1 with m = (q - n - 1)/2; apply Prop. 2.2(b), then (a).

Lemma 5.7: the free quadratic extension B = R ⊕ θR, θ² = c

B := QuadraticAlgebra R c 0 (Mathlib: ω * ω = c • 1 + 0 • ω), θ := ω.

Formulation without localization. In B[1/c] (2 a unit) one has 1/(2θ) = θ/(2c), so an element of (2θ)⁻¹B is x = y/(2θ) = θy/(2c) with y ∈ B unique, and Tr(x z) = Tr(θ y z)/(2c). Hence "x ↦ Tr(x·) identifies (2θ)⁻¹B with Hom_R(B,R)" is equivalent to:

• dual_of_mem: for each y ∈ B, Tr(θ y z) is divisible by 2c, uniformly and linearly in z (so z ↦ Tr(xz) is an R-valued functional: (2θ)⁻¹B ⊆ dual);
• dual_eq: each f : B →ₗ[R] R satisfies 2c · f z = Tr(θ y z) for exactly one y ∈ B (dual ⊆ (2θ)⁻¹B, and the map is injective). Since 2c is a non-zero-divisor, 2c·f z = Tr(θyz) is equivalent to f z = Tr(xz) in R[1/c]. The Kähler part (c) holds for every c (no hypothesis on 2 or c).

theorem NotaPuente.trace_quadraticAlgebra {R : Type u_1} [CommRing R] (a b : R) (z : QuadraticAlgebra R a b) : (Algebra.trace R (QuadraticAlgebra R a b)) z = 2 * z.re + b * z.im

Trace of a general quadratic algebra R[ω]/(ω² - bω - a): Tr(x + yω) = 2x + b y.

theorem NotaPuente.trace_B {R : Type u_1} [CommRing R] (c : R) (z : QuadraticAlgebra R c 0) : (Algebra.trace R (QuadraticAlgebra R c 0)) z = 2 * z.re

(a) Tr(x + yθ) = 2x.

theorem NotaPuente.trace_B_basis {R : Type u_1} [CommRing R] (c : R) : (Algebra.trace R (QuadraticAlgebra R c 0)) 1 = 2 ∧ (Algebra.trace R (QuadraticAlgebra R c 0)) QuadraticAlgebra.omega = 0 ∧ (Algebra.trace R (QuadraticAlgebra R c 0)) (QuadraticAlgebra.omega * QuadraticAlgebra.omega) = 2 * c

(a) The trace form on the basis 1, θ: Tr 1 = 2, Tr θ = 0, Tr θ² = 2c.

theorem NotaPuente.trace_omega_mul {R : Type u_1} [CommRing R] (c : R) (y z : QuadraticAlgebra R c 0) : (Algebra.trace R (QuadraticAlgebra R c 0)) (QuadraticAlgebra.omega * y * z) = 2 * c * (y.im * z.re + y.re * z.im)

The pairing Tr(θ y z) is divisible by 2c: Tr(θ y z) = 2c (y.im z.re + y.re z.im).

theorem NotaPuente.dual_of_mem {R : Type u_1} [CommRing R] (c : R) (y : QuadraticAlgebra R c 0) : ∃ (f : QuadraticAlgebra R c 0 →ₗ[R] R), ∀ (z : QuadraticAlgebra R c 0), 2 * c * f z = (Algebra.trace R (QuadraticAlgebra R c 0)) (QuadraticAlgebra.omega * y * z)

(b), inclusion (2θ)⁻¹B ⊆ dual: for every y ∈ B the functional z ↦ Tr(y z / (2θ)) is R-valued, i.e. there is f : B →ₗ[R] R with 2c · f z = Tr(θ y z).

theorem NotaPuente.dual_eq {R : Type u_1} [CommRing R] (c : R) (h2 : IsUnit 2) (hc : c ∈ nonZeroDivisors R) (f : QuadraticAlgebra R c 0 →ₗ[R] R) : ∃! y : QuadraticAlgebra R c 0, ∀ (z : QuadraticAlgebra R c 0), 2 * c * f z = (Algebra.trace R (QuadraticAlgebra R c 0)) (QuadraticAlgebra.omega * y * z)

(b), every functional comes from a unique y ∈ B, i.e. dual ⊆ (2θ)⁻¹B and the identification is bijective (needs 2 a unit and c a non-zero-divisor only for uniqueness).

(c) Kähler differentials: Ω_{B/R} ≅ B ⧸ (2θ).

@[reducible, inline]

abbrev NotaPuente.I2θ {R : Type u_1} [CommRing R] (c : R) : Ideal (QuadraticAlgebra R c 0)

The ideal 2θ·B.

Equations

• NotaPuente.I2θ c = Ideal.span {2 * QuadraticAlgebra.omega}

theorem NotaPuente.omega_mul_omega_B {R : Type u_1} [CommRing R] (c : R) : QuadraticAlgebra.omega * QuadraticAlgebra.omega = (algebraMap R (QuadraticAlgebra R c 0)) c

θ² = c in B.

def NotaPuente.dQ {R : Type u_1} [CommRing R] (c : R) : Derivation R (QuadraticAlgebra R c 0) (QuadraticAlgebra R c 0 ⧸ I2θ c)

The universal derivation, explicitly: d(x + yθ) = y mod 2θ (i.e. y · dθ).

Equations

• One or more equations did not get rendered due to their size.

theorem NotaPuente.dQ_apply {R : Type u_1} [CommRing R] (c : R) (z : QuadraticAlgebra R c 0) : (dQ c) z = (Ideal.Quotient.mk (I2θ c)) ((algebraMap R (QuadraticAlgebra R c 0)) z.im)

theorem NotaPuente.two_omega_smul_D {R : Type u_1} [CommRing R] (c : R) : (2 * QuadraticAlgebra.omega) • (KaehlerDifferential.D R (QuadraticAlgebra R c 0)) QuadraticAlgebra.omega = 0

2θ · dθ = d(θ²) = d c = 0 in Ω_{B/R}.

noncomputable def NotaPuente.kPhi {R : Type u_1} [CommRing R] (c : R) : Ω[QuadraticAlgebra R c 0⁄R] →ₗ[QuadraticAlgebra R c 0] QuadraticAlgebra R c 0 ⧸ I2θ c

Ω_{B/R} → B ⧸ 2θB, induced by the derivation dQ.

Equations

• NotaPuente.kPhi c = (NotaPuente.dQ c).liftKaehlerDifferential

noncomputable def NotaPuente.kPsi {R : Type u_1} [CommRing R] (c : R) : QuadraticAlgebra R c 0 ⧸ I2θ c →ₗ[QuadraticAlgebra R c 0] Ω[QuadraticAlgebra R c 0⁄R]

B ⧸ 2θB → Ω_{B/R}, b ↦ b · dθ (well defined by two_omega_smul_D).

Equations

• One or more equations did not get rendered due to their size.

theorem NotaPuente.kPsi_mk {R : Type u_1} [CommRing R] (c : R) (b : QuadraticAlgebra R c 0) : (kPsi c) ((Ideal.Quotient.mk (I2θ c)) b) = b • (KaehlerDifferential.D R (QuadraticAlgebra R c 0)) QuadraticAlgebra.omega

noncomputable def NotaPuente.kaehlerEquiv {R : Type u_1} [CommRing R] (c : R) : Ω[QuadraticAlgebra R c 0⁄R] ≃ₗ[QuadraticAlgebra R c 0] QuadraticAlgebra R c 0 ⧸ I2θ c

(c) Ω_{B/R} ≅ B ⧸ 2θB as B-modules, dθ ↦ 1.

Equations

• NotaPuente.kaehlerEquiv c = LinearEquiv.ofLinearMap (NotaPuente.kPhi c) (NotaPuente.kPsi c) ⋯ ⋯

theorem NotaPuente.kaehlerEquiv_D_omega {R : Type u_1} [CommRing R] (c : R) : (kaehlerEquiv c) ((KaehlerDifferential.D R (QuadraticAlgebra R c 0)) QuadraticAlgebra.omega) = 1