Puncturing and shortening additive and linear codes

An additive code is an additive subgroup of the word space; its puncture is the image under restriction, and its shortening is the inverse image under extension by zero. These operations require only an abelian alphabet. Forgetting scalar closure commutes with both operations.

A linear code on coordinates ι is a submodule of the word space ι → F, as defined in TauCeti/InformationTheory/Coding/Basic.lean. Given a set s of coordinates to retain, puncturing restricts every codeword to s. Shortening first restricts to the codewords which vanish outside s, and then forgets those zero coordinates.

Neither the field nor the coordinate type is assumed finite; finiteness enters only in the dimension bounds. The API records membership, order preservation, the zero and whole-space cases, the comparison between shortening and puncturing, and dimension control. Restriction to the deleted coordinates has the shortened code as its kernel, so dim shorten C s + dim puncture C sᶜ = dim C. For a single deleted coordinate i this gives the exact dimensions: shortening at i drops the dimension by one precisely when some codeword is nonzero at i, and puncturing at i drops it by one precisely when the unit word at i is a codeword.

Main declarations

• puncture: restriction of a code to a retained coordinate set.
• shorten: restriction after imposing zero outside the retained coordinate set.
• punctureAt and shortenAt: the corresponding operations deleting one coordinate.
• mem_puncture and mem_shorten: membership characterizations.
• finrank_puncture_le, finrank_puncture_eq, and finrank_shorten_eq: dimension control.
• finrank_shorten_add_finrank_puncture_compl: rank–nullity for shortening and puncturing.
• finrank_shortenAt_add_one_of_exists_ne_zero and finrank_punctureAt_add_one_of_single_mem: the exact dimension drop when deleting one coordinate.

References

• W. C. Huffman and V. Pless, Fundamentals of Error-Correcting Codes, Cambridge University Press, 2003, Sections 1.5 and 1.6.

def TauCeti.AdditiveCode.puncture {A : Type u_1} {ι : Type u_2} [AddCommGroup A] (C : AdditiveCode A ι) (s : Set ι) : AdditiveCode A ↑s

Puncturing an additive code retains precisely the coordinates in s.

theorem TauCeti.AdditiveCode.puncture_def {A : Type u_1} {ι : Type u_2} [AddCommGroup A] (C : AdditiveCode A ι) (s : Set ι) : C.puncture s = AddSubgroup.map (AddMonoidHom.pi fun (i : ↑s) => Pi.evalAddMonoidHom (fun (x : ι) => A) ↑i) C

Puncturing is the image under the coordinate restriction homomorphism.

noncomputable def TauCeti.AdditiveCode.shorten {A : Type u_1} {ι : Type u_2} [AddCommGroup A] (C : AdditiveCode A ι) (s : Set ι) : AdditiveCode A ↑s

Shortening retains the words whose extension by zero is a codeword.

theorem TauCeti.AdditiveCode.shorten_def {A : Type u_1} {ι : Type u_2} [AddCommGroup A] (C : AdditiveCode A ι) (s : Set ι) : C.shorten s = AddSubgroup.comap (Function.ExtendByZero.hom A Subtype.val) C

Shortening is the inverse image under extension by zero.

@[simp]

theorem TauCeti.AdditiveCode.mem_puncture {A : Type u_1} {ι : Type u_2} [AddCommGroup A] {C : AdditiveCode A ι} {s : Set ι} {y : ↑s → A} : y ∈ C.puncture s ↔ ∃ x ∈ C, ∀ (i : ↑s), x ↑i = y i

A word belongs to the punctured code exactly when it restricts a codeword.

@[simp]

theorem TauCeti.AdditiveCode.mem_shorten_iff_extend_mem {A : Type u_1} {ι : Type u_2} [AddCommGroup A] {C : AdditiveCode A ι} {s : Set ι} {y : ↑s → A} : y ∈ C.shorten s ↔ Function.extend Subtype.val y 0 ∈ C

A word belongs to the shortened code exactly when its extension by zero belongs to the original code.

