Documentation

TauCeti.LinearAlgebra.IntegralLattice.ConstructionA.Discriminant

The discriminant of a Construction A lattice #

This file computes the index and discriminant of the rational Construction A lattice attached to an additive code over ZMod m. Reduction modulo m identifies the quotient of the carrier of a code C by the zero-code carrier with C itself. Thus adjoining the codewords enlarges the zero-code lattice by index #C, while the zero-code lattice has diagonal Gram matrix m I.

Consequently, whenever C is self-orthogonal so that Construction A is integral,

disc(P_m(C)) * (#C)^2 = m^(#ι).

The multiplicative form records the divisibility needed for the quotient formula and remains valid without introducing truncated natural-number division.

References #

source
@[simp]
theorem TauCeti.ConstructionA.relIndex_lattice (m : ℕ) {ι : Type u_1} (C D : AddSubgroup (ι → ZMod m)) :
(lattice m C).toAddSubgroup.relIndex (lattice m D).toAddSubgroup = C.relIndex D

Construction A preserves relative indices: the relative index of the carrier of C in the carrier of D is the relative index of C in D.

source
noncomputable def TauCeti.ConstructionA.scaledStandardIsometry (m : ℕ) {ι : Type u_1} [Fintype ι] [NeZero m] :
(↑m • IntegralLattice.unitLattice ι).Isometry (integralLattice m ⊥ ⋯)

Multiplying every coordinate by m is an isometry from the standard coordinate lattice ℤ^ι, with its dot product scaled by m, onto the Construction A lattice of the zero code. It exhibits the zero-code lattice as m ℤ^ι carrying the normalized form.

Instances For
    source
    @[simp]
    theorem TauCeti.ConstructionA.scaledStandardIsometry_apply (m : ℕ) {ι : Type u_1} [Fintype ι] [NeZero m] (x : ι → ℚ) :
    (scaledStandardIsometry m) x = ↑m • x

    The scaled-standard isometry acts by multiplying every coordinate by m.

    source
    theorem TauCeti.ConstructionA.integralLattice_discriminant_bot (m : ℕ) {ι : Type u_1} [Fintype ι] [NeZero m] :
    (integralLattice m ⊥ ⋯).discriminant = m ^ Fintype.card ι

    The zero-code Construction A lattice has diagonal Gram matrix m I, hence discriminant m ^ #ι.

    source
    theorem TauCeti.ConstructionA.integralLattice_discriminant_mul_natCard_sq (m : ℕ) {ι : Type u_1} [Fintype ι] [NeZero m] (C : AddSubgroup (ι → ZMod m)) (hC : (AddSubgroup.toZModSubmodule m) C ≤ ((AddSubgroup.toZModSubmodule m) C).euclideanDual) :
    (integralLattice m C hC).discriminant * Nat.card ↥C ^ 2 = m ^ Fintype.card ι

    The discriminant formula for Construction A, with its divisibility visible: the discriminant times the square of the number of codewords is m ^ #ι.

    source
    theorem TauCeti.ConstructionA.natCard_sq_dvd_modulus_pow_card (m : ℕ) {ι : Type u_1} [Fintype ι] [NeZero m] (C : AddSubgroup (ι → ZMod m)) (hC : (AddSubgroup.toZModSubmodule m) C ≤ ((AddSubgroup.toZModSubmodule m) C).euclideanDual) :
    Nat.card ↥C ^ 2 ∣ m ^ Fintype.card ι

    The square of the number of codewords divides m ^ #ι, as required for the Construction A discriminant quotient.

    source
    @[simp]
    theorem TauCeti.ConstructionA.integralLattice_discriminant (m : ℕ) {ι : Type u_1} [Fintype ι] [NeZero m] (C : AddSubgroup (ι → ZMod m)) (hC : (AddSubgroup.toZModSubmodule m) C ≤ ((AddSubgroup.toZModSubmodule m) C).euclideanDual) :
    (integralLattice m C hC).discriminant = m ^ Fintype.card ι / Nat.card ↥C ^ 2

    The discriminant of an integral Construction A lattice is the exact natural-number quotient m ^ #ι / (#C)^2.

    source
    @[simp]
    theorem TauCeti.ConstructionA.integralLattice_discriminant_of_prime {ι : Type u_1} [Fintype ι] {p : ℕ} [hp : Fact (Nat.Prime p)] (C : Submodule (ZMod p) (ι → ZMod p)) (hC : C ≤ C.euclideanDual) :
    (integralLattice p C.toAddSubgroup hC).discriminant = p ^ (Fintype.card ι - 2 * Module.finrank (ZMod p) ↥C)

    For a self-orthogonal linear code of dimension k over the prime field ZMod p, the Construction A discriminant is p ^ (n - 2k).