Monomial and permutation equivalences of linear codes

A monomial transformation of the coordinate space ι → R rescales each coordinate by a unit of R and then relabels the coordinates along an equivalence of index types; a permutation transformation only relabels. Two linear codes — unbundled submodules of coordinate spaces — are monomially, respectively permutation, equivalent when such a transformation carries one onto the other. These are the transformations preserving all Hamming data of a code, so weights, weight distributions, pairwise Hamming distances and minimum distance are invariants of the resulting equivalence classes.

The coordinate transformations and their ambient monomial and permutation groups are defined in TauCeti.LinearAlgebra.Monomial. This file develops their Hamming invariants and their actions on codes.

Main definitions

• TauCeti.signedEquiv u e: the monomial equivalence induced by integer signs and a coordinate relabelling, available over every commutative ring.
• TauCeti.IsMonomialEquivalent, TauCeti.IsPermutationEquivalent: the two resulting equivalence relations on linear codes.
• TauCeti.monomialAut C: the monomial automorphism group of a code, acting on its codewords.
• TauCeti.permutationAut C: the coordinate-permutation automorphism group of a code.

Main statements

• TauCeti.hammingNorm_monomialEquiv, TauCeti.hammingDist_monomialEquiv: a monomial equivalence preserves Hamming weight and Hamming distance.
• TauCeti.hammingNorm_signedEquiv: so does a signed coordinate change, for Hamming weight.
• TauCeti.IsMonomialEquivalent.finrank_eq, TauCeti.IsMonomialEquivalent.card_eq: monomially equivalent codes have the same dimension and the same number of codewords.
• TauCeti.IsPermutationEquivalent.finrank_eq, TauCeti.IsPermutationEquivalent.card_eq: the corresponding invariants for permutation-equivalent codes.
• TauCeti.IsMonomialEquivalent.hammingMinDist_eq, TauCeti.IsPermutationEquivalent.hammingMinDist_eq: equivalent codes have the same minimum distance, including under the zero-code convention.
• TauCeti.monomialGroup_eq_permutationGroup, TauCeti.isMonomialEquivalent_iff_isPermutationEquivalent, TauCeti.monomialAut_eq_permutationAut: over a ring whose only unit is one — the binary field in particular — monomial transformations are exactly coordinate permutations, so the two notions of equivalence and the two automorphism groups agree.

Invariance of the weight distribution and weight enumerator is in TauCeti.InformationTheory.Coding.Weight.Enumerator.

References

W. C. Huffman and V. Pless, Fundamentals of Error-Correcting Codes, Cambridge University Press (2003), §1.6.

Monomial transformations of a coordinate space

@[simp]

theorem TauCeti.hammingNorm_monomialEquiv {ι : Type u_1} {κ : Type u_2} {R : Type u_4} [CommSemiring R] [Fintype ι] [Fintype κ] [DecidableEq R] (u : ι → Rˣ) (e : ι ≃ κ) (x : ι → R) : hammingNorm ((monomialEquiv u e) x) = hammingNorm x

A monomial equivalence of finite coordinate spaces preserves Hamming weight.

@[simp]

theorem TauCeti.hammingDist_monomialEquiv {ι : Type u_1} {κ : Type u_2} {R : Type u_4} [CommSemiring R] [Fintype ι] [Fintype κ] [DecidableEq R] (u : ι → Rˣ) (e : ι ≃ κ) (x y : ι → R) : hammingDist ((monomialEquiv u e) x) ((monomialEquiv u e) y) = hammingDist x y

A monomial equivalence of finite coordinate spaces preserves Hamming distance.

Signed coordinate transformations

def TauCeti.signedEquiv {ι : Type u_1} {κ : Type u_2} {R : Type u_4} [CommRing R] (u : ι → ℤˣ) (e : ι ≃ κ) : (ι → R) ≃ₗ[R] κ → R

The monomial equivalence which multiplies coordinates by integer signs before relabelling them. It specializes coherently to every commutative ring.

theorem TauCeti.signedEquiv_one {ι : Type u_1} {κ : Type u_2} {R : Type u_4} [CommRing R] (e : ι ≃ κ) : signedEquiv 1 e = LinearEquiv.funCongrLeft R R e.symm

