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.

Equations

• Representation.ofMulActionSubsingletonEquivTrivial k G H = Representation.Equiv.mk (Finsupp.LinearEquiv.finsuppUnique k k H) ⋯

@[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 = Finsupp.single 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.

Equations

• Representation.diagonalOneEquivLeftRegular k G = Representation.Equiv.mk (Finsupp.domLCongr (Equiv.funUnique (Fin 1) G)) ⋯

@[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) (Finsupp.single f r) = Finsupp.single (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 (Finsupp.single g r) = Finsupp.single (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.

Equations

• σ.freeLift f = { toLinearMap := (Finsupp.linearCombination k fun (x : α × G) => (σ x.2) (f x.1)) ∘ₗ ↑(Finsupp.curryLinearEquiv k).symm, isIntertwining' := ⋯ }

@[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) (Finsupp.single i (Finsupp.single 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 intertwing map module (α →₀ G →₀ k) → V and V.

Equations

• One or more equations did not get rendered due to their size.

@[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 (Finsupp.single i (Finsupp.single 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).

Equations

• σ.finsuppTensorLeft ρ α = Representation.Equiv.mk (TensorProduct.finsuppLeft k k V 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) => Finsupp.single 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 (Finsupp.single i (v ⊗ₜ[k] w)) = Finsupp.single 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).

Equations

• σ.finsuppTensorRight ρ α = Representation.Equiv.mk (TensorProduct.finsuppRight k k V 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) => Finsupp.single 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 (Finsupp.single i (v ⊗ₜ[k] w)) = v ⊗ₜ[k] Finsupp.single 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.

Equations

• One or more equations did not get rendered due to their size.

@[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 α) (Finsupp.single g r ⊗ₜ[k] Finsupp.single i s) = Finsupp.single i (Finsupp.single 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 (Finsupp.single i (Finsupp.single g r)) = Finsupp.single g 1 ⊗ₜ[k] Finsupp.single 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.

Equations

• One or more equations did not get rendered due to their size.

@[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.toLinearMap (Finsupp.single 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) (Finsupp.single g 1) = (σ g) v