Self-dual and normal bases, and the downsize identities

The vocabulary of blueprint lem:self-dual-basis and of the paper's \downsize maps (preliminaries.tex, sec:ff-representations): a basis of K / F is self-dual when its trace-form Gram matrix is the identity, and normal when its vectors are the Frobenius orbit of a single element.

The two identities proved here are items 1 and 2 of the paper's lem:downsize_field, and they are the reason the pipeline insists on self-duality:

• coord_eq_trace — the coordinates of x are its trace pairings, κ(x)ᵢ = tr(x eᵢ), so \downsize is computed by the trace form and needs no matrix inversion;
• trace_mul_eq_dot — tr(xy) = κ(x) · κ(y), so the trace form becomes the standard inner product on coordinates.

Both need only self-duality, not normality and not odd degree (ledger node 1.1.6.1.11). Normality is what the introspection and Pauli-basis interfaces need on top, and is the harder half of lem:self-dual-basis.

def MIPRE.LowDegree.IsSelfDualBasis {F : Type u_1} {K : Type u_2} [Field F] [Field K] [Algebra F K] {ι : Type u_3} [DecidableEq ι] (b : Module.Basis ι F K) : Prop

b is a self-dual basis for the trace form of K / F: tr(eᵢ eⱼ) = δᵢⱼ, that is, the Gram matrix of Algebra.traceForm in b is the identity.

Equations

• MIPRE.LowDegree.IsSelfDualBasis b = ∀ (i j : ι), (Algebra.trace F K) (b i * b j) = if i = j then 1 else 0

def MIPRE.LowDegree.IsNormalBasis {F : Type u_1} {K : Type u_2} [Field F] [Field K] [Algebra F K] [Fintype F] {k : ℕ} (b : Module.Basis (Fin k) F K) : Prop

b is a normal basis of K / F: its vectors are the Frobenius orbit α, α^q, α^{q²}, … of a single α, where q = #F.

Equations

• MIPRE.LowDegree.IsNormalBasis b = ∃ (α : K), ∀ (i : Fin k), b i = α ^ Fintype.card F ^ ↑i

theorem MIPRE.LowDegree.coord_eq_trace {F : Type u_1} {K : Type u_2} [Field F] [Field K] [Algebra F K] {ι : Type u_3} [Fintype ι] [DecidableEq ι] {b : Module.Basis ι F K} (hb : IsSelfDualBasis b) (x : K) (i : ι) : (b.repr x) i = (Algebra.trace F K) (x * b i)

The coordinates of a self-dual basis are trace pairings (lem:downsize_field, item 1): κ(x)ᵢ = tr(x eᵢ).

theorem MIPRE.LowDegree.trace_mul_eq_dot {F : Type u_1} {K : Type u_2} [Field F] [Field K] [Algebra F K] {ι : Type u_3} [Fintype ι] [DecidableEq ι] {b : Module.Basis ι F K} (hb : IsSelfDualBasis b) (x y : K) : (Algebra.trace F K) (x * y) = ∑ i : ι, (b.repr x) i * (b.repr y) i

The trace form is the coordinate inner product (lem:downsize_field, item 2): tr(xy) = κ(x) · κ(y).