Coordinate powers of finite bilinear and quadratic modules

A finite bilinear module A determines a bilinear module on words ι → A by summing its pairing coordinatewise. Thus the orthogonal complement of an additive subgroup of words is its standard dual additive code. Nondegeneracy of the alphabet pairing passes to every finite coordinate power, so the existing orthogonal-complement cardinality and double-complement theorems apply to these codes.

For a finite quadratic module the quadratic value of a word is likewise the sum of its coordinate values. Its polar bilinear module is definitionally the corresponding coordinate power. These constructions are the finite-form interface used when code coordinates are identified with discriminant-module coordinates.

Main declarations

• TauCeti.FiniteBilinearModule.coordinatePower: the summed pairing on ι → A.
• TauCeti.FiniteBilinearModule.IsNondegenerate.coordinatePower: nondegeneracy of a coordinate power.
• TauCeti.FiniteBilinearModule.mem_orthogonalComplement_coordinatePower_iff: membership in the dual additive code.
• TauCeti.FiniteBilinearModule.Isometry.coordinatePower: the coordinatewise isometry induced by an alphabet isometry.
• TauCeti.FiniteQuadraticModule.coordinatePower: the summed quadratic map on ι → A.
• TauCeti.FiniteQuadraticModule.isIsotropic_coordinatePower_iff: the coordinate-sum criterion for quadratic isotropy.
• TauCeti.FiniteQuadraticModule.Isometry.coordinatePowerSigned: the isometry of coordinate powers given by signs and a relabelling of coordinates.

References

• W. C. Huffman and V. Pless, Fundamentals of Error-Correcting Codes, §§1.2–1.4.
• J. H. Conway and N. J. A. Sloane, Sphere Packings, Lattices and Groups, Chapter 4, §3.

@[reducible, inline]

abbrev TauCeti.FiniteBilinearModule.coordinatePower (A : FiniteBilinearModule) (ι : Type v) [Fintype ι] : FiniteBilinearModule

The finite bilinear module on words ι → A, with pairing obtained by summing the coordinate pairings.

This is reducible, as FiniteBilinearModule.prod is, so that additive codes in the raw function type are directly subgroups of the coordinate power.

theorem TauCeti.FiniteBilinearModule.coordinatePower_pairing (A : FiniteBilinearModule) (ι : Type v) [Fintype ι] (x y : ι → A.carrier) : ((A.coordinatePower ι).pairing x) y = ∑ i : ι, (A.pairing (x i)) (y i)

The pairing on a coordinate power is the sum of the coordinate pairings.

theorem TauCeti.FiniteBilinearModule.coordinatePower_pairing_extend_zero_left (A : FiniteBilinearModule) {ι : Type v} {κ : Type w} [Fintype ι] [Fintype κ] {f : ι → κ} (hf : Function.Injective f) (x : ι → A.carrier) (y : κ → A.carrier) : ((A.coordinatePower κ).pairing (Function.extend f x 0)) y = ((A.coordinatePower ι).pairing x) (y ∘ f)

Extension by zero along an injective coordinate map is adjoint to restriction for the coordinate pairing.

theorem TauCeti.FiniteBilinearModule.coordinatePower_pairing_single_right (A : FiniteBilinearModule) (ι : Type v) [Fintype ι] [DecidableEq ι] (x : ι → A.carrier) (i : ι) (a : A.carrier) : ((A.coordinatePower ι).pairing x) (Pi.single i a) = (A.pairing (x i)) a

Pairing a word with a word supported at one coordinate extracts that coordinate pairing.

theorem TauCeti.FiniteBilinearModule.coordinatePower_pairing_single_left (A : FiniteBilinearModule) (ι : Type v) [Fintype ι] [DecidableEq ι] (i : ι) (a : A.carrier) (y : ι → A.carrier) : ((A.coordinatePower ι).pairing (Pi.single i a)) y = (A.pairing a) (y i)

Pairing a word supported at one coordinate with an arbitrary word extracts that coordinate pairing.

theorem TauCeti.FiniteBilinearModule.IsNondegenerate.coordinatePower {A : FiniteBilinearModule} (hA : A.IsNondegenerate) (ι : Type v) [Fintype ι] : (A.coordinatePower ι).IsNondegenerate

A coordinate power of a nondegenerate finite bilinear module is nondegenerate.

@[simp]

theorem TauCeti.FiniteBilinearModule.mem_orthogonalComplement_coordinatePower_iff (A : FiniteBilinearModule) (ι : Type v) [Fintype ι] (C : AddSubgroup (ι → A.carrier)) (x : ι → A.carrier) : x ∈ (A.coordinatePower ι).orthogonalComplement C ↔ ∀ y ∈ C, ∑ i : ι, (A.pairing (x i)) (y i) = 0

Membership in the orthogonal complement of an additive code is vanishing of every summed coordinate pairing.

def TauCeti.FiniteBilinearModule.Isometry.coordinatePower {A : FiniteBilinearModule} {B : FiniteBilinearModule} (f : A.Isometry B) (ι : Type v) [Fintype ι] : (A.coordinatePower ι).Isometry (B.coordinatePower ι)

An isometry of finite bilinear alphabets induces an isometry on every finite coordinate power by acting coordinatewise.

@[simp]

theorem TauCeti.FiniteBilinearModule.Isometry.coordinatePower_apply {A : FiniteBilinearModule} {B : FiniteBilinearModule} (f : A.Isometry B) (ι : Type v) [Fintype ι] (x : ι → A.carrier) (i : ι) : (f.coordinatePower ι) x i = f (x i)