theorem TauCeti.AdditiveCode.mem_shorten {A : Type u_1} {ι : Type u_2} [AddCommGroup A] {C : AdditiveCode A ι} {s : Set ι} {y : ↑s → A} : y ∈ C.shorten s ↔ ∃ x ∈ C, (∀ i ∉ s, x i = 0) ∧ ∀ (j : ↑s), x ↑j = y j

Equivalently, shortening restricts the codewords that vanish outside the retained set.

theorem TauCeti.AdditiveCode.shorten_le_puncture {A : Type u_1} {ι : Type u_2} [AddCommGroup A] (C : AdditiveCode A ι) (s : Set ι) : C.shorten s ≤ C.puncture s

Every shortened word is a punctured word.

theorem TauCeti.AdditiveCode.puncture_mono {A : Type u_1} {ι : Type u_2} [AddCommGroup A] {C D : AdditiveCode A ι} (h : C ≤ D) (s : Set ι) : C.puncture s ≤ D.puncture s

Puncturing preserves inclusion of additive codes.

theorem TauCeti.AdditiveCode.shorten_mono {A : Type u_1} {ι : Type u_2} [AddCommGroup A] {C D : AdditiveCode A ι} (h : C ≤ D) (s : Set ι) : C.shorten s ≤ D.shorten s

Shortening preserves inclusion of additive codes.

@[simp]

theorem TauCeti.AdditiveCode.puncture_bot {A : Type u_1} {ι : Type u_2} [AddCommGroup A] (s : Set ι) : ⊥.puncture s = ⊥

Puncturing the zero code gives the zero code.

@[simp]

theorem TauCeti.AdditiveCode.shorten_bot {A : Type u_1} {ι : Type u_2} [AddCommGroup A] (s : Set ι) : ⊥.shorten s = ⊥

Shortening the zero code gives the zero code.

@[simp]

theorem TauCeti.AdditiveCode.puncture_top {A : Type u_1} {ι : Type u_2} [AddCommGroup A] (s : Set ι) : ⊤.puncture s = ⊤

Puncturing the whole word space gives the whole retained word space.

@[simp]

theorem TauCeti.AdditiveCode.shorten_top {A : Type u_1} {ι : Type u_2} [AddCommGroup A] (s : Set ι) : ⊤.shorten s = ⊤

Shortening the whole word space gives the whole retained word space.

noncomputable def TauCeti.puncture {F : Type u_1} [Field F] {ι : Type u_2} (C : LinearCode F ι) (s : Set ι) : LinearCode F ↑s

Puncturing a code at s retains precisely the coordinates in s.

theorem TauCeti.puncture_def {F : Type u_1} [Field F] {ι : Type u_2} (C : LinearCode F ι) (s : Set ι) : puncture C s = Submodule.map (LinearMap.funLeft F F Subtype.val) C

Puncturing is the image under restriction to the retained coordinates.

noncomputable def TauCeti.shorten {F : Type u_1} [Field F] {ι : Type u_2} (C : LinearCode F ι) (s : Set ι) : LinearCode F ↑s

Shortening a code at s first imposes zero outside s, then retains the coordinates in s.

theorem TauCeti.shorten_def {F : Type u_1} [Field F] {ι : Type u_2} (C : LinearCode F ι) (s : Set ι) : shorten C s = Submodule.map (LinearMap.funLeft F F Subtype.val) (C ⊓ Submodule.pi sᶜ fun (x : ι) => ⊥)

Shortening is the image under restriction of the words supported on the retained set.

@[simp]

theorem TauCeti.LinearCode.puncture_toAddSubgroup {F : Type u_1} [Field F] {ι : Type u_2} (C : LinearCode F ι) (s : Set ι) : Submodule.toAddSubgroup (puncture C s) = AdditiveCode.puncture (Submodule.toAddSubgroup C) s

Forgetting scalar closure commutes with puncturing a linear code.

@[simp]

theorem TauCeti.LinearCode.shorten_toAddSubgroup {F : Type u_1} [Field F] {ι : Type u_2} (C : LinearCode F ι) (s : Set ι) : Submodule.toAddSubgroup (shorten C s) = AdditiveCode.shorten (Submodule.toAddSubgroup C) s