With trivial signs a signed coordinate change is a bare relabelling of coordinates.

@[simp]

theorem TauCeti.signedEquiv_apply {ι : Type u_1} {κ : Type u_2} {R : Type u_4} [CommRing R] (u : ι → ℤˣ) (e : ι ≃ κ) (x : ι → R) (j : κ) : (signedEquiv u e) x j = ↑↑(u (e.symm j)) * x (e.symm j)

Evaluation of a signed coordinate change.

@[simp]

theorem TauCeti.signedEquiv_signedEquiv {ι : Type u_1} {R : Type u_4} [CommRing R] (u : ι → ℤˣ) (x : ι → R) : (signedEquiv u (Equiv.refl ι)) ((signedEquiv u (Equiv.refl ι)) x) = x

A sign change of coordinates without relabelling is an involution.

@[simp]

theorem TauCeti.signedEquiv_toAddMonoidHom_apply {ι : Type u_1} {κ : Type u_2} {R : Type u_4} [CommRing R] (u : ι → ℤˣ) (e : ι ≃ κ) (x : ι → R) : (signedEquiv u e).toAddEquiv.toAddMonoidHom x = (signedEquiv u e) x

The additive homomorphism underlying a signed coordinate change has the same action as the ambient linear equivalence.

@[simp]

theorem TauCeti.signedEquiv_intCast {ι : Type u_1} {κ : Type u_2} {R : Type u_4} [CommRing R] (u : ι → ℤˣ) (e : ι ≃ κ) (z : ι → ℤ) : ((signedEquiv u e) fun (i : ι) => ↑(z i)) = fun (j : κ) => ↑((signedEquiv u e) z j)

Signed coordinate changes commute with taking integer coordinates in any commutative ring.

@[simp]

theorem TauCeti.signedEquiv_restrictScalars_apply {ι : Type u_1} {κ : Type u_2} (u : ι → ℤˣ) (e : ι ≃ κ) (x : ι → ℚ) : (LinearEquiv.restrictScalars ℤ (signedEquiv u e)) x = (signedEquiv u e) x

Restricting a rational signed coordinate change to integer scalars does not change its underlying function.

theorem TauCeti.monomialEquiv_eq_signedEquiv_of_intUnits {ι : Type u_1} {κ : Type u_2} {R : Type u_4} [CommRing R] (u : ι → Rˣ) (e : ι ≃ κ) (v : ι → ℤˣ) (hv : ∀ (i : ι), ↑↑(v i) = ↑(u i)) : monomialEquiv u e = signedEquiv v e

A monomial coordinate change agrees with a signed coordinate change when its coordinate units are images of integer units.

@[simp]

theorem TauCeti.hammingNorm_signedEquiv {ι : Type u_1} {κ : Type u_2} {R : Type u_4} [CommRing R] [Fintype ι] [Fintype κ] [DecidableEq R] (u : ι → ℤˣ) (e : ι ≃ κ) (x : ι → R) : hammingNorm ((signedEquiv u e) x) = hammingNorm x

A signed coordinate change of finite coordinate spaces preserves Hamming weight.

theorem TauCeti.exists_signed_monomialEquiv_iff {ι : Type u_1} {κ : Type u_2} {R : Type u_4} [CommRing R] (u : ι → Rˣ) (e : ι ≃ κ) : (∃ (v : ι → ℤˣ), monomialEquiv u e = signedEquiv v e) ↔ ∀ (i : ι), u i = 1 ∨ u i = -1

A monomial map over a commutative ring is a signed coordinate change exactly when each multiplier is 1 or -1.

@[simp]

theorem TauCeti.dotProduct_signedEquiv {ι : Type u_1} {κ : Type u_2} {R : Type u_4} [CommRing R] [Fintype ι] [Fintype κ] (u : ι → ℤˣ) (e : ι ≃ κ) (x y : ι → R) : (signedEquiv u e) x ⬝ᵥ (signedEquiv u e) y = x ⬝ᵥ y

A signed coordinate change preserves the standard dot product.

Permutation equivalence of linear codes

