Linear and additive codes

This file fixes the carrier conventions for finite-coordinate codes. A linear code over a semiring, usually a finite field, is a submodule of the word space, while an additive code over a commutative additive group is an additive subgroup. Consequently, the lattice operations, maps, comaps, and membership notation are exactly those of Submodule and AddSubgroup rather than parallel wrappers.

These aliases let matrix presentations, Hamming invariants, and duality share Mathlib's existing subobject APIs. Coordinate types are arbitrary; results about dimensions or matrices add finiteness assumptions where needed, and particular codes may use Fin n to display a conventional matrix.

@[reducible, inline]

abbrev TauCeti.LinearCode (R : Type u_1) (ι : Type u_2) [Semiring R] : Type (max u_1 u_2)

A linear code over R with coordinate set ι is a submodule of the word space ι → R. Over a field this is a linear subspace; over a ring such as ZMod 4 it is a ring-linear code.

@[reducible, inline]

abbrev TauCeti.AdditiveCode (A : Type u_1) (ι : Type u_2) [AddCommGroup A] : Type (max u_1 u_2)

An additive code over A with coordinate set ι is an additive subgroup of the word space ι → A. No scalar closure is implicit in this notion.