Forgetting scalar closure commutes with shortening a linear code.

@[simp]

theorem TauCeti.mem_puncture {F : Type u_1} [Field F] {ι : Type u_2} {C : LinearCode F ι} {s : Set ι} {y : ↑s → F} : y ∈ puncture C s ↔ ∃ x ∈ C, ∀ (j : ↑s), x ↑j = y j

A word belongs to the punctured code exactly when it is the restriction of a codeword.

@[simp]

theorem TauCeti.mem_shorten {F : Type u_1} [Field F] {ι : Type u_2} {C : LinearCode F ι} {s : Set ι} {y : ↑s → F} : y ∈ shorten C s ↔ ∃ x ∈ C, (∀ i ∉ s, x i = 0) ∧ ∀ (j : ↑s), x ↑j = y j

A word belongs to the shortened code exactly when its extension by zero is a codeword: equivalently, it is the restriction of a codeword which vanishes off the retained set.

theorem TauCeti.mem_shorten_iff_extend_mem {F : Type u_1} [Field F] {ι : Type u_2} {C : LinearCode F ι} {s : Set ι} {y : ↑s → F} : y ∈ shorten C s ↔ Function.extend Subtype.val y 0 ∈ C

A word on the retained coordinates belongs to the shortened code exactly when its extension by zero belongs to the original code.

theorem TauCeti.mem_puncture_singleton {F : Type u_1} [Field F] {ι : Type u_2} {C : LinearCode F ι} {i : ι} {y : ↑{i} → F} : y ∈ puncture C {i} ↔ ∃ x ∈ C, x i = y ⟨i, ⋯⟩

Membership in a puncture retaining one coordinate is determined by that coordinate.

theorem TauCeti.mem_shorten_singleton {F : Type u_1} [Field F] {ι : Type u_2} {C : LinearCode F ι} {i : ι} {y : ↑{i} → F} : y ∈ shorten C {i} ↔ ∃ x ∈ C, (∀ (j : ι), j ≠ i → x j = 0) ∧ x i = y ⟨i, ⋯⟩

Membership in a shortening retaining one coordinate is determined by a codeword supported at that coordinate.

noncomputable def TauCeti.punctureAt {F : Type u_1} [Field F] {ι : Type u_2} (C : LinearCode F ι) (i : ι) : LinearCode F ↑{i}ᶜ

Puncturing at i deletes that coordinate and retains all the others.

theorem TauCeti.punctureAt_def {F : Type u_1} [Field F] {ι : Type u_2} (C : LinearCode F ι) (i : ι) : punctureAt C i = puncture C {i}ᶜ

Puncturing at one coordinate is puncturing with its singleton complement retained.

noncomputable def TauCeti.shortenAt {F : Type u_1} [Field F] {ι : Type u_2} (C : LinearCode F ι) (i : ι) : LinearCode F ↑{i}ᶜ

Shortening at i imposes zero there and retains all the other coordinates.

theorem TauCeti.shortenAt_def {F : Type u_1} [Field F] {ι : Type u_2} (C : LinearCode F ι) (i : ι) : shortenAt C i = shorten C {i}ᶜ

Shortening at one coordinate is shortening with its singleton complement retained.

@[simp]

theorem TauCeti.mem_punctureAt {F : Type u_1} [Field F] {ι : Type u_2} {C : LinearCode F ι} {i : ι} {y : ↑{i}ᶜ → F} : y ∈ punctureAt C i ↔ ∃ x ∈ C, ∀ (j : ↑{i}ᶜ), x ↑j = y j

A word belongs to the code punctured at i exactly when it is the restriction of a codeword to the other coordinates.

@[simp]

theorem TauCeti.mem_shortenAt {F : Type u_1} [Field F] {ι : Type u_2} {C : LinearCode F ι} {i : ι} {y : ↑{i}ᶜ → F} : y ∈ shortenAt C i ↔ ∃ x ∈ C, x i = 0 ∧ ∀ (j : ↑{i}ᶜ), x ↑j = y j