def TauCeti.IsPermutationEquivalent {R : Type u_1} {ι : Type u_2} {κ : Type u_3} [Semiring R] (C : Submodule R (ι → R)) (D : Submodule R (κ → R)) : Prop

Two linear codes are permutation equivalent when a relabelling of the coordinates carries one onto the other.

theorem TauCeti.isPermutationEquivalent_iff {R : Type u_1} {ι : Type u_2} {κ : Type u_3} [Semiring R] {C : Submodule R (ι → R)} {D : Submodule R (κ → R)} : IsPermutationEquivalent C D ↔ ∃ (e : ι ≃ κ), Submodule.map (↑(LinearEquiv.funCongrLeft R R e.symm)) C = D

Unfolds permutation equivalence to the existence of a relabelling carrying one code onto the other.

def TauCeti.permutationCodeEquiv {R : Type u_1} {ι : Type u_2} {κ : Type u_3} [Semiring R] {C : Submodule R (ι → R)} {D : Submodule R (κ → R)} (e : ι ≃ κ) (h : Submodule.map (↑(LinearEquiv.funCongrLeft R R e.symm)) C = D) : ↥C ≃ₗ[R] ↥D

A coordinate relabelling that maps one code onto another restricts to a linear equivalence between their codewords.

@[simp]

theorem TauCeti.coe_permutationCodeEquiv_apply {R : Type u_3} {ι : Type u_1} {κ : Type u_2} [Semiring R] {C : Submodule R (ι → R)} {D : Submodule R (κ → R)} (e : ι ≃ κ) (h : Submodule.map (↑(LinearEquiv.funCongrLeft R R e.symm)) C = D) (x : ↥C) : ↑((permutationCodeEquiv e h) x) = (LinearMap.funLeft R R ⇑e.symm) ↑x

permutationCodeEquiv acts on codewords by the ambient relabelling LinearEquiv.funCongrLeft R R e.symm, in its simp normal form LinearMap.funLeft R R e.symm.

@[simp]

theorem TauCeti.coe_permutationCodeEquiv_symm_apply {R : Type u_3} {ι : Type u_1} {κ : Type u_2} [Semiring R] {C : Submodule R (ι → R)} {D : Submodule R (κ → R)} (e : ι ≃ κ) (h : Submodule.map (↑(LinearEquiv.funCongrLeft R R e.symm)) C = D) (y : ↥D) : ↑((permutationCodeEquiv e h).symm y) = (LinearMap.funLeft R R ⇑e) ↑y

The inverse of permutationCodeEquiv acts on codewords by the inverse relabelling.

theorem TauCeti.IsPermutationEquivalent.refl {R : Type u_1} {ι : Type u_2} [Semiring R] (C : Submodule R (ι → R)) : IsPermutationEquivalent C C

theorem TauCeti.IsPermutationEquivalent.symm {R : Type u_1} {ι : Type u_2} {κ : Type u_3} [Semiring R] {C : Submodule R (ι → R)} {D : Submodule R (κ → R)} (h : IsPermutationEquivalent C D) : IsPermutationEquivalent D C

