Direct sums of linear codes

This file defines the direct sum of two linear codes with an arbitrary module alphabet on the disjoint union of their coordinate types. A word belongs to the direct sum precisely when its restrictions to the two summands belong to the respective codes. Inclusion and equality of direct sums are therefore decided summandwise.

The direct sum is identified linearly with the product of the two codes. Consequently its dimension is the sum of the dimensions and its cardinality is the product of the cardinalities. Hamming weight and distance are additive across the two coordinate summands; consequently a natural number divides all weights of a direct sum exactly when it divides all weights of both summands. Canonical reindexings by the commutativity and associativity equivalences for Sum give the corresponding code identities. Relabelling, or monomially transforming, the two coordinate blocks separately acts on the two constituent codes separately. Hence permutation and monomial equivalence are compatible with direct sums, and the direct sum is commutative and associative up to permutation equivalence.

The construction follows the direct-sum convention in Huffman and Pless, Fundamentals of Error-Correcting Codes, Section 1.6.

def Submodule.directSum {R : Type u_1} {A : Type u_2} {ι : Type u_3} {κ : Type u_4} [Semiring R] [AddCommMonoid A] [Module R A] (C : Submodule R (ι → A)) (D : Submodule R (κ → A)) : Submodule R (ι ⊕ κ → A)

The direct sum of two linear codes, on the disjoint union of their coordinate types.

@[simp]

theorem Submodule.mem_directSum_iff {R : Type u_1} {A : Type u_2} {ι : Type u_3} {κ : Type u_4} [Semiring R] [AddCommMonoid A] [Module R A] {C : Submodule R (ι → A)} {D : Submodule R (κ → A)} {x : ι ⊕ κ → A} : x ∈ C.directSum D ↔ (fun (i : ι) => x (Sum.inl i)) ∈ C ∧ (fun (j : κ) => x (Sum.inr j)) ∈ D

A word belongs to a direct sum exactly when each of its two restrictions belongs to the corresponding code.

theorem Submodule.sumElim_zero_right_mem_directSum {R : Type u_1} {A : Type u_2} {ι : Type u_3} {κ : Type u_4} [Semiring R] [AddCommMonoid A] [Module R A] {C : Submodule R (ι → A)} (D : Submodule R (κ → A)) {x : ι → A} (hx : x ∈ C) : Sum.elim x 0 ∈ C.directSum D

A word of the first code, extended by zeros, belongs to a direct sum.

theorem Submodule.sumElim_zero_left_mem_directSum {R : Type u_1} {A : Type u_2} {ι : Type u_3} {κ : Type u_4} [Semiring R] [AddCommMonoid A] [Module R A] (C : Submodule R (ι → A)) {D : Submodule R (κ → A)} {y : κ → A} (hy : y ∈ D) : Sum.elim 0 y ∈ C.directSum D

A word of the second code, extended by zeros, belongs to a direct sum.

def Submodule.directSumEquivProd {R : Type u_1} {A : Type u_2} {ι : Type u_3} {κ : Type u_4} [Semiring R] [AddCommMonoid A] [Module R A] (C : Submodule R (ι → A)) (D : Submodule R (κ → A)) : ↥(C.directSum D) ≃ₗ[R] ↥C × ↥D

The direct sum is linearly equivalent to the product of its two constituent codes.

@[simp]

theorem Submodule.directSumEquivProd_apply_fst {R : Type u_1} {A : Type u_2} {ι : Type u_3} {κ : Type u_4} [Semiring R] [AddCommMonoid A] [Module R A] (C : Submodule R (ι → A)) (D : Submodule R (κ → A)) (x : ↥(C.directSum D)) (i : ι) : ↑((C.directSumEquivProd D) x).1 i = ↑x (Sum.inl i)

@[simp]

theorem Submodule.directSumEquivProd_apply_snd {R : Type u_1} {A : Type u_2} {ι : Type u_3} {κ : Type u_4} [Semiring R] [AddCommMonoid A] [Module R A] (C : Submodule R (ι → A)) (D : Submodule R (κ → A)) (x : ↥(C.directSum D)) (j : κ) : ↑((C.directSumEquivProd D) x).2 j = ↑x (Sum.inr j)

@[simp]

theorem Submodule.directSumEquivProd_symm_apply_inl {R : Type u_1} {A : Type u_2} {ι : Type u_3} {κ : Type u_4} [Semiring R] [AddCommMonoid A] [Module R A] (C : Submodule R (ι → A)) (D : Submodule R (κ → A)) (x : ↥C) (y : ↥D) (i : ι) : ↑((C.directSumEquivProd D).symm (x, y)) (Sum.inl i) = ↑x i

@[simp]

