Representations with a freely permuted basis

Let ρ be a representation of a monoid G with a basis b whose index set is identified with Σ _ : ι, G, so that every basis vector is b ⟨i, h⟩ for a label i and a group element h. If ρ g sends b ⟨i, h⟩ to b ⟨i, g * h⟩, then ρ is the free representation on ι: the generator single i (single h 1) of Representation.free k G ι corresponds to b ⟨i, h⟩.

Main definitions

• Representation.freeEquivOfBasis: a basis freely permuted by the action identifies the representation with the free representation on the labels.

noncomputable def Representation.freeEquivOfBasis {k : Type u_1} {G : Type u_2} {V : Type u_3} {ι : Type u_4} {X : Type u_5} [CommSemiring k] [Monoid G] [AddCommMonoid V] [Module k V] (ρ : Representation k G V) (b : Module.Basis X k V) (e : (_ : ι) × G ≃ X) (hb : ∀ (g h : G) (i : ι), (ρ g) (b (e ⟨i, h⟩)) = b (e ⟨i, g * h⟩)) : (free k G ι).Equiv ρ

A representation with a freely permuted basis is free. If the basis b of ρ is indexed, through e, by Σ _ : ι, G, and ρ g sends b (e ⟨i, h⟩) to b (e ⟨i, g * h⟩), then ρ is equivalent to the free representation on ι, the generator single i (single h 1) corresponding to b (e ⟨i, h⟩).

@[simp]

theorem Representation.freeEquivOfBasis_single {k : Type u_1} {G : Type u_2} {V : Type u_3} {ι : Type u_4} {X : Type u_5} [CommSemiring k] [Monoid G] [AddCommMonoid V] [Module k V] (ρ : Representation k G V) (b : Module.Basis X k V) (e : (_ : ι) × G ≃ X) (hb : ∀ (g h : G) (i : ι), (ρ g) (b (e ⟨i, h⟩)) = b (e ⟨i, g * h⟩)) (i : ι) (h : G) (r : k) : (ρ.freeEquivOfBasis b e hb) (Finsupp.single i (MonoidAlgebra.single h r)) = r • b (e ⟨i, h⟩)

The generator single i (single h r) of the free representation corresponds to r • b (e ⟨i, h⟩).

@[simp]

theorem Representation.freeEquivOfBasis_symm_basis {k : Type u_1} {G : Type u_2} {V : Type u_3} {ι : Type u_4} {X : Type u_5} [CommSemiring k] [Monoid G] [AddCommMonoid V] [Module k V] (ρ : Representation k G V) (b : Module.Basis X k V) (e : (_ : ι) × G ≃ X) (hb : ∀ (g h : G) (i : ι), (ρ g) (b (e ⟨i, h⟩)) = b (e ⟨i, g * h⟩)) (i : ι) (h : G) : (ρ.freeEquivOfBasis b e hb).symm (b (e ⟨i, h⟩)) = Finsupp.single i (MonoidAlgebra.single h 1)

The basis vector b (e ⟨i, h⟩) corresponds to the generator single i (single h 1) of the free representation.