Operations on even and doubly-even binary codes

Evenness and double evenness are preserved by direct sums and by monomial equivalence, hence also by coordinate permutations. Over the binary field every unit is one and the only field automorphism is the identity, so semilinear, monomial, and permutation equivalence all agree, by TauCeti.isSemilinearEquivalent_iff_isMonomialEquivalent and TauCeti.isMonomialEquivalent_iff_isPermutationEquivalent; in particular both properties are also invariant under semilinear equivalence.

These results provide the closure properties used to build larger self-orthogonal binary codes from smaller ones without changing the divisibility conditions on their Hamming weights.

The conventions follow Huffman and Pless, Fundamentals of Error-Correcting Codes, Chapters 1 and 9.

Direct sums

@[simp]

theorem TauCeti.BinaryCode.isEven_directSum_iff {ι : Type u_1} {κ : Type u_2} {C : LinearCode (ZMod 2) ι} {D : LinearCode (ZMod 2) κ} [Fintype ι] [Fintype κ] : IsEven (Submodule.directSum C D) ↔ IsEven C ∧ IsEven D

A direct sum of binary codes is even exactly when both summands are even.

theorem TauCeti.BinaryCode.IsEven.directSum {ι : Type u_1} {κ : Type u_2} {C : LinearCode (ZMod 2) ι} {D : LinearCode (ZMod 2) κ} [Fintype ι] [Fintype κ] (hC : IsEven C) (hD : IsEven D) : IsEven (Submodule.directSum C D)

The direct sum of two even binary codes is even.

@[simp]

theorem TauCeti.BinaryCode.isDoublyEven_directSum_iff {ι : Type u_1} {κ : Type u_2} {C : LinearCode (ZMod 2) ι} {D : LinearCode (ZMod 2) κ} [Fintype ι] [Fintype κ] : IsDoublyEven (Submodule.directSum C D) ↔ IsDoublyEven C ∧ IsDoublyEven D

A direct sum of binary codes is doubly even exactly when both summands are doubly even.

theorem TauCeti.BinaryCode.IsDoublyEven.directSum {ι : Type u_1} {κ : Type u_2} {C : LinearCode (ZMod 2) ι} {D : LinearCode (ZMod 2) κ} [Fintype ι] [Fintype κ] (hC : IsDoublyEven C) (hD : IsDoublyEven D) : IsDoublyEven (Submodule.directSum C D)

The direct sum of two doubly-even binary codes is doubly even.

Equivalence invariance

theorem TauCeti.BinaryCode.isEven_iff_of_isMonomialEquivalent {ι : Type u_1} {κ : Type u_2} {C : LinearCode (ZMod 2) ι} {D : LinearCode (ZMod 2) κ} [Fintype ι] [Fintype κ] (h : IsMonomialEquivalent C D) : IsEven C ↔ IsEven D

Evenness of binary codes is invariant under monomial equivalence.

theorem TauCeti.BinaryCode.IsEven.of_isMonomialEquivalent {ι : Type u_1} {κ : Type u_2} {C : LinearCode (ZMod 2) ι} {D : LinearCode (ZMod 2) κ} [Fintype ι] [Fintype κ] (hC : IsEven C) (h : IsMonomialEquivalent C D) : IsEven D

Monomial equivalence preserves evenness of binary codes.

theorem TauCeti.BinaryCode.isEven_iff_of_isPermutationEquivalent {ι : Type u_1} {κ : Type u_2} {C : LinearCode (ZMod 2) ι} {D : LinearCode (ZMod 2) κ} [Fintype ι] [Fintype κ] (h : IsPermutationEquivalent C D) : IsEven C ↔ IsEven D

Evenness of binary codes is invariant under permutation equivalence.

theorem TauCeti.BinaryCode.IsEven.of_isPermutationEquivalent {ι : Type u_1} {κ : Type u_2} {C : LinearCode (ZMod 2) ι} {D : LinearCode (ZMod 2) κ} [Fintype ι] [Fintype κ] (hC : IsEven C) (h : IsPermutationEquivalent C D) : IsEven D

Permutation equivalence preserves evenness of binary codes.

theorem TauCeti.BinaryCode.isDoublyEven_iff_of_isMonomialEquivalent {ι : Type u_1} {κ : Type u_2} {C : LinearCode (ZMod 2) ι} {D : LinearCode (ZMod 2) κ} [Fintype ι] [Fintype κ] (h : IsMonomialEquivalent C D) : IsDoublyEven C ↔ IsDoublyEven D

Double evenness of binary codes is invariant under monomial equivalence.

theorem TauCeti.BinaryCode.IsDoublyEven.of_isMonomialEquivalent {ι : Type u_1} {κ : Type u_2} {C : LinearCode (ZMod 2) ι} {D : LinearCode (ZMod 2) κ} [Fintype ι] [Fintype κ] (hC : IsDoublyEven C) (h : IsMonomialEquivalent C D) : IsDoublyEven D

Monomial equivalence preserves double evenness of binary codes.

theorem TauCeti.BinaryCode.isDoublyEven_iff_of_isPermutationEquivalent {ι : Type u_1} {κ : Type u_2} {C : LinearCode (ZMod 2) ι} {D : LinearCode (ZMod 2) κ} [Fintype ι] [Fintype κ] (h : IsPermutationEquivalent C D) : IsDoublyEven C ↔ IsDoublyEven D

Double evenness of binary codes is invariant under permutation equivalence.

theorem TauCeti.BinaryCode.IsDoublyEven.of_isPermutationEquivalent {ι : Type u_1} {κ : Type u_2} {C : LinearCode (ZMod 2) ι} {D : LinearCode (ZMod 2) κ} [Fintype ι] [Fintype κ] (hC : IsDoublyEven C) (h : IsPermutationEquivalent C D) : IsDoublyEven D

Permutation equivalence preserves double evenness of binary codes.

theorem TauCeti.BinaryCode.isEven_iff_of_isSemilinearEquivalent {ι : Type u_1} {κ : Type u_2} {C : LinearCode (ZMod 2) ι} {D : LinearCode (ZMod 2) κ} [Fintype ι] [Fintype κ] (h : IsSemilinearEquivalent C D) : IsEven C ↔ IsEven D

Evenness of binary codes is invariant under semilinear equivalence.

theorem TauCeti.BinaryCode.IsEven.of_isSemilinearEquivalent {ι : Type u_1} {κ : Type u_2} {C : LinearCode (ZMod 2) ι} {D : LinearCode (ZMod 2) κ} [Fintype ι] [Fintype κ] (hC : IsEven C) (h : IsSemilinearEquivalent C D) : IsEven D

Semilinear equivalence preserves evenness of binary codes.

theorem TauCeti.BinaryCode.isDoublyEven_iff_of_isSemilinearEquivalent {ι : Type u_1} {κ : Type u_2} {C : LinearCode (ZMod 2) ι} {D : LinearCode (ZMod 2) κ} [Fintype ι] [Fintype κ] (h : IsSemilinearEquivalent C D) : IsDoublyEven C ↔ IsDoublyEven D

Double evenness of binary codes is invariant under semilinear equivalence.

theorem TauCeti.BinaryCode.IsDoublyEven.of_isSemilinearEquivalent {ι : Type u_1} {κ : Type u_2} {C : LinearCode (ZMod 2) ι} {D : LinearCode (ZMod 2) κ} [Fintype ι] [Fintype κ] (hC : IsDoublyEven C) (h : IsSemilinearEquivalent C D) : IsDoublyEven D

Semilinear equivalence preserves double evenness of binary codes.