Monomial linear equivalences of coordinate spaces

A monomial equivalence rescales coordinates by units and then relabels them along an equivalence of index types. These transformations form the monomial subgroup of the group of linear automorphisms. Coordinate permutations form a subgroup, equal to the monomial subgroup when the coefficient semiring has only one unit. The construction allows infinite coordinate sets; only the dot-product and matrix statements require finite coordinates.

The application, composition, inverse, support and matrix formulas provide the coordinate description used to compare monomial linear automorphisms with monomial matrices. In particular these subgroups make sense over small fields where the normalizer of the rational points of a diagonal torus need not be the monomial subgroup.

The code-specific invariants and automorphism groups are developed in TauCeti.InformationTheory.Coding.Equivalence.

References

• W. C. Huffman and V. Pless, Fundamentals of Error-Correcting Codes (2003), §1.6.
• N. Bourbaki, Lie Groups and Lie Algebras, Chapters 4--6, Chapter IV, §2, no. 2.

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

The monomial equivalence of coordinate spaces attached to a family of units u : ι → Rˣ and a relabelling e : ι ≃ κ of coordinates: it rescales the i-th coordinate by u i and places the result in the coordinate e i.

@[simp]

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

At a target coordinate, a monomial equivalence multiplies the corresponding source coordinate by its assigned unit.

theorem TauCeti.monomialEquiv_symm_apply {ι : Type u_1} {κ : Type u_2} {R : Type u_4} [CommSemiring R] (u : ι → Rˣ) (e : ι ≃ κ) (y : κ → R) (i : ι) : (monomialEquiv u e).symm y i = ↑(u i)⁻¹ * y (e i)

The inverse monomial equivalence reads the relabelled coordinate and multiplies it by the inverse of the source coordinate's unit.

@[simp]

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

With trivial scalars a monomial equivalence is a bare relabelling of coordinates.

@[simp]

theorem TauCeti.monomialEquiv_trans {ι : Type u_1} {κ : Type u_2} {μ : Type u_3} {R : Type u_4} [CommSemiring R] (u : ι → Rˣ) (e : ι ≃ κ) (v : κ → Rˣ) (f : κ ≃ μ) : monomialEquiv u e ≪≫ₗ monomialEquiv v f = monomialEquiv (fun (i : ι) => u i * v (e i)) (e.trans f)

Composing monomial equivalences multiplies their coordinate units after relabelling and composes their coordinate equivalences.

@[simp]

theorem TauCeti.monomialEquiv_symm {ι : Type u_1} {κ : Type u_2} {R : Type u_4} [CommSemiring R] (u : ι → Rˣ) (e : ι ≃ κ) : (monomialEquiv u e).symm = monomialEquiv (fun (j : κ) => (u (e.symm j))⁻¹) e.symm

Inverting a monomial equivalence inverts and relabels its coordinate units and inverts its coordinate equivalence.

@[simp]

theorem TauCeti.support_monomialEquiv {ι : Type u_1} {κ : Type u_2} {R : Type u_4} [CommSemiring R] (u : ι → Rˣ) (e : ι ≃ κ) (x : ι → R) : Function.support ((monomialEquiv u e) x) = ⇑e '' Function.support x

A monomial equivalence transports support along its coordinate equivalence.

theorem TauCeti.monomialEquiv_apply_eq_comp {ι : Type u_1} {κ : Type u_2} {R : Type u_4} [CommSemiring R] (u : ι → Rˣ) (e : ι ≃ κ) (x : ι → R) : (monomialEquiv u e) x = (fun (i : ι) => ↑(u i) * x i) ∘ ⇑e.symm

A monomial equivalence is coordinatewise rescaling followed by reindexing.