theorem Submodule.directSumEquivProd_symm_apply_inr {R : Type u_1} {A : Type u_2} {ι : Type u_3} {κ : Type u_4} [Semiring R] [AddCommMonoid A] [Module R A] (C : Submodule R (ι → A)) (D : Submodule R (κ → A)) (x : ↥C) (y : ↥D) (j : κ) : ↑((C.directSumEquivProd D).symm (x, y)) (Sum.inr j) = ↑y j

theorem Submodule.directSum_mono {R : Type u_1} {A : Type u_2} {ι : Type u_3} {κ : Type u_4} [Semiring R] [AddCommMonoid A] [Module R A] {C C' : Submodule R (ι → A)} {D D' : Submodule R (κ → A)} (hC : C ≤ C') (hD : D ≤ D') : C.directSum D ≤ C'.directSum D'

Direct sum is monotone in both constituent codes.

@[simp]

theorem Submodule.directSum_le_directSum_iff {R : Type u_1} {A : Type u_2} {ι : Type u_3} {κ : Type u_4} [Semiring R] [AddCommMonoid A] [Module R A] {C C' : Submodule R (ι → A)} {D D' : Submodule R (κ → A)} : C.directSum D ≤ C'.directSum D' ↔ C ≤ C' ∧ D ≤ D'

One direct sum lies in another exactly when the constituent codes lie in each other.

@[simp]

theorem Submodule.directSum_inj {R : Type u_1} {A : Type u_2} {ι : Type u_3} {κ : Type u_4} [Semiring R] [AddCommMonoid A] [Module R A] {C C' : Submodule R (ι → A)} {D D' : Submodule R (κ → A)} : C.directSum D = C'.directSum D' ↔ C = C' ∧ D = D'

Two direct sums are equal exactly when their constituent codes are equal.

@[simp]

theorem Submodule.map_directSum_sumComm {R : Type u_1} {A : Type u_2} {ι : Type u_3} {κ : Type u_4} [Semiring R] [AddCommMonoid A] [Module R A] (C : Submodule R (ι → A)) (D : Submodule R (κ → A)) : map (↑(LinearEquiv.funCongrLeft R A (Equiv.sumComm κ ι))) (C.directSum D) = D.directSum C

Reindexing a direct sum by swapping the coordinate summands swaps the two codes.

@[simp]

theorem Submodule.map_directSum_sumAssoc {R : Type u_1} {A : Type u_2} {ι : Type u_3} {κ : Type u_4} {ν : Type u_5} [Semiring R] [AddCommMonoid A] [Module R A] (C : Submodule R (ι → A)) (D : Submodule R (κ → A)) (E : Submodule R (ν → A)) : map (↑(LinearEquiv.funCongrLeft R A (Equiv.sumAssoc ι κ ν).symm)) ((C.directSum D).directSum E) = C.directSum (D.directSum E)

Reindexing an iterated direct sum by associating its coordinate summands associates the three codes in the same way.

@[simp]

theorem Submodule.map_directSum_sumCongr {R : Type u_1} {A : Type u_2} {ι : Type u_3} {κ : Type u_4} [Semiring R] [AddCommMonoid A] [Module R A] {ι' : Type u_6} {κ' : Type u_7} (C : Submodule R (ι → A)) (D : Submodule R (κ → A)) (e : ι' ≃ ι) (f : κ' ≃ κ) : map (↑(LinearEquiv.funCongrLeft R A (e.sumCongr f))) (C.directSum D) = (map (↑(LinearEquiv.funCongrLeft R A e)) C).directSum (map (↑(LinearEquiv.funCongrLeft R A f)) D)

Relabelling the two coordinate blocks of a direct sum separately relabels the two constituent codes.

theorem Submodule.isPermutationEquivalent_directSum_comm {R : Type u_1} {ι : Type u_3} {κ : Type u_4} [Semiring R] (C : Submodule R (ι → R)) (D : Submodule R (κ → R)) : TauCeti.IsPermutationEquivalent (C.directSum D) (D.directSum C)

A direct sum is permutation equivalent to the direct sum taken in the other order.

theorem Submodule.isPermutationEquivalent_directSum_assoc {R : Type u_1} {ι : Type u_3} {κ : Type u_4} {ν : Type u_5} [Semiring R] (C : Submodule R (ι → R)) (D : Submodule R (κ → R)) (E : Submodule R (ν → R)) : TauCeti.IsPermutationEquivalent ((C.directSum D).directSum E) (C.directSum (D.directSum E))

An iterated direct sum is permutation equivalent to the direct sum associated the other way.

@[simp]