A coordinatewise bilinear-module isometry acts at each coordinate by the alphabet isometry.

@[reducible, inline]

abbrev TauCeti.FiniteQuadraticModule.coordinatePower (A : FiniteQuadraticModule) (ι : Type v) [Fintype ι] : FiniteQuadraticModule

The finite quadratic module on words ι → A, with quadratic value obtained by summing the coordinate values.

This is reducible so that its carrier is literally the raw function type and its polar module is definitionally the bilinear coordinate power.

theorem TauCeti.FiniteQuadraticModule.coordinatePower_quadratic (A : FiniteQuadraticModule) (ι : Type v) [Fintype ι] (x : ι → A.carrier) : (A.coordinatePower ι).quadratic x = ∑ i : ι, A.quadratic (x i)

The quadratic value on a coordinate power is the sum of the coordinate quadratic values.

theorem TauCeti.FiniteQuadraticModule.coordinatePower_pairing (A : FiniteQuadraticModule) (ι : Type v) [Fintype ι] (x y : ι → A.carrier) : ((A.coordinatePower ι).pairing x) y = ∑ i : ι, (A.pairing (x i)) (y i)

The pairing on a quadratic coordinate power is the sum of the coordinate polar pairings.

@[simp]

theorem TauCeti.FiniteQuadraticModule.coordinatePower_toFiniteBilinearModule (A : FiniteQuadraticModule) (ι : Type v) [Fintype ι] : (A.coordinatePower ι).toFiniteBilinearModule = A.coordinatePower ι

Forgetting the quadratic map from a coordinate power gives the coordinate power of the polar finite bilinear module.

theorem TauCeti.FiniteQuadraticModule.IsNondegenerate.coordinatePower {A : FiniteQuadraticModule} (hA : A.IsNondegenerate) (ι : Type v) [Fintype ι] : (A.coordinatePower ι).IsNondegenerate

A coordinate power of a nondegenerate finite quadratic module is nondegenerate.

@[simp]

theorem TauCeti.FiniteQuadraticModule.isIsotropic_coordinatePower_iff (A : FiniteQuadraticModule) (ι : Type v) [Fintype ι] (C : AddSubgroup (ι → A.carrier)) : (A.coordinatePower ι).IsIsotropic C ↔ ∀ x ∈ C, ∑ i : ι, A.quadratic (x i) = 0

A subgroup of a quadratic coordinate power is isotropic exactly when the sum of the coordinate quadratic values vanishes on every one of its words.

def TauCeti.FiniteQuadraticModule.Isometry.coordinatePower {A : FiniteQuadraticModule} {B : FiniteQuadraticModule} (f : A.Isometry B) (ι : Type v) [Fintype ι] : (A.coordinatePower ι).Isometry (B.coordinatePower ι)

An isometry of finite quadratic alphabets induces an isometry on every finite coordinate power by acting coordinatewise.

@[simp]

theorem TauCeti.FiniteQuadraticModule.Isometry.coordinatePower_apply {A : FiniteQuadraticModule} {B : FiniteQuadraticModule} (f : A.Isometry B) (ι : Type v) [Fintype ι] (x : ι → A.carrier) (i : ι) : (f.coordinatePower ι) x i = f (x i)

A coordinatewise quadratic-module isometry acts at each coordinate by the alphabet isometry.

@[simp]

theorem TauCeti.FiniteQuadraticModule.Isometry.coordinatePower_toAddEquiv {A : FiniteQuadraticModule} {B : FiniteQuadraticModule} (f : A.Isometry B) (ι : Type v) [Fintype ι] : (f.coordinatePower ι).toAddEquiv = AddEquiv.piCongrRight fun (x : ι) => f.toAddEquiv

The additive equivalence underlying a coordinatewise quadratic isometry is the coordinatewise additive equivalence.

@[simp]

theorem TauCeti.FiniteQuadraticModule.Isometry.coordinatePower_toFiniteBilinearModule {A : FiniteQuadraticModule} {B : FiniteQuadraticModule} (f : A.Isometry B) (ι : Type v) [Fintype ι] : (f.coordinatePower ι).toFiniteBilinearModule = f.toFiniteBilinearModule.coordinatePower ι

Forgetting the quadratic data from a coordinatewise isometry gives the corresponding coordinatewise bilinear isometry.

def TauCeti.FiniteQuadraticModule.Isometry.coordinatePowerSigned (A : FiniteQuadraticModule) {ι : Type v} {κ : Type w} [Fintype ι] [Fintype κ] (u : ι → ℤˣ) (e : ι ≃ κ) : (A.coordinatePower ι).Isometry (A.coordinatePower κ)

Signed coordinate changes are isometries. For signs u : ι → ℤˣ and a relabelling e : ι ≃ κ of coordinates, multiplying the i-th coordinate of a word by u i and placing it in coordinate e i is an isometry of coordinate powers, because q(-x) = q(x).

@[simp]

theorem TauCeti.FiniteQuadraticModule.Isometry.coordinatePowerSigned_apply (A : FiniteQuadraticModule) {ι : Type v} {κ : Type w} [Fintype ι] [Fintype κ] (u : ι → ℤˣ) (e : ι ≃ κ) (x : ι → A.carrier) (j : κ) : (coordinatePowerSigned A u e) x j = u (e.symm j) • x (e.symm j)

A signed coordinate change multiplies the source coordinate of each target coordinate by its sign.