Main purpose

This file is a preliminary file for the Isos in Rep, we build all the isomorphisms from representation level to avoid abusing defeq.

TODO (Edison) : refactor Rep into a two-field structure (bundled Representation) and rebuild all the Isos in Rep using the equivs in this file.

noncomputable def Representation.ofMulActionSubsingletonEquivTrivial (k : Type u) [Semiring k] (G : Type v) [Monoid G] (H : Type w) [Subsingleton H] [MulOneClass H] [MulAction G H] : (ofMulAction k G H).Equiv (trivial k G k)

If there exists G-action on a trivial monoid H then the induced representation on k[H] is equivalent to the trivial representation.

@[simp]

theorem Representation.ofMulActionSubsingletonEquivTrivial_apply {k : Type u} [Semiring k] {G : Type v} [Monoid G] (H : Type w) [Subsingleton H] [MulOneClass H] [MulAction G H] (f : H →₀ k) : (↑(ofMulActionSubsingletonEquivTrivial k G H)).toLinearMap f = f 1

@[simp]

theorem Representation.ofMulActionSubsingletonEquivTrivial_symm_apply {k : Type u} [Semiring k] {G : Type v} [Monoid G] (H : Type w) [Subsingleton H] [MulOneClass H] [MulAction G H] (r : k) : (↑(ofMulActionSubsingletonEquivTrivial k G H).symm).toLinearMap r = fun₀ | 1 => r

noncomputable def Representation.diagonalOneEquivLeftRegular (k : Type u) [Semiring k] (G : Type v) [Monoid G] : (diagonal k G 1).Equiv (leftRegular k G)

The equivalence of representations between (Fin 1 → G) →₀ k and G →₀ k.

@[simp]

theorem Representation.diagonalOneEquivLeftRegular_apply_single {k : Type u} [Semiring k] {G : Type v} [Monoid G] (f : Fin 1 → G) (r : k) : ((diagonalOneEquivLeftRegular k G) fun₀ | f => r) = fun₀ | f 0 => r

@[simp]

theorem Representation.diagonalOneEquivLeftRegular_symm_apply_single {k : Type u} [Semiring k] {G : Type v} [Monoid G] (g : G) (r : k) : ((diagonalOneEquivLeftRegular k G).symm fun₀ | g => r) = fun₀ | uniqueElim g => r

noncomputable def Representation.freeLift {G : Type v} [Monoid G] {V : Type v'} [AddCommMonoid V] {k : Type u} [CommSemiring k] [Module k V] (σ : Representation k G V) {α : Type w'} (f : α → V) : (free k G α).IntertwiningMap σ

Every f : α → V can induce an intertwining map between (α →₀ G →₀ k) and V.

@[simp]

theorem Representation.freeLift_toLinearMap {G : Type v} [Monoid G] {V : Type v'} [AddCommMonoid V] {k : Type u} [CommSemiring k] [Module k V] (σ : Representation k G V) {α : Type w'} (f : α → V) : (σ.freeLift f).toLinearMap = (Finsupp.linearCombination k fun (x : α × G) => (σ x.2) (f x.1)) ∘ₗ ↑(Finsupp.curryLinearEquiv k).symm

@[simp]

theorem Representation.freeLift_single_single {G : Type v} [Monoid G] {V : Type v'} [AddCommMonoid V] {k : Type u} [CommSemiring k] [Module k V] (σ : Representation k G V) {α : Type w'} (i : α) (g : G) (r : k) (f : α → V) : ((σ.freeLift f) fun₀ | i => fun₀ | g => r) = r • (σ g) (f i)

noncomputable def Representation.freeLiftLEquiv {G : Type v} [Monoid G] {V : Type v'} [AddCommMonoid V] {k : Type u} [CommSemiring k] [Module k V] (σ : Representation k G V) (α : Type w') : (free k G α).IntertwiningMap σ ≃ₗ[k] α → V

Equiv between the intertwining map module (α →₀ G →₀ k) → V and the function space α → V.

@[simp]