A word belongs to the code shortened at i exactly when it extends to a codeword which is zero at i.

theorem TauCeti.shorten_le_puncture {F : Type u_1} [Field F] {ι : Type u_2} (C : LinearCode F ι) (s : Set ι) : shorten C s ≤ puncture C s

Every shortened word is a punctured word.

theorem TauCeti.puncture_mono {F : Type u_1} [Field F] {ι : Type u_2} {C D : LinearCode F ι} (h : C ≤ D) (s : Set ι) : puncture C s ≤ puncture D s

Puncturing is monotone in the code.

theorem TauCeti.shorten_mono {F : Type u_1} [Field F] {ι : Type u_2} {C D : LinearCode F ι} (h : C ≤ D) (s : Set ι) : shorten C s ≤ shorten D s

Shortening is monotone in the code.

@[simp]

theorem TauCeti.puncture_bot {F : Type u_1} [Field F] {ι : Type u_2} (s : Set ι) : puncture ⊥ s = ⊥

Puncturing sends the zero code to the zero code.

@[simp]

theorem TauCeti.shorten_bot {F : Type u_1} [Field F] {ι : Type u_2} (s : Set ι) : shorten ⊥ s = ⊥

Shortening sends the zero code to the zero code.

@[simp]

theorem TauCeti.puncture_top {F : Type u_1} [Field F] {ι : Type u_2} (s : Set ι) : puncture ⊤ s = ⊤

Puncturing the whole word space gives the whole word space on the retained coordinates.

@[simp]

theorem TauCeti.shorten_top {F : Type u_1} [Field F] {ι : Type u_2} (s : Set ι) : shorten ⊤ s = ⊤

Shortening the whole word space gives the whole word space on the retained coordinates.

theorem TauCeti.puncture_singleton_eq_top_iff {F : Type u_1} [Field F] {ι : Type u_2} {C : LinearCode F ι} {i : ι} : puncture C {i} = ⊤ ↔ ∃ x ∈ C, x i ≠ 0

Puncturing to a single retained coordinate i gives the whole word space on {i} exactly when some codeword is nonzero at i.

theorem TauCeti.shorten_singleton_eq_top_iff {F : Type u_1} [Field F] {ι : Type u_2} [DecidableEq ι] {C : LinearCode F ι} {i : ι} : shorten C {i} = ⊤ ↔ Pi.single i 1 ∈ C

Shortening to a single retained coordinate i gives the whole word space on {i} exactly when the unit word at i is a codeword.

@[simp]

theorem TauCeti.puncture_sup {F : Type u_1} [Field F] {ι : Type u_2} (C D : LinearCode F ι) (s : Set ι) : puncture (C ⊔ D) s = puncture C s ⊔ puncture D s

Puncturing commutes with sums of codes.

@[simp]

theorem TauCeti.shorten_inf {F : Type u_1} [Field F] {ι : Type u_2} (C D : LinearCode F ι) (s : Set ι) : shorten (C ⊓ D) s = shorten C s ⊓ shorten D s

Shortening commutes with intersections.

theorem TauCeti.finrank_puncture_le {F : Type u_1} [Field F] {ι : Type u_2} (C : LinearCode F ι) [FiniteDimensional F ↥C] (s : Set ι) : Module.finrank F ↥(puncture C s) ≤ Module.finrank F ↥C

Puncturing cannot increase dimension.

theorem TauCeti.finrank_puncture_eq {F : Type u_1} [Field F] {ι : Type u_2} (C : LinearCode F ι) (s : Set ι) (h : ∀ x ∈ C, (∀ (j : ↑s), x ↑j = 0) → x = 0) : Module.finrank F ↥(puncture C s) = Module.finrank F ↥C

Puncturing preserves dimension when the only codeword vanishing at every retained coordinate is zero.

theorem TauCeti.finrank_shorten_eq {F : Type u_1} [Field F] {ι : Type u_2} (C : LinearCode F ι) (s : Set ι) : Module.finrank F ↥(shorten C s) = Module.finrank F ↥(C ⊓ Submodule.pi sᶜ fun (x : ι) => ⊥)

