Orthogonal sums of finite families of finite quadratic modules

For a finite family A : ι → FiniteQuadraticModule, the group Π i, A i carries the quadratic map

q(x) = ∑ i, q_i(x_i),

Mathlib's QuadraticMap.pi, whose polar pairing is the sum of the coordinate pairings. This is the orthogonal sum of the family; the binary case is TauCeti.FiniteQuadraticModule.prod. Classification results for finite quadratic modules are stated with it, as an isometry from an orthogonal sum of standard generators.

Since the quadratic map of pi A is literally QuadraticMap.pi, isometries between orthogonal sums come from the general theory of quadratic maps: an orthogonal sum of coordinatewise isometries is Mathlib's QuadraticMap.IsometryEquiv.pi, and over Fin (n + 1) splitting off the first summand is QuadraticMap.IsometryEquiv.consPi.

For a constant family, the quadratic map and pairing of pi agree with those of TauCeti.FiniteQuadraticModule.coordinatePower, which carries the additional coordinatewise API used for codes.

Main declarations

• TauCeti.FiniteQuadraticModule.pi: the orthogonal sum of a finite family.
• TauCeti.FiniteQuadraticModule.pi_quadratic and TauCeti.FiniteQuadraticModule.pi_pairing: its quadratic map and pairing are the sums of the coordinate ones.
• TauCeti.FiniteQuadraticModule.isNondegenerate_pi_iff: the orthogonal sum is nondegenerate exactly when every summand is.

References

• V. V. Nikulin, Integral symmetric bilinear forms and some of their applications, §1.1.

@[reducible, inline]

abbrev TauCeti.FiniteQuadraticModule.pi {ι : Type v} [Fintype ι] (A : ι → FiniteQuadraticModule) : FiniteQuadraticModule

The orthogonal sum of a finite family of finite quadratic modules: the group Π i, A i with the quadratic map x ↦ ∑ i, q_i(x_i), Mathlib's QuadraticMap.pi, and its polar pairing.

Reducible, exactly as TauCeti.FiniteQuadraticModule.prod is, so that the carrier of an orthogonal sum reduces to the product of the carriers.

theorem TauCeti.FiniteQuadraticModule.pi_quadratic {ι : Type v} [Fintype ι] (A : ι → FiniteQuadraticModule) (x : (pi A).carrier) : (pi A).quadratic x = ∑ i : ι, (A i).quadratic (x i)

The quadratic map of an orthogonal sum is the sum of the coordinate quadratic maps.

theorem TauCeti.FiniteQuadraticModule.pi_pairing {ι : Type v} [Fintype ι] (A : ι → FiniteQuadraticModule) (x y : (pi A).carrier) : ((pi A).pairing x) y = ∑ i : ι, ((A i).pairing (x i)) (y i)

The pairing of an orthogonal sum is the sum of the coordinate pairings.

@[simp]

theorem TauCeti.FiniteQuadraticModule.isNondegenerate_pi_iff {ι : Type v} [Fintype ι] (A : ι → FiniteQuadraticModule) : (pi A).IsNondegenerate ↔ ∀ (i : ι), (A i).IsNondegenerate

An orthogonal sum is nondegenerate exactly when every summand is.

theorem TauCeti.FiniteQuadraticModule.forall_quadratic_add_self_eq_zero_pi_iff {ι : Type v} [Fintype ι] (A : ι → FiniteQuadraticModule) : (∀ (x : (pi A).carrier), (pi A).quadratic x + (pi A).quadratic x = 0) ↔ ∀ (i : ι) (y : (A i).carrier), (A i).quadratic y + (A i).quadratic y = 0

An orthogonal sum has quadratic form with values in ½ℤ/ℤ exactly when every summand does.