theorem TauCeti.dotProduct_monomialEquiv_iff {ι : Type u_1} {κ : Type u_2} {R : Type u_4} [CommSemiring R] [Fintype ι] [Fintype κ] (u : ι → Rˣ) (e : ι ≃ κ) : (∀ (x y : ι → R), (monomialEquiv u e) x ⬝ᵥ (monomialEquiv u e) y = x ⬝ᵥ y) ↔ ∀ (i : ι), ↑(u i) ^ 2 = 1

A monomial coordinate change preserves the standard dot product exactly when every coordinate multiplier has square one.

theorem TauCeti.toMatrix'_monomialEquiv {ι : Type u_1} {κ : Type u_2} {R : Type u_4} [CommSemiring R] [Fintype ι] [DecidableEq ι] [DecidableEq κ] (u : ι → Rˣ) (e : ι ≃ κ) (k : κ) (i : ι) : LinearMap.toMatrix' (↑(monomialEquiv u e)) k i = if e i = k then ↑(u i) else 0

The matrix of a monomial equivalence: its column i is u i times the standard basis vector of the coordinate e i.

def TauCeti.monomialGroup (R : Type u_5) (ι : Type u_6) [CommSemiring R] : Subgroup ((ι → R) ≃ₗ[R] ι → R)

The group of monomial transformations of the coordinate space ι → R, as a subgroup of its group of linear automorphisms.

@[simp]

theorem TauCeti.mem_monomialGroup {ι : Type u_1} {R : Type u_4} [CommSemiring R] {f : (ι → R) ≃ₗ[R] ι → R} : f ∈ monomialGroup R ι ↔ ∃ (u : ι → Rˣ) (e : Equiv.Perm ι), monomialEquiv u e = f

The monomial group consists exactly of the monomial transformations of ι → R.

theorem TauCeti.monomialEquiv_mem_monomialGroup {ι : Type u_1} {R : Type u_4} [CommSemiring R] (u : ι → Rˣ) (e : Equiv.Perm ι) : monomialEquiv u e ∈ monomialGroup R ι

A monomial equivalence induced by coordinate units and a coordinate permutation belongs to the monomial group.

def TauCeti.permutationGroup (R : Type u_5) (ι : Type u_6) [Semiring R] : Subgroup ((ι → R) ≃ₗ[R] ι → R)

The group of coordinate permutations of ι → R, as a subgroup of its group of linear automorphisms.

@[simp]

theorem TauCeti.mem_permutationGroup {ι : Type u_1} {R : Type u_4} [Semiring R] {f : (ι → R) ≃ₗ[R] ι → R} : f ∈ permutationGroup R ι ↔ ∃ (e : Equiv.Perm ι), LinearEquiv.funCongrLeft R R (Equiv.symm e) = f

The permutation group consists exactly of the coordinate relabellings of ι → R.

theorem TauCeti.funCongrLeft_mem_permutationGroup {ι : Type u_1} {R : Type u_4} [Semiring R] (e : Equiv.Perm ι) : LinearEquiv.funCongrLeft R R (Equiv.symm e) ∈ permutationGroup R ι

A coordinate relabelling belongs to the permutation group.

theorem TauCeti.permutationGroup_le_monomialGroup {ι : Type u_1} {R : Type u_4} [CommSemiring R] : permutationGroup R ι ≤ monomialGroup R ι

A coordinate permutation is the monomial transformation with all scalars equal to one.

@[simp]

theorem TauCeti.monomialEquiv_eq_funCongrLeft {ι : Type u_1} {κ : Type u_2} {R : Type u_4} [CommSemiring R] [Subsingleton Rˣ] (u : ι → Rˣ) (e : ι ≃ κ) : monomialEquiv u e = LinearEquiv.funCongrLeft R R e.symm

When one is the only unit, a monomial transformation is its underlying coordinate permutation.

@[simp]

theorem TauCeti.monomialGroup_eq_permutationGroup {ι : Type u_1} {R : Type u_4} [CommSemiring R] [Subsingleton Rˣ] : monomialGroup R ι = permutationGroup R ι

When one is the only unit, the monomial group is the coordinate-permutation group.