Shortening preserves the dimension of the subcode of words supported on the retained coordinates.

theorem TauCeti.finrank_shorten_le {F : Type u_1} [Field F] {ι : Type u_2} (C : LinearCode F ι) [FiniteDimensional F ↥C] (s : Set ι) : Module.finrank F ↥(shorten C s) ≤ Module.finrank F ↥C

Shortening cannot increase dimension.

theorem TauCeti.finrank_shorten_add_finrank_puncture_compl {F : Type u_1} [Field F] {ι : Type u_2} (C : LinearCode F ι) [FiniteDimensional F ↥C] (s : Set ι) : Module.finrank F ↥(shorten C s) + Module.finrank F ↥(puncture C sᶜ) = Module.finrank F ↥C

Rank–nullity for shortening and puncturing. Restricting a code to the deleted coordinates sᶜ has kernel the words vanishing off s, which is the shortened code; so the dimensions of shorten C s and puncture C sᶜ add up to the dimension of C.

theorem TauCeti.finrank_puncture_add_finrank_shorten_compl {F : Type u_1} [Field F] {ι : Type u_2} (C : LinearCode F ι) [FiniteDimensional F ↥C] (s : Set ι) : Module.finrank F ↥(puncture C s) + Module.finrank F ↥(shorten C sᶜ) = Module.finrank F ↥C

The dimensions of puncture C s and shorten C sᶜ add up to the dimension of C.

theorem TauCeti.finrank_le_finrank_shorten_add_ncard_compl {F : Type u_1} [Field F] {ι : Type u_2} [Finite ι] (C : LinearCode F ι) (s : Set ι) : Module.finrank F ↥C ≤ Module.finrank F ↥(shorten C s) + sᶜ.ncard

The dimension lost by shortening is at most the number of deleted coordinates.

theorem TauCeti.finrank_le_finrank_puncture_add_ncard_compl {F : Type u_1} [Field F] {ι : Type u_2} [Finite ι] (C : LinearCode F ι) (s : Set ι) : Module.finrank F ↥C ≤ Module.finrank F ↥(puncture C s) + sᶜ.ncard

The dimension lost by puncturing is at most the number of deleted coordinates.

Deleting one coordinate

theorem TauCeti.finrank_shortenAt_add_one_of_exists_ne_zero {F : Type u_1} [Field F] {ι : Type u_2} (C : LinearCode F ι) [FiniteDimensional F ↥C] {i : ι} (h : ∃ x ∈ C, x i ≠ 0) : Module.finrank F ↥(shortenAt C i) + 1 = Module.finrank F ↥C

Shortening at i lowers the dimension by exactly one when some codeword is nonzero at i.

theorem TauCeti.finrank_shortenAt_of_forall_eq_zero {F : Type u_1} [Field F] {ι : Type u_2} (C : LinearCode F ι) {i : ι} (h : ∀ x ∈ C, x i = 0) : Module.finrank F ↥(shortenAt C i) = Module.finrank F ↥C

Shortening at i preserves the dimension when every codeword vanishes at i.

theorem TauCeti.finrank_punctureAt_add_one_of_single_mem {F : Type u_1} [Field F] {ι : Type u_2} [DecidableEq ι] (C : LinearCode F ι) [FiniteDimensional F ↥C] {i : ι} (h : Pi.single i 1 ∈ C) : Module.finrank F ↥(punctureAt C i) + 1 = Module.finrank F ↥C

Puncturing at i lowers the dimension by exactly one when the unit word at i is a codeword.

theorem TauCeti.finrank_punctureAt_of_single_notMem {F : Type u_1} [Field F] {ι : Type u_2} [DecidableEq ι] (C : LinearCode F ι) {i : ι} (h : Pi.single i 1 ∉ C) : Module.finrank F ↥(punctureAt C i) = Module.finrank F ↥C

Puncturing at i preserves the dimension when the unit word at i is not a codeword.