theorem Submodule.map_directSum_monomialEquiv {R : Type u_1} {ι : Type u_3} {κ : Type u_4} [CommSemiring R] {ι' : Type u_6} {κ' : Type u_7} (C : Submodule R (ι → R)) (D : Submodule R (κ → R)) (u : ι → Rˣ) (v : κ → Rˣ) (e : ι ≃ ι') (f : κ ≃ κ') : map (↑(TauCeti.monomialEquiv (Sum.elim u v) (e.sumCongr f))) (C.directSum D) = (map (↑(TauCeti.monomialEquiv u e)) C).directSum (map (↑(TauCeti.monomialEquiv v f)) D)

A monomial transformation acting blockwise on the two coordinate summands maps a direct sum to the direct sum of the images of the two constituent codes.

@[simp]

theorem Submodule.finrank_directSum {R : Type u_1} {A : Type u_2} {ι : Type u_3} {κ : Type u_4} [Semiring R] [AddCommMonoid A] [Module R A] [StrongRankCondition R] (C : Submodule R (ι → A)) (D : Submodule R (κ → A)) [Module.Free R ↥C] [Module.Free R ↥D] [Module.Finite R ↥C] [Module.Finite R ↥D] : Module.finrank R ↥(C.directSum D) = Module.finrank R ↥C + Module.finrank R ↥D

The dimension of a direct sum is the sum of the dimensions of its constituent codes.

@[simp]

theorem Submodule.natCard_directSum {R : Type u_1} {A : Type u_2} {ι : Type u_3} {κ : Type u_4} [Semiring R] [AddCommMonoid A] [Module R A] (C : Submodule R (ι → A)) (D : Submodule R (κ → A)) : Nat.card ↥(C.directSum D) = Nat.card ↥C * Nat.card ↥D

The cardinality of a direct sum is the product of the cardinalities of its constituent codes.

@[simp]

theorem Submodule.hammingNorm_directSumEquivProd_symm {R : Type u_1} {A : Type u_2} {ι : Type u_3} {κ : Type u_4} [Semiring R] [AddCommMonoid A] [Module R A] [DecidableEq A] [Fintype ι] [Fintype κ] (C : Submodule R (ι → A)) (D : Submodule R (κ → A)) (x : ↥C) (y : ↥D) : hammingNorm ↑((C.directSumEquivProd D).symm (x, y)) = hammingNorm ↑x + hammingNorm ↑y

Hamming weight is additive on words in a direct sum.

theorem Submodule.forall_dvd_hammingNorm_directSum_iff {R : Type u_1} {A : Type u_2} {ι : Type u_3} {κ : Type u_4} [Semiring R] [AddCommMonoid A] [Module R A] [DecidableEq A] [Fintype ι] [Fintype κ] (C : Submodule R (ι → A)) (D : Submodule R (κ → A)) (k : ℕ) : (∀ z ∈ C.directSum D, k ∣ hammingNorm z) ↔ (∀ x ∈ C, k ∣ hammingNorm x) ∧ ∀ y ∈ D, k ∣ hammingNorm y

All weights of a direct sum are divisible by k exactly when this holds in both constituent codes.

@[simp]

theorem Submodule.hammingDist_directSumEquivProd_symm {R : Type u_1} {A : Type u_2} {ι : Type u_3} {κ : Type u_4} [Semiring R] [AddCommMonoid A] [Module R A] [DecidableEq A] [Fintype ι] [Fintype κ] (C : Submodule R (ι → A)) (D : Submodule R (κ → A)) (x x' : ↥C) (y y' : ↥D) : hammingDist ↑((C.directSumEquivProd D).symm (x, y)) ↑((C.directSumEquivProd D).symm (x', y')) = hammingDist ↑x ↑x' + hammingDist ↑y ↑y'

Hamming distance is additive on pairs of words in a direct sum.

theorem TauCeti.IsPermutationEquivalent.directSum {R : Type u_1} {ι : Type u_2} {κ : Type u_3} {ι' : Type u_4} {κ' : Type u_5} [Semiring R] {C : Submodule R (ι → R)} {C' : Submodule R (ι' → R)} {D : Submodule R (κ → R)} {D' : Submodule R (κ' → R)} (hC : IsPermutationEquivalent C C') (hD : IsPermutationEquivalent D D') : IsPermutationEquivalent (C.directSum D) (C'.directSum D')

Permutation equivalence is compatible with direct sums: relabellings of the two summands combine to a relabelling of the direct sum.

theorem TauCeti.IsMonomialEquivalent.directSum {R : Type u_1} {ι : Type u_2} {κ : Type u_3} {ι' : Type u_4} {κ' : Type u_5} [CommSemiring R] {C : Submodule R (ι → R)} {C' : Submodule R (ι' → R)} {D : Submodule R (κ → R)} {D' : Submodule R (κ' → R)} (hC : IsMonomialEquivalent C C') (hD : IsMonomialEquivalent D D') : IsMonomialEquivalent (C.directSum D) (C'.directSum D')

Monomial equivalence is compatible with direct sums: monomial transformations of the two summands combine blockwise to one of the direct sum.