theorem Representation.freeLiftLEquiv_symm_apply {G : Type v} [Monoid G] {V : Type v'} [AddCommMonoid V] {k : Type u} [CommSemiring k] [Module k V] (σ : Representation k G V) (α : Type w') (f : α → V) : (σ.freeLiftLEquiv α).symm f = σ.freeLift f

@[simp]

theorem Representation.freeLiftLEquiv_apply {G : Type v} [Monoid G] {V : Type v'} [AddCommMonoid V] {k : Type u} [CommSemiring k] [Module k V] (σ : Representation k G V) (α : Type w') (f : (free k G α).IntertwiningMap σ) (i : α) : (σ.freeLiftLEquiv α) f i = f fun₀ | i => fun₀ | 1 => 1

noncomputable def Representation.finsuppTensorLeft {G : Type v} [Monoid G] {V : Type v'} [AddCommMonoid V] {W : Type w'} [AddCommMonoid W] {k : Type u} [CommSemiring k] [Module k V] [Module k W] (σ : Representation k G V) (ρ : Representation k G W) (α : Type w') [DecidableEq α] : ((σ.finsupp α).tprod ρ).Equiv ((σ.tprod ρ).finsupp α)

Equiv between representations induced by linear equiv between (α →₀ V) ⊗[k] W and α →₀ (V ⊗[k] W).

theorem Representation.finsuppTensorLeft_apply_tmul {G : Type v} [Monoid G] {V : Type v'} [AddCommMonoid V] {W : Type w'} [AddCommMonoid W] {k : Type u} [CommSemiring k] [Module k V] [Module k W] (σ : Representation k G V) (ρ : Representation k G W) {α : Type w'} [DecidableEq α] (f : α →₀ V) (w : W) : (σ.finsuppTensorLeft ρ α) (f ⊗ₜ[k] w) = f.sum fun (i : α) (v : V) => fun₀ | i => v ⊗ₜ[k] w

@[simp]

theorem Representation.finsuppTensorLeft_apply_tmul_apply {G : Type v} [Monoid G] {V : Type v'} [AddCommMonoid V] {W : Type w'} [AddCommMonoid W] {k : Type u} [CommSemiring k] [Module k V] [Module k W] (σ : Representation k G V) (ρ : Representation k G W) {α : Type w'} [DecidableEq α] (f : α →₀ V) (w : W) (i : α) : ((σ.finsuppTensorLeft ρ α) (f ⊗ₜ[k] w)) i = f i ⊗ₜ[k] w

@[simp]

theorem Representation.finsuppTensorLeft_symm_apply_single {G : Type v} [Monoid G] {V : Type v'} [AddCommMonoid V] {W : Type w'} [AddCommMonoid W] {k : Type u} [CommSemiring k] [Module k V] [Module k W] (σ : Representation k G V) (ρ : Representation k G W) {α : Type w'} [DecidableEq α] (i : α) (v : V) (w : W) : ((σ.finsuppTensorLeft ρ α).symm fun₀ | i => v ⊗ₜ[k] w) = (fun₀ | i => v) ⊗ₜ[k] w

noncomputable def Representation.finsuppTensorRight {G : Type v} [Monoid G] {V : Type v'} [AddCommMonoid V] {W : Type w'} [AddCommMonoid W] {k : Type u} [CommSemiring k] [Module k V] [Module k W] (σ : Representation k G V) (ρ : Representation k G W) (α : Type w') [DecidableEq α] : (σ.tprod (ρ.finsupp α)).Equiv ((σ.tprod ρ).finsupp α)

Equiv between representations induced by linear equiv between V ⊗[k] (α →₀ W) and α →₀ (V ⊗[k] W).

theorem Representation.finsuppTensorRight_apply_tmul {G : Type v} [Monoid G] {V : Type v'} [AddCommMonoid V] {W : Type w'} [AddCommMonoid W] {k : Type u} [CommSemiring k] [Module k V] [Module k W] (σ : Representation k G V) (ρ : Representation k G W) {α : Type w'} [DecidableEq α] (v : V) (f : α →₀ W) : (σ.finsuppTensorRight ρ α) (v ⊗ₜ[k] f) = f.sum fun (i : α) (w : W) => fun₀ | i => v ⊗ₜ[k] w

@[simp]

theorem Representation.finsuppTensorRight_apply_tmul_apply {G : Type v} [Monoid G] {V : Type v'} [AddCommMonoid V] {W : Type w'} [AddCommMonoid W] {k : Type u} [CommSemiring k] [Module k V] [Module k W] (σ : Representation k G V) (ρ : Representation k G W) {α : Type w'} [DecidableEq α] (v : V) (f : α →₀ W) (i : α) : ((σ.finsuppTensorRight ρ α) (v ⊗ₜ[k] f)) i = v ⊗ₜ[k] f i

@[simp]

theorem Representation.finsuppTensorRight_symm_apply_single {G : Type v} [Monoid G] {V : Type v'} [AddCommMonoid V] {W : Type w'} [AddCommMonoid W] {k : Type u} [CommSemiring k] [Module k V] [Module k W] (σ : Representation k G V) (ρ : Representation k G W) {α : Type w'} [DecidableEq α] (i : α) (v : V) (w : W) : ((σ.finsuppTensorRight ρ α).symm fun₀ | i => v ⊗ₜ[k] w) = v ⊗ₜ[k] fun₀ | i => w

noncomputable def Representation.leftRegularTensorTrivialIsoFree {G : Type v} [Monoid G] {k : Type u} [CommSemiring k] (α : Type w') : ((leftRegular k G).tprod (trivial k G (α →₀ k))).Equiv (free k G α)

Equiv between representations induced by linear equiv between (G →₀ k) ⊗[k] (α →₀ k) and α →₀ G →₀ k.

@[simp]

theorem Representation.leftRegularTensorTrivialIsoFree_apply_single_tmul_single {G : Type v} [Monoid G] {k : Type u} [CommSemiring k] {α : Type w'} (g : G) (i : α) (r s : k) : (leftRegularTensorTrivialIsoFree α) ((fun₀ | g => r) ⊗ₜ[k] fun₀ | i => s) = fun₀ | i => fun₀ | g => r * s

@[simp]

theorem Representation.leftRegularTensorTrivialIsoFree_symm_apply_single_single {G : Type v} [Monoid G] {k : Type u} [CommSemiring k] {α : Type w'} (i : α) (g : G) (r : k) : ((leftRegularTensorTrivialIsoFree α).symm fun₀ | i => fun₀ | g => r) = (fun₀ | g => 1) ⊗ₜ[k] fun₀ | i => r

noncomputable def Representation.leftRegularMapEquiv {G : Type v} [Monoid G] {V : Type v'} [AddCommMonoid V] {k : Type u} [CommSemiring k] [Module k V] (σ : Representation k G V) : (leftRegular k G).IntertwiningMap σ ≃ₗ[k] V

The linear equiv between the hom module k[G] ⟶ᵍ V and V itself.

@[simp]

theorem Representation.leftRegularMapEquiv_apply {G : Type v} [Monoid G] {V : Type v'} [AddCommMonoid V] {k : Type u} [CommSemiring k] [Module k V] (σ : Representation k G V) (f : (leftRegular k G).IntertwiningMap σ) : σ.leftRegularMapEquiv f = f fun₀ | 1 => 1

@[simp]

theorem Representation.leftRegularMapEquiv_symm_apply_toFun {G : Type v} [Monoid G] {V : Type v'} [AddCommMonoid V] {k : Type u} [CommSemiring k] [Module k V] (σ : Representation k G V) (v : V) (d : G →₀ k) : (σ.leftRegularMapEquiv.symm v) d = d.sum fun (i : G) (c : k) => c • (σ i) v

theorem Representation.leftRegularMapEquiv_symm_single {G : Type v} [Monoid G] {V : Type v'} [AddCommMonoid V] {k : Type u} [CommSemiring k] [Module k V] (σ : Representation k G V) (g : G) (v : V) : ((σ.leftRegularMapEquiv.symm v) fun₀ | g => 1) = (σ g) v