theorem TauCeti.IsPermutationEquivalent.trans {R : Type u_1} {ι : Type u_2} {κ : Type u_3} {μ : Type u_4} [Semiring R] {C : Submodule R (ι → R)} {D : Submodule R (κ → R)} {E : Submodule R (μ → R)} (h : IsPermutationEquivalent C D) (h' : IsPermutationEquivalent D E) : IsPermutationEquivalent C E

theorem TauCeti.IsPermutationEquivalent.finrank_eq {R : Type u_1} {ι : Type u_2} {κ : Type u_3} [Semiring R] {C : Submodule R (ι → R)} {D : Submodule R (κ → R)} (h : IsPermutationEquivalent C D) : Module.finrank R ↥C = Module.finrank R ↥D

Permutation-equivalent codes have the same dimension.

theorem TauCeti.IsPermutationEquivalent.card_eq {R : Type u_1} {ι : Type u_2} {κ : Type u_3} [Semiring R] {C : Submodule R (ι → R)} {D : Submodule R (κ → R)} (h : IsPermutationEquivalent C D) : Nat.card ↥C = Nat.card ↥D

Permutation-equivalent codes have the same number of codewords.

theorem TauCeti.IsPermutationEquivalent.hammingMinDist_eq {R : Type u_3} {ι : Type u_1} {κ : Type u_2} [Semiring R] {C : Submodule R (ι → R)} {D : Submodule R (κ → R)} [Fintype ι] [Fintype κ] [DecidableEq R] (h : IsPermutationEquivalent C D) : (↑C).hammingMinDist = (↑D).hammingMinDist

Permutation-equivalent codes have the same minimum distance.

Monomial equivalence of linear codes

def TauCeti.IsMonomialEquivalent {R : Type u_1} {ι : Type u_2} {κ : Type u_3} [CommSemiring R] (C : Submodule R (ι → R)) (D : Submodule R (κ → R)) : Prop

Two linear codes are monomially equivalent when some monomial transformation of the coordinate spaces carries one onto the other.

theorem TauCeti.isMonomialEquivalent_iff {R : Type u_1} {ι : Type u_2} {κ : Type u_3} [CommSemiring R] {C : Submodule R (ι → R)} {D : Submodule R (κ → R)} : IsMonomialEquivalent C D ↔ ∃ (u : ι → Rˣ) (e : ι ≃ κ), Submodule.map (↑(monomialEquiv u e)) C = D

Unfolds monomial equivalence to the existence of a monomial transformation carrying one code onto the other.

def TauCeti.monomialCodeEquiv {R : Type u_1} {ι : Type u_2} {κ : Type u_3} [CommSemiring R] {C : Submodule R (ι → R)} {D : Submodule R (κ → R)} (u : ι → Rˣ) (e : ι ≃ κ) (h : Submodule.map (↑(monomialEquiv u e)) C = D) : ↥C ≃ₗ[R] ↥D

A monomial transformation that maps one code onto another restricts to a linear equivalence between their codewords.

@[simp]

theorem TauCeti.coe_monomialCodeEquiv_apply {R : Type u_1} {ι : Type u_2} {κ : Type u_3} [CommSemiring R] {C : Submodule R (ι → R)} {D : Submodule R (κ → R)} (u : ι → Rˣ) (e : ι ≃ κ) (h : Submodule.map (↑(monomialEquiv u e)) C = D) (x : ↥C) : ↑((monomialCodeEquiv u e h) x) = (monomialEquiv u e) ↑x

monomialCodeEquiv acts on codewords by the ambient monomial transformation.

@[simp]

theorem TauCeti.coe_monomialCodeEquiv_symm_apply {R : Type u_1} {ι : Type u_2} {κ : Type u_3} [CommSemiring R] {C : Submodule R (ι → R)} {D : Submodule R (κ → R)} (u : ι → Rˣ) (e : ι ≃ κ) (h : Submodule.map (↑(monomialEquiv u e)) C = D) (y : ↥D) : ↑((monomialCodeEquiv u e h).symm y) = (monomialEquiv u e).symm ↑y

The inverse of monomialCodeEquiv acts on codewords by the inverse monomial transformation.

theorem TauCeti.IsPermutationEquivalent.isMonomialEquivalent {R : Type u_1} {ι : Type u_2} {κ : Type u_3} [CommSemiring R] {C : Submodule R (ι → R)} {D : Submodule R (κ → R)} (h : IsPermutationEquivalent C D) : IsMonomialEquivalent C D

theorem TauCeti.IsMonomialEquivalent.refl {R : Type u_1} {ι : Type u_2} [CommSemiring R] (C : Submodule R (ι → R)) : IsMonomialEquivalent C C

theorem TauCeti.IsMonomialEquivalent.symm {R : Type u_1} {ι : Type u_2} {κ : Type u_3} [CommSemiring R] {C : Submodule R (ι → R)} {D : Submodule R (κ → R)} (h : IsMonomialEquivalent C D) : IsMonomialEquivalent D C

theorem TauCeti.IsMonomialEquivalent.trans {R : Type u_1} {ι : Type u_2} {κ : Type u_3} {μ : Type u_4} [CommSemiring R] {C : Submodule R (ι → R)} {D : Submodule R (κ → R)} {E : Submodule R (μ → R)} (h : IsMonomialEquivalent C D) (h' : IsMonomialEquivalent D E) : IsMonomialEquivalent C E

theorem TauCeti.IsMonomialEquivalent.exists_mem_hammingNorm_eq {R : Type u_3} {ι : Type u_1} {κ : Type u_2} [CommSemiring R] {C : Submodule R (ι → R)} {D : Submodule R (κ → R)} [Fintype ι] [Fintype κ] [DecidableEq R] (h : IsMonomialEquivalent C D) {y : κ → R} (hy : y ∈ D) : ∃ x ∈ C, hammingNorm x = hammingNorm y

A monomial equivalence matches every word of the target code with a word of the source code of the same Hamming weight.

theorem TauCeti.IsMonomialEquivalent.forall_dvd_hammingNorm_iff {R : Type u_3} {ι : Type u_1} {κ : Type u_2} [CommSemiring R] {C : Submodule R (ι → R)} {D : Submodule R (κ → R)} [Fintype ι] [Fintype κ] [DecidableEq R] (h : IsMonomialEquivalent C D) (k : ℕ) : (∀ x ∈ C, k ∣ hammingNorm x) ↔ ∀ y ∈ D, k ∣ hammingNorm y

Monomial equivalence preserves divisibility of all codeword weights.

theorem TauCeti.IsMonomialEquivalent.finrank_eq {R : Type u_1} {ι : Type u_2} {κ : Type u_3} [CommSemiring R] {C : Submodule R (ι → R)} {D : Submodule R (κ → R)} (h : IsMonomialEquivalent C D) : Module.finrank R ↥C = Module.finrank R ↥D

Monomially equivalent codes have the same dimension.

theorem TauCeti.IsMonomialEquivalent.card_eq {R : Type u_1} {ι : Type u_2} {κ : Type u_3} [CommSemiring R] {C : Submodule R (ι → R)} {D : Submodule R (κ → R)} (h : IsMonomialEquivalent C D) : Nat.card ↥C = Nat.card ↥D

Monomially equivalent codes have the same number of codewords.

theorem TauCeti.IsMonomialEquivalent.hammingMinDist_eq {R : Type u_3} {ι : Type u_1} {κ : Type u_2} [CommSemiring R] {C : Submodule R (ι → R)} {D : Submodule R (κ → R)} [Fintype ι] [Fintype κ] [DecidableEq R] (h : IsMonomialEquivalent C D) : (↑C).hammingMinDist = (↑D).hammingMinDist

Monomially equivalent codes have the same minimum distance.

The monomial group and the automorphism group of a code

theorem TauCeti.hammingNorm_apply_of_mem_monomialGroup {R : Type u_2} [CommSemiring R] {ι : Type u_1} [Fintype ι] [DecidableEq R] {f : (ι → R) ≃ₗ[R] ι → R} (hf : f ∈ monomialGroup R ι) (x : ι → R) : hammingNorm (f x) = hammingNorm x

A monomial-group element preserves Hamming weight.

theorem TauCeti.hammingDist_apply_of_mem_monomialGroup {R : Type u_2} [CommSemiring R] {ι : Type u_1} [Fintype ι] [DecidableEq R] {f : (ι → R) ≃ₗ[R] ι → R} (hf : f ∈ monomialGroup R ι) (x y : ι → R) : hammingDist (f x) (f y) = hammingDist x y

A monomial-group element preserves Hamming distance.

def TauCeti.monomialAut {R : Type u_1} {ι : Type u_2} [CommSemiring R] (C : Submodule R (ι → R)) : Subgroup ((ι → R) ≃ₗ[R] ι → R)

The monomial automorphism group of a linear code: the monomial transformations of its coordinate space that map the code onto itself.

@[simp]

theorem TauCeti.mem_monomialAut {R : Type u_1} {ι : Type u_2} [CommSemiring R] {C : Submodule R (ι → R)} {f : (ι → R) ≃ₗ[R] ι → R} : f ∈ monomialAut C ↔ f ∈ monomialGroup R ι ∧ Submodule.map (↑f) C = C

The monomial automorphism group of C consists exactly of the monomial transformations mapping C onto itself.

theorem TauCeti.monomialAut_le_monomialGroup {R : Type u_1} {ι : Type u_2} [CommSemiring R] {C : Submodule R (ι → R)} : monomialAut C ≤ monomialGroup R ι

theorem TauCeti.apply_mem_of_mem_monomialAut {R : Type u_1} {ι : Type u_2} [CommSemiring R] {C : Submodule R (ι → R)} {f : (ι → R) ≃ₗ[R] ι → R} (hf : f ∈ monomialAut C) {x : ι → R} (hx : x ∈ C) : f x ∈ C

@[instance_reducible]

instance TauCeti.instSMulMonomialAut {R : Type u_1} {ι : Type u_2} [CommSemiring R] {C : Submodule R (ι → R)} : SMul ↥(monomialAut C) ↥C

A monomial automorphism of a code permutes its codewords.

@[simp]

theorem TauCeti.coe_smul_monomialAut {R : Type u_1} {ι : Type u_2} [CommSemiring R] {C : Submodule R (ι → R)} (f : ↥(monomialAut C)) (c : ↥C) : ↑(f • c) = ↑f ↑c

@[instance_reducible]

instance TauCeti.instDistribMulActionMonomialAut {R : Type u_1} {ι : Type u_2} [CommSemiring R] {C : Submodule R (ι → R)} : DistribMulAction ↥(monomialAut C) ↥C

instance TauCeti.instSMulCommClassMonomialAut {R : Type u_1} {ι : Type u_2} [CommSemiring R] {C : Submodule R (ι → R)} : SMulCommClass R ↥(monomialAut C) ↥C

Monomial automorphisms act by R-linear maps, so their action on codewords commutes with the scalar action.

instance TauCeti.instSMulCommClassMonomialAut' {R : Type u_1} {ι : Type u_2} [CommSemiring R] {C : Submodule R (ι → R)} : SMulCommClass (↥(monomialAut C)) R ↥C

The converse orientation of TauCeti.instSMulCommClassMonomialAut: the monomial automorphism action on codewords commutes with the scalar action of R.

@[simp]

theorem TauCeti.hammingNorm_monomialAut_apply {R : Type u_2} {ι : Type u_1} [CommSemiring R] {C : Submodule R (ι → R)} [Fintype ι] [DecidableEq R] (f : ↥(monomialAut C)) (x : ι → R) : hammingNorm (↑f x) = hammingNorm x

A monomial automorphism of a code preserves Hamming weight.

@[simp]

theorem TauCeti.hammingDist_monomialAut_apply {R : Type u_2} {ι : Type u_1} [CommSemiring R] {C : Submodule R (ι → R)} [Fintype ι] [DecidableEq R] (f : ↥(monomialAut C)) (x y : ι → R) : hammingDist (↑f x) (↑f y) = hammingDist x y

A monomial automorphism of a code preserves Hamming distance.

The permutation group and the permutation automorphism group of a code

theorem TauCeti.hammingNorm_apply_of_mem_permutationGroup {R : Type u_2} [Semiring R] {ι : Type u_1} [Fintype ι] [DecidableEq R] {f : (ι → R) ≃ₗ[R] ι → R} (hf : f ∈ permutationGroup R ι) (x : ι → R) : hammingNorm (f x) = hammingNorm x

A permutation-group element preserves Hamming weight.

theorem TauCeti.hammingDist_apply_of_mem_permutationGroup {R : Type u_2} [Semiring R] {ι : Type u_1} [Fintype ι] [DecidableEq R] {f : (ι → R) ≃ₗ[R] ι → R} (hf : f ∈ permutationGroup R ι) (x y : ι → R) : hammingDist (f x) (f y) = hammingDist x y

A permutation-group element preserves Hamming distance.

def TauCeti.permutationAut {R : Type u_1} {ι : Type u_2} [Semiring R] (C : Submodule R (ι → R)) : Subgroup ((ι → R) ≃ₗ[R] ι → R)

The permutation automorphism group of a linear code: the coordinate permutations that map the code onto itself.

@[simp]

theorem TauCeti.mem_permutationAut {R : Type u_1} {ι : Type u_2} [Semiring R] {C : Submodule R (ι → R)} {f : (ι → R) ≃ₗ[R] ι → R} : f ∈ permutationAut C ↔ f ∈ permutationGroup R ι ∧ Submodule.map (↑f) C = C

The permutation automorphism group of C consists exactly of the coordinate permutations mapping C onto itself.

theorem TauCeti.permutationAut_le_permutationGroup {R : Type u_1} {ι : Type u_2} [Semiring R] {C : Submodule R (ι → R)} : permutationAut C ≤ permutationGroup R ι

theorem TauCeti.apply_mem_of_mem_permutationAut {R : Type u_1} {ι : Type u_2} [Semiring R] {C : Submodule R (ι → R)} {f : (ι → R) ≃ₗ[R] ι → R} (hf : f ∈ permutationAut C) {x : ι → R} (hx : x ∈ C) : f x ∈ C

@[instance_reducible]

instance TauCeti.instSMulPermutationAut {R : Type u_1} {ι : Type u_2} [Semiring R] {C : Submodule R (ι → R)} : SMul ↥(permutationAut C) ↥C

A permutation automorphism of a code permutes its codewords.

@[simp]

theorem TauCeti.coe_smul_permutationAut {R : Type u_1} {ι : Type u_2} [Semiring R] {C : Submodule R (ι → R)} (f : ↥(permutationAut C)) (c : ↥C) : ↑(f • c) = ↑f ↑c

@[instance_reducible]

instance TauCeti.instDistribMulActionPermutationAut {R : Type u_1} {ι : Type u_2} [Semiring R] {C : Submodule R (ι → R)} : DistribMulAction ↥(permutationAut C) ↥C

instance TauCeti.instSMulCommClassPermutationAut {R : Type u_1} {ι : Type u_2} [Semiring R] {C : Submodule R (ι → R)} : SMulCommClass R ↥(permutationAut C) ↥C

Permutation automorphisms act by R-linear maps, so their action on codewords commutes with the scalar action.

instance TauCeti.instSMulCommClassPermutationAut' {R : Type u_1} {ι : Type u_2} [Semiring R] {C : Submodule R (ι → R)} : SMulCommClass (↥(permutationAut C)) R ↥C

The converse orientation of TauCeti.instSMulCommClassPermutationAut: the permutation automorphism action on codewords commutes with the scalar action of R.

@[simp]

theorem TauCeti.hammingNorm_permutationAut_apply {R : Type u_2} {ι : Type u_1} [Semiring R] {C : Submodule R (ι → R)} [Fintype ι] [DecidableEq R] (f : ↥(permutationAut C)) (x : ι → R) : hammingNorm (↑f x) = hammingNorm x

A permutation automorphism of a code preserves Hamming weight.

@[simp]

theorem TauCeti.hammingDist_permutationAut_apply {R : Type u_2} {ι : Type u_1} [Semiring R] {C : Submodule R (ι → R)} [Fintype ι] [DecidableEq R] (f : ↥(permutationAut C)) (x y : ι → R) : hammingDist (↑f x) (↑f y) = hammingDist x y

A permutation automorphism of a code preserves Hamming distance.

Permutation transformations as monomial transformations

theorem TauCeti.permutationAut_le_monomialAut {R : Type u_1} {ι : Type u_2} [CommSemiring R] {C : Submodule R (ι → R)} : permutationAut C ≤ monomialAut C

A permutation automorphism of a code is a monomial automorphism of it.

Monomial transformations when one is the only unit

@[simp]

theorem TauCeti.isMonomialEquivalent_iff_isPermutationEquivalent {R : Type u_3} [CommSemiring R] [Subsingleton Rˣ] {ι : Type u_1} {κ : Type u_2} {C : Submodule R (ι → R)} {D : Submodule R (κ → R)} : IsMonomialEquivalent C D ↔ IsPermutationEquivalent C D

When one is the only unit, monomial equivalence is permutation equivalence.

@[simp]

theorem TauCeti.monomialAut_eq_permutationAut {R : Type u_2} [CommSemiring R] [Subsingleton Rˣ] {ι : Type u_1} (C : Submodule R (ι → R)) : monomialAut C = permutationAut C

When one is the only unit, the monomial and permutation automorphism groups of a code coincide.