Intertwining maps

This file gives defines intertwining maps of representations (aka equivariant linear maps).

structure Representation.IsIntertwiningMap {A : Type u_1} {G : Type u_2} {V : Type u_3} {W : Type u_4} [Semiring A] [Monoid G] [AddCommMonoid V] [AddCommMonoid W] [Module A V] [Module A W] (ρ : Representation A G V) (σ : Representation A G W) (f : V →ₗ[A] W) : Prop

An unbundled version of IntertwiningMap.

• isIntertwining (g : G) (v : V) : f ((ρ g) v) = (σ g) (f v)

theorem Representation.isIntertwiningMap_iff {A : Type u_1} {G : Type u_2} {V : Type u_3} {W : Type u_4} [Semiring A] [Monoid G] [AddCommMonoid V] [AddCommMonoid W] [Module A V] [Module A W] (ρ : Representation A G V) (σ : Representation A G W) (f : V →ₗ[A] W) : ρ.IsIntertwiningMap σ f ↔ ∀ (g : G) (v : V), f ((ρ g) v) = (σ g) (f v)

structure Representation.IntertwiningMap {A : Type u_1} {G : Type u_2} {V : Type u_3} {W : Type u_4} [Semiring A] [Monoid G] [AddCommMonoid V] [AddCommMonoid W] [Module A V] [Module A W] (ρ : Representation A G V) (σ : Representation A G W) extends V →ₗ[A] W : Type (max u_3 u_4)

An intertwining map between two representations ρ and σ of the same monoid G is a map between underlying modules which commutes with the G-actions.

• toFun : V → W
• map_add' (x y : V) : self.toFun (x + y) = self.toFun x + self.toFun y
• map_smul' (m : A) (x : V) : self.toFun (m • x) = (RingHom.id A) m • self.toFun x
• isIntertwining' (g : G) : self.toLinearMap ∘ₗ ρ g = σ g ∘ₗ self.toLinearMap

  An underlying A-linear map of the underlying A-modules.

def LinearMap.intertwiningMap_of_isIntertwiningMap {A : Type u_1} {G : Type u_2} {V : Type u_3} {W : Type u_4} [Semiring A] [Monoid G] [AddCommMonoid V] [AddCommMonoid W] [Module A V] [Module A W] (ρ : Representation A G V) (σ : Representation A G W) (f : V →ₗ[A] W) (hf : ∀ (g : G) (v : V), f ((ρ g) v) = (σ g) (f v)) : ρ.IntertwiningMap σ

An intertwining map constructed form the linear map and the fact that it is intertwining.

Equations

• LinearMap.intertwiningMap_of_isIntertwiningMap ρ σ f hf = { toLinearMap := f, isIntertwining' := ⋯ }

theorem Representation.IntertwiningMap.isIntertwining_assoc {A : Type u_1} {G : Type u_2} {V : Type u_3} {W : Type u_4} {U : Type u_5} [Semiring A] [Monoid G] [AddCommMonoid V] [AddCommMonoid W] [AddCommMonoid U] [Module A V] [Module A W] [Module A U] (ρ : Representation A G V) (σ : Representation A G W) {f : ρ.IntertwiningMap σ} (g : G) (l : U →ₗ[A] V) : f.toLinearMap ∘ₗ ρ g ∘ₗ l = σ g ∘ₗ f.toLinearMap ∘ₗ l

theorem Representation.IntertwiningMap.ext {A : Type u_1} {G : Type u_2} {V : Type u_3} {W : Type u_4} [Semiring A] [Monoid G] [AddCommMonoid V] [AddCommMonoid W] [Module A V] [Module A W] {ρ : Representation A G V} {σ : Representation A G W} {f g : ρ.IntertwiningMap σ} (h : f.toLinearMap = g.toLinearMap) : f = g

theorem Representation.IntertwiningMap.ext_iff {A : Type u_1} {G : Type u_2} {V : Type u_3} {W : Type u_4} [Semiring A] [Monoid G] [AddCommMonoid V] [AddCommMonoid W] [Module A V] [Module A W] {ρ : Representation A G V} {σ : Representation A G W} {f g : ρ.IntertwiningMap σ} : f = g ↔ f.toLinearMap = g.toLinearMap

theorem Representation.IntertwiningMap.toLinearMap_injective {A : Type u_1} {G : Type u_2} {V : Type u_3} {W : Type u_4} [Semiring A] [Monoid G] [AddCommMonoid V] [AddCommMonoid W] [Module A V] [Module A W] (ρ : Representation A G V) (σ : Representation A G W) : Function.Injective fun (f : ρ.IntertwiningMap σ) => f.toLinearMap

theorem Representation.IntertwiningMap.toFun_injective {A : Type u_1} {G : Type u_2} {V : Type u_3} {W : Type u_4} [Semiring A] [Monoid G] [AddCommMonoid V] [AddCommMonoid W] [Module A V] [Module A W] (ρ : Representation A G V) (σ : Representation A G W) : Function.Injective fun (f : ρ.IntertwiningMap σ) => f.toFun

@[implicit_reducible]

instance Representation.IntertwiningMap.instFunLike {A : Type u_1} {G : Type u_2} {V : Type u_3} {W : Type u_4} [Semiring A] [Monoid G] [AddCommMonoid V] [AddCommMonoid W] [Module A V] [Module A W] (ρ : Representation A G V) (σ : Representation A G W) : FunLike (ρ.IntertwiningMap σ) V W

Equations

• Representation.IntertwiningMap.instFunLike ρ σ = { coe := fun (f : ρ.IntertwiningMap σ) => f.toFun, coe_injective' := ⋯ }

instance Representation.IntertwiningMap.instLinearMapClass {A : Type u_1} {G : Type u_2} {V : Type u_3} {W : Type u_4} [Semiring A] [Monoid G] [AddCommMonoid V] [AddCommMonoid W] [Module A V] [Module A W] (ρ : Representation A G V) (σ : Representation A G W) : LinearMapClass (ρ.IntertwiningMap σ) A V W

@[simp]

theorem Representation.IntertwiningMap.coe_mk {A : Type u_1} {G : Type u_2} {V : Type u_3} {W : Type u_4} [Semiring A] [Monoid G] [AddCommMonoid V] [AddCommMonoid W] [Module A V] [Module A W] (ρ : Representation A G V) (σ : Representation A G W) (f : V →ₗ[A] W) (h : ∀ (g : G), f ∘ₗ ρ g = σ g ∘ₗ f) : ⇑{ toLinearMap := f, isIntertwining' := h } = ⇑f

theorem Representation.IntertwiningMap.toLinearMap_mk {A : Type u_1} {G : Type u_2} {V : Type u_3} {W : Type u_4} [Semiring A] [Monoid G] [AddCommMonoid V] [AddCommMonoid W] [Module A V] [Module A W] (ρ : Representation A G V) (σ : Representation A G W) (f : V →ₗ[A] W) (h : ∀ (g : G), f ∘ₗ ρ g = σ g ∘ₗ f) : { toLinearMap := f, isIntertwining' := h }.toLinearMap = f

theorem Representation.IntertwiningMap.isIntertwining {A : Type u_1} {G : Type u_2} {V : Type u_3} {W : Type u_4} [Semiring A] [Monoid G] [AddCommMonoid V] [AddCommMonoid W] [Module A V] [Module A W] (ρ : Representation A G V) (σ : Representation A G W) (f : ρ.IntertwiningMap σ) (g : G) (v : V) : f.toLinearMap ((ρ g) v) = (σ g) (f.toLinearMap v)

theorem Representation.IntertwiningMap.toLinearMap_apply {A : Type u_1} {G : Type u_2} {V : Type u_3} {W : Type u_4} [Semiring A] [Monoid G] [AddCommMonoid V] [AddCommMonoid W] [Module A V] [Module A W] (ρ : Representation A G V) (σ : Representation A G W) (f : ρ.IntertwiningMap σ) (v : V) : f.toLinearMap v = f v

@[simp]

theorem LinearMap.toIntertwiningMap {A : Type u_1} {G : Type u_2} {V : Type u_3} {W : Type u_4} [Semiring A] [Monoid G] [AddCommMonoid V] [AddCommMonoid W] [Module A V] [Module A W] (ρ : Representation A G V) (σ : Representation A G W) (f : V →ₗ[A] W) (hf : ∀ (g : G) (v : V), f ((ρ g) v) = (σ g) (f v)) (v : V) : (intertwiningMap_of_isIntertwiningMap ρ σ f hf) v = f v

@[implicit_reducible]

instance Representation.IntertwiningMap.instZero {A : Type u_1} {G : Type u_2} {V : Type u_3} {W : Type u_4} [Semiring A] [Monoid G] [AddCommMonoid V] [AddCommMonoid W] [Module A V] [Module A W] (ρ : Representation A G V) (σ : Representation A G W) : Zero (ρ.IntertwiningMap σ)

Equations

• Representation.IntertwiningMap.instZero ρ σ = { zero := { toLinearMap := 0, isIntertwining' := ⋯ } }

@[simp]

theorem Representation.IntertwiningMap.coe_zero {A : Type u_1} {G : Type u_2} {V : Type u_3} {W : Type u_4} [Semiring A] [Monoid G] [AddCommMonoid V] [AddCommMonoid W] [Module A V] [Module A W] (ρ : Representation A G V) (σ : Representation A G W) : ⇑0 = 0

@[simp]

theorem Representation.IntertwiningMap.zero_toLinearMap {A : Type u_1} {G : Type u_2} {V : Type u_3} {W : Type u_4} [Semiring A] [Monoid G] [AddCommMonoid V] [AddCommMonoid W] [Module A V] [Module A W] (ρ : Representation A G V) (σ : Representation A G W) : toLinearMap 0 = 0

@[implicit_reducible]

instance Representation.IntertwiningMap.instAdd {A : Type u_1} {G : Type u_2} {V : Type u_3} {W : Type u_4} [Semiring A] [Monoid G] [AddCommMonoid V] [AddCommMonoid W] [Module A V] [Module A W] (ρ : Representation A G V) (σ : Representation A G W) : Add (ρ.IntertwiningMap σ)

Equations

• Representation.IntertwiningMap.instAdd ρ σ = { add := fun (f g : ρ.IntertwiningMap σ) => { toLinearMap := f.toLinearMap + g.toLinearMap, isIntertwining' := ⋯ } }

@[simp]

theorem Representation.IntertwiningMap.coe_add {A : Type u_1} {G : Type u_2} {V : Type u_3} {W : Type u_4} [Semiring A] [Monoid G] [AddCommMonoid V] [AddCommMonoid W] [Module A V] [Module A W] (ρ : Representation A G V) (σ : Representation A G W) (f g : ρ.IntertwiningMap σ) : ⇑(f + g) = ⇑f + ⇑g

@[simp]

theorem Representation.IntertwiningMap.add_toLinearMap {A : Type u_1} {G : Type u_2} {V : Type u_3} {W : Type u_4} [Semiring A] [Monoid G] [AddCommMonoid V] [AddCommMonoid W] [Module A V] [Module A W] (ρ : Representation A G V) (σ : Representation A G W) (f g : ρ.IntertwiningMap σ) : (f + g).toLinearMap = f.toLinearMap + g.toLinearMap

@[implicit_reducible]

instance Representation.IntertwiningMap.instSMulNat {A : Type u_1} {G : Type u_2} {V : Type u_3} {W : Type u_4} [Semiring A] [Monoid G] [AddCommMonoid V] [AddCommMonoid W] [Module A V] [Module A W] (ρ : Representation A G V) (σ : Representation A G W) : SMul ℕ (ρ.IntertwiningMap σ)

Equations

• Representation.IntertwiningMap.instSMulNat ρ σ = { smul := fun (n : ℕ) (f : ρ.IntertwiningMap σ) => { toLinearMap := n • f.toLinearMap, isIntertwining' := ⋯ } }

@[simp]

theorem Representation.IntertwiningMap.coe_nsmul {A : Type u_1} {G : Type u_2} {V : Type u_3} {W : Type u_4} [Semiring A] [Monoid G] [AddCommMonoid V] [AddCommMonoid W] [Module A V] [Module A W] (ρ : Representation A G V) (σ : Representation A G W) (f : ρ.IntertwiningMap σ) (n : ℕ) : ⇑(n • f) = n • ⇑f

@[implicit_reducible]

instance Representation.IntertwiningMap.instAddCommMonoid {A : Type u_1} {G : Type u_2} {V : Type u_3} {W : Type u_4} [Semiring A] [Monoid G] [AddCommMonoid V] [AddCommMonoid W] [Module A V] [Module A W] (ρ : Representation A G V) (σ : Representation A G W) : AddCommMonoid (ρ.IntertwiningMap σ)

Equations

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

@[implicit_reducible]

instance Representation.IntertwiningMap.instNeg {A : Type u_1} {G : Type u_2} [Semiring A] [Monoid G] {V : Type u_6} {W : Type u_7} [AddCommMonoid V] [AddCommGroup W] [Module A V] [Module A W] (ρ : Representation A G V) (σ : Representation A G W) : Neg (ρ.IntertwiningMap σ)

Equations

• Representation.IntertwiningMap.instNeg ρ σ = { neg := fun (f : ρ.IntertwiningMap σ) => { toLinearMap := -f.toLinearMap, isIntertwining' := ⋯ } }

@[simp]

theorem Representation.IntertwiningMap.coe_neg {A : Type u_1} {G : Type u_2} [Semiring A] [Monoid G] {V : Type u_6} {W : Type u_7} [AddCommMonoid V] [AddCommGroup W] [Module A V] [Module A W] (ρ : Representation A G V) (σ : Representation A G W) (f : ρ.IntertwiningMap σ) : ⇑(-f) = -⇑f

@[implicit_reducible]

instance Representation.IntertwiningMap.instSub {A : Type u_1} {G : Type u_2} [Semiring A] [Monoid G] {V : Type u_6} {W : Type u_7} [AddCommMonoid V] [AddCommGroup W] [Module A V] [Module A W] (ρ : Representation A G V) (σ : Representation A G W) : Sub (ρ.IntertwiningMap σ)

Equations

• Representation.IntertwiningMap.instSub ρ σ = { sub := fun (f g : ρ.IntertwiningMap σ) => { toLinearMap := f.toLinearMap - g.toLinearMap, isIntertwining' := ⋯ } }

@[simp]

theorem Representation.IntertwiningMap.coe_sub {A : Type u_1} {G : Type u_2} [Semiring A] [Monoid G] {V : Type u_6} {W : Type u_7} [AddCommMonoid V] [AddCommGroup W] [Module A V] [Module A W] (ρ : Representation A G V) (σ : Representation A G W) (f g : ρ.IntertwiningMap σ) : ⇑(f - g) = ⇑f - ⇑g

@[simp]

theorem Representation.IntertwiningMap.sub_toLinearMap {A : Type u_1} {G : Type u_2} [Semiring A] [Monoid G] {V : Type u_6} {W : Type u_7} [AddCommMonoid V] [AddCommGroup W] [Module A V] [Module A W] (ρ : Representation A G V) (σ : Representation A G W) (f g : ρ.IntertwiningMap σ) : (f - g).toLinearMap = f.toLinearMap - g.toLinearMap

@[implicit_reducible]

instance Representation.IntertwiningMap.instSMulInt {A : Type u_1} {G : Type u_2} [Semiring A] [Monoid G] {V : Type u_6} {W : Type u_7} [AddCommMonoid V] [AddCommGroup W] [Module A V] [Module A W] (ρ : Representation A G V) (σ : Representation A G W) : SMul ℤ (ρ.IntertwiningMap σ)

Equations

• Representation.IntertwiningMap.instSMulInt ρ σ = { smul := fun (z : ℤ) (f : ρ.IntertwiningMap σ) => { toLinearMap := z • f.toLinearMap, isIntertwining' := ⋯ } }

@[simp]

theorem Representation.IntertwiningMap.coe_zsmul {A : Type u_1} {G : Type u_2} [Semiring A] [Monoid G] {V : Type u_6} {W : Type u_7} [AddCommMonoid V] [AddCommGroup W] [Module A V] [Module A W] (ρ : Representation A G V) (σ : Representation A G W) (f : ρ.IntertwiningMap σ) (z : ℤ) : ⇑(z • f) = z • ⇑f

@[implicit_reducible]

instance Representation.IntertwiningMap.instAddCommGroup {A : Type u_1} {G : Type u_2} [Semiring A] [Monoid G] {V : Type u_6} {W : Type u_7} [AddCommMonoid V] [AddCommGroup W] [Module A V] [Module A W] (ρ : Representation A G V) (σ : Representation A G W) : AddCommGroup (ρ.IntertwiningMap σ)

Equations

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

def Representation.IntertwiningMap.coeFnAddMonoidHom {A : Type u_1} {G : Type u_2} {V : Type u_3} {W : Type u_4} [Semiring A] [Monoid G] [AddCommMonoid V] [AddCommMonoid W] [Module A V] [Module A W] (ρ : Representation A G V) (σ : Representation A G W) : ρ.IntertwiningMap σ →+ V → W

A coercion from intertwining maps to additive monoid homomorphisms.

Equations

• Representation.IntertwiningMap.coeFnAddMonoidHom ρ σ = { toFun := DFunLike.coe, map_zero' := ⋯, map_add' := ⋯ }

def Representation.IntertwiningMap.id {A : Type u_1} {G : Type u_2} {V : Type u_3} [Semiring A] [Monoid G] [AddCommMonoid V] [Module A V] (ρ : Representation A G V) : ρ.IntertwiningMap ρ

The identity map, considered as an intertwining map from a representation to itself.

Equations

• Representation.IntertwiningMap.id ρ = { toLinearMap := LinearMap.id, isIntertwining' := ⋯ }

@[simp]

theorem Representation.IntertwiningMap.toLinearMap_id {A : Type u_1} {G : Type u_2} {V : Type u_3} [Semiring A] [Monoid G] [AddCommMonoid V] [Module A V] (ρ : Representation A G V) : (id ρ).toLinearMap = LinearMap.id

@[simp]

theorem Representation.IntertwiningMap.id_apply {A : Type u_1} {G : Type u_2} {V : Type u_3} [Semiring A] [Monoid G] [AddCommMonoid V] [Module A V] (ρ : Representation A G V) (v : V) : (id ρ) v = v

def Representation.IntertwiningMap.comp {A : Type u_1} {G : Type u_2} {V : Type u_3} {W : Type u_4} {U : Type u_5} [Semiring A] [Monoid G] [AddCommMonoid V] [AddCommMonoid W] [AddCommMonoid U] [Module A V] [Module A W] [Module A U] {ρ : Representation A G V} {σ : Representation A G W} {τ : Representation A G U} (f : σ.IntertwiningMap τ) (g : ρ.IntertwiningMap σ) : ρ.IntertwiningMap τ

Composition of intertwining maps.

A convenience variant of IntertwiningMap.llcomp for use in dot notation.

Equations

• f.comp g = { toLinearMap := f.toLinearMap ∘ₗ g.toLinearMap, isIntertwining' := ⋯ }

@[simp]

theorem Representation.IntertwiningMap.comp_toLinearMap {A : Type u_1} {G : Type u_2} {V : Type u_3} {W : Type u_4} {U : Type u_5} [Semiring A] [Monoid G] [AddCommMonoid V] [AddCommMonoid W] [AddCommMonoid U] [Module A V] [Module A W] [Module A U] (ρ : Representation A G V) (σ : Representation A G W) (τ : Representation A G U) (f : σ.IntertwiningMap τ) (g : ρ.IntertwiningMap σ) : (f.comp g).toLinearMap = f.toLinearMap ∘ₗ g.toLinearMap

@[simp]

theorem Representation.IntertwiningMap.comp_apply {A : Type u_1} {G : Type u_2} {V : Type u_3} {W : Type u_4} {U : Type u_5} [Semiring A] [Monoid G] [AddCommMonoid V] [AddCommMonoid W] [AddCommMonoid U] [Module A V] [Module A W] [Module A U] (ρ : Representation A G V) (σ : Representation A G W) (τ : Representation A G U) (f : σ.IntertwiningMap τ) (g : ρ.IntertwiningMap σ) (v : V) : (f.comp g) v = f (g v)

theorem Representation.IntertwiningMap.comp_add {A : Type u_1} {G : Type u_2} {V : Type u_3} {W : Type u_4} {U : Type u_5} [Semiring A] [Monoid G] [AddCommMonoid V] [AddCommMonoid W] [AddCommMonoid U] [Module A V] [Module A W] [Module A U] (ρ : Representation A G V) (σ : Representation A G W) (τ : Representation A G U) (f₁ f₂ : σ.IntertwiningMap τ) (g : ρ.IntertwiningMap σ) : (f₁ + f₂).comp g = f₁.comp g + f₂.comp g

theorem Representation.IntertwiningMap.add_comp {A : Type u_1} {G : Type u_2} {V : Type u_3} {W : Type u_4} {U : Type u_5} [Semiring A] [Monoid G] [AddCommMonoid V] [AddCommMonoid W] [AddCommMonoid U] [Module A V] [Module A W] [Module A U] (ρ : Representation A G V) (σ : Representation A G W) (τ : Representation A G U) (f : σ.IntertwiningMap τ) (g₁ g₂ : ρ.IntertwiningMap σ) : f.comp (g₁ + g₂) = f.comp g₁ + f.comp g₂

structure Representation.Equiv {A : Type u_1} {G : Type u_2} {V : Type u_3} {W : Type u_4} [Semiring A] [Monoid G] [AddCommMonoid V] [AddCommMonoid W] [Module A V] [Module A W] (ρ : Representation A G V) (σ : Representation A G W) extends ρ.IntertwiningMap σ, V ≃ₗ[A] W : Type (max u_3 u_4)

Equivalence between representations is a bijective intertwining map.

• mk' :: (
• toFun : V → W
• map_add' (x y : V) : (↑self).toFun (x + y) = (↑self).toFun x + (↑self).toFun y
• map_smul' (m : A) (x : V) : (↑self).toFun (m • x) = (RingHom.id A) m • (↑self).toFun x
• isIntertwining' (g : G) : (↑self).toLinearMap ∘ₗ ρ g = σ g ∘ₗ (↑self).toLinearMap
• invFun : W → V
• left_inv : Function.LeftInverse self.invFun (↑self).toFun
• right_inv : Function.RightInverse self.invFun (↑self).toFun
• )

def Representation.Equiv.mk {A : Type u_1} {G : Type u_2} {V : Type u_3} {W : Type u_4} [Semiring A] [Monoid G] [AddCommMonoid V] [AddCommMonoid W] [Module A V] [Module A W] {ρ : Representation A G V} {σ : Representation A G W} (e : V ≃ₗ[A] W) (he : ∀ (g : G), ↑e ∘ₗ ρ g = σ g ∘ₗ ↑e) : ρ.Equiv σ

An Equiv between representations could be built from a LinearEquiv and an assumption proving the G-equivariance.

Equations

• Representation.Equiv.mk e he = { toLinearMap := ↑e, isIntertwining' := he, invFun := e.invFun, left_inv := ⋯, right_inv := ⋯ }

theorem Representation.Equiv.toLinearEquiv_mk' {A : Type u_1} {G : Type u_2} {V : Type u_3} {W : Type u_4} [Semiring A] [Monoid G] [AddCommMonoid V] [AddCommMonoid W] [Module A V] [Module A W] {ρ : Representation A G V} {σ : Representation A G W} {e : V ≃ₗ[A] W} (he : ∀ (g : G), ↑e ∘ₗ ρ g = σ g ∘ₗ ↑e) : (mk e he).toLinearEquiv = e

theorem Representation.Equiv.toIntertwiningMap_mk' {A : Type u_1} {G : Type u_2} {V : Type u_3} {W : Type u_4} [Semiring A] [Monoid G] [AddCommMonoid V] [AddCommMonoid W] [Module A V] [Module A W] {ρ : Representation A G V} {σ : Representation A G W} (e : V ≃ₗ[A] W) (he : ∀ (g : G), ↑e ∘ₗ ρ g = σ g ∘ₗ ↑e) : ↑(mk e he) = { toLinearMap := ↑e, isIntertwining' := he }

@[simp]

theorem Representation.Equiv.toLinearMap_mk' {A : Type u_1} {G : Type u_2} {V : Type u_3} {W : Type u_4} [Semiring A] [Monoid G] [AddCommMonoid V] [AddCommMonoid W] [Module A V] [Module A W] {ρ : Representation A G V} {σ : Representation A G W} (e : V ≃ₗ[A] W) (he : ∀ (g : G), ↑e ∘ₗ ρ g = σ g ∘ₗ ↑e) : (↑(mk e he)).toLinearMap = ↑e

theorem Representation.Equiv.toLinearEquiv_injective {A : Type u_1} {G : Type u_2} {V : Type u_3} {W : Type u_4} [Semiring A] [Monoid G] [AddCommMonoid V] [AddCommMonoid W] [Module A V] [Module A W] {ρ : Representation A G V} {σ : Representation A G W} : Function.Injective toLinearEquiv

theorem Representation.Equiv.toLinearEquiv_inj {A : Type u_1} {G : Type u_2} {V : Type u_3} {W : Type u_4} [Semiring A] [Monoid G] [AddCommMonoid V] [AddCommMonoid W] [Module A V] [Module A W] {ρ : Representation A G V} {σ : Representation A G W} (φ ψ : σ.Equiv ρ) : φ.toLinearEquiv = ψ.toLinearEquiv ↔ φ = ψ

@[implicit_reducible]

instance Representation.Equiv.instEquivLike {A : Type u_1} {G : Type u_2} {V : Type u_3} {W : Type u_4} [Semiring A] [Monoid G] [AddCommMonoid V] [AddCommMonoid W] [Module A V] [Module A W] {ρ : Representation A G V} {σ : Representation A G W} : EquivLike (ρ.Equiv σ) V W

Equations

• Representation.Equiv.instEquivLike = { coe := fun (φ : ρ.Equiv σ) => ⇑φ.toLinearEquiv, inv := fun (φ : ρ.Equiv σ) => φ.invFun, left_inv := ⋯, right_inv := ⋯, coe_injective' := ⋯ }

instance Representation.Equiv.instLinearEquivClass {A : Type u_1} {G : Type u_2} {V : Type u_3} {W : Type u_4} [Semiring A] [Monoid G] [AddCommMonoid V] [AddCommMonoid W] [Module A V] [Module A W] {ρ : Representation A G V} {σ : Representation A G W} : LinearEquivClass (σ.Equiv ρ) A W V

@[simp]

theorem Representation.Equiv.mk_apply {A : Type u_1} {G : Type u_2} {V : Type u_3} {W : Type u_4} [Semiring A] [Monoid G] [AddCommMonoid V] [AddCommMonoid W] [Module A V] [Module A W] {ρ : Representation A G V} {σ : Representation A G W} {e : V ≃ₗ[A] W} (he : ∀ (g : G), ↑e ∘ₗ ρ g = σ g ∘ₗ ↑e) (v : V) : (mk e he) v = e v

theorem Representation.Equiv.ext {A : Type u_1} {G : Type u_2} {V : Type u_3} {W : Type u_4} [Semiring A] [Monoid G] [AddCommMonoid V] [AddCommMonoid W] [Module A V] [Module A W] {ρ : Representation A G V} {σ : Representation A G W} {φ ψ : ρ.Equiv σ} (h : ⇑φ = ⇑ψ) : φ = ψ

theorem Representation.Equiv.ext_iff {A : Type u_1} {G : Type u_2} {V : Type u_3} {W : Type u_4} [Semiring A] [Monoid G] [AddCommMonoid V] [AddCommMonoid W] [Module A V] [Module A W] {ρ : Representation A G V} {σ : Representation A G W} {φ ψ : ρ.Equiv σ} : φ = ψ ↔ ⇑φ = ⇑ψ

def Representation.Equiv.refl {A : Type u_1} {G : Type u_2} {V : Type u_3} [Semiring A] [Monoid G] [AddCommMonoid V] [Module A V] (ρ : Representation A G V) : ρ.Equiv ρ

Any representation is equivalent to itself.

Equations

• Representation.Equiv.refl ρ = { toLinearMap := ↑(LinearEquiv.refl A V), isIntertwining' := ⋯, invFun := (LinearEquiv.refl A V).invFun, left_inv := ⋯, right_inv := ⋯ }

@[simp]

theorem Representation.Equiv.toIntertwiningMap_refl {A : Type u_1} {G : Type u_2} {V : Type u_3} [Semiring A] [Monoid G] [AddCommMonoid V] [Module A V] {ρ : Representation A G V} : ↑(refl ρ) = IntertwiningMap.id ρ

@[simp]

theorem Representation.Equiv.toLinearMap_refl {A : Type u_1} {G : Type u_2} {V : Type u_3} [Semiring A] [Monoid G] [AddCommMonoid V] [Module A V] {ρ : Representation A G V} : (↑(refl ρ)).toLinearMap = LinearMap.id

@[simp]

theorem Representation.Equiv.refl_apply {A : Type u_1} {G : Type u_2} {V : Type u_3} [Semiring A] [Monoid G] [AddCommMonoid V] [Module A V] {ρ : Representation A G V} (v : V) : (refl ρ) v = v

@[simp]

theorem Representation.Equiv.coe_toIntertwiningMap {A : Type u_1} {G : Type u_2} {V : Type u_3} {W : Type u_4} [Semiring A] [Monoid G] [AddCommMonoid V] [AddCommMonoid W] [Module A V] [Module A W] {ρ : Representation A G V} {σ : Representation A G W} (φ : ρ.Equiv σ) : ⇑↑φ = ⇑φ

@[simp]

theorem Representation.Equiv.coe_toLinearMap {A : Type u_1} {G : Type u_2} {V : Type u_3} {W : Type u_4} [Semiring A] [Monoid G] [AddCommMonoid V] [AddCommMonoid W] [Module A V] [Module A W] {ρ : Representation A G V} {σ : Representation A G W} (φ : ρ.Equiv σ) : ⇑(↑φ).toLinearMap = ⇑φ

theorem Representation.Equiv.coe_invFun {A : Type u_1} {G : Type u_2} {V : Type u_3} {W : Type u_4} [Semiring A] [Monoid G] [AddCommMonoid V] [AddCommMonoid W] [Module A V] [Module A W] {ρ : Representation A G V} {σ : Representation A G W} (φ : ρ.Equiv σ) : φ.invFun = ⇑φ.toLinearEquiv.symm

theorem Representation.Equiv.toLinearEquiv_toLinearMap {A : Type u_1} {G : Type u_2} {V : Type u_3} {W : Type u_4} [Semiring A] [Monoid G] [AddCommMonoid V] [AddCommMonoid W] [Module A V] [Module A W] {ρ : Representation A G V} {σ : Representation A G W} (φ : ρ.Equiv σ) : ↑φ.toLinearEquiv = (↑φ).toLinearMap

theorem Representation.Equiv.toLinearEquiv_apply {A : Type u_1} {G : Type u_2} {V : Type u_3} {W : Type u_4} [Semiring A] [Monoid G] [AddCommMonoid V] [AddCommMonoid W] [Module A V] [Module A W] {ρ : Representation A G V} {σ : Representation A G W} (φ : ρ.Equiv σ) (v : V) : φ.toLinearEquiv v = ↑φ v

def Representation.Equiv.symm {A : Type u_1} {G : Type u_2} {V : Type u_3} {W : Type u_4} [Semiring A] [Monoid G] [AddCommMonoid V] [AddCommMonoid W] [Module A V] [Module A W] {ρ : Representation A G V} {σ : Representation A G W} (φ : ρ.Equiv σ) : σ.Equiv ρ

The equiv between representations are symmetric.

Equations

• φ.symm = { toLinearMap := ↑φ.toLinearEquiv.symm, isIntertwining' := ⋯, invFun := φ.toLinearEquiv.symm.invFun, left_inv := ⋯, right_inv := ⋯ }

theorem Representation.Equiv.toLinearMap_symm {A : Type u_1} {G : Type u_2} {V : Type u_3} {W : Type u_4} [Semiring A] [Monoid G] [AddCommMonoid V] [AddCommMonoid W] [Module A V] [Module A W] {ρ : Representation A G V} {σ : Representation A G W} (φ : ρ.Equiv σ) : (↑φ.symm).toLinearMap = ↑φ.toLinearEquiv.symm

theorem Representation.Equiv.coe_symm {A : Type u_1} {G : Type u_2} {V : Type u_3} {W : Type u_4} [Semiring A] [Monoid G] [AddCommMonoid V] [AddCommMonoid W] [Module A V] [Module A W] {ρ : Representation A G V} {σ : Representation A G W} (φ : ρ.Equiv σ) : ⇑φ.toLinearEquiv.symm = ⇑φ.symm

theorem LinearEquiv.isIntertwining_symm_isIntertwining {A : Type u_1} {G : Type u_2} {V : Type u_3} {W : Type u_4} [Semiring A] [Monoid G] [AddCommMonoid V] [AddCommMonoid W] [Module A V] [Module A W] {ρ : Representation A G V} {σ : Representation A G W} {e : V ≃ₗ[A] W} (he : ∀ (g : G), ↑e ∘ₗ ρ g = σ g ∘ₗ ↑e) (g : G) : ↑e.symm ∘ₗ σ g = ρ g ∘ₗ ↑e.symm

@[simp]

theorem Representation.Equiv.mk_symm {A : Type u_1} {G : Type u_2} {V : Type u_3} {W : Type u_4} [Semiring A] [Monoid G] [AddCommMonoid V] [AddCommMonoid W] [Module A V] [Module A W] {ρ : Representation A G V} {σ : Representation A G W} {e : V ≃ₗ[A] W} (he1 : ∀ (g : G), ↑e ∘ₗ ρ g = σ g ∘ₗ ↑e) : (mk e he1).symm = mk e.symm ⋯

def Representation.Equiv.trans {A : Type u_1} {G : Type u_2} {V : Type u_3} {W : Type u_4} {U : Type u_5} [Semiring A] [Monoid G] [AddCommMonoid V] [AddCommMonoid W] [AddCommMonoid U] [Module A V] [Module A W] [Module A U] {ρ : Representation A G V} {σ : Representation A G W} {τ : Representation A G U} (φ : ρ.Equiv σ) (ψ : σ.Equiv τ) : ρ.Equiv τ

Composition of two Equiv.

Equations

• φ.trans ψ = { toLinearMap := ↑(φ.toLinearEquiv ≪≫ₗ ψ.toLinearEquiv), isIntertwining' := ⋯, invFun := (φ.toLinearEquiv ≪≫ₗ ψ.toLinearEquiv).invFun, left_inv := ⋯, right_inv := ⋯ }

@[simp]

theorem Representation.Equiv.toIntertwiningMap_trans {A : Type u_1} {G : Type u_2} {V : Type u_3} {W : Type u_4} {U : Type u_5} [Semiring A] [Monoid G] [AddCommMonoid V] [AddCommMonoid W] [AddCommMonoid U] [Module A V] [Module A W] [Module A U] {ρ : Representation A G V} {σ : Representation A G W} {τ : Representation A G U} (φ : ρ.Equiv σ) (ψ : σ.Equiv τ) : ↑(φ.trans ψ) = (↑ψ).comp ↑φ

@[simp]

theorem Representation.Equiv.toLinearMap_trans {A : Type u_1} {G : Type u_2} {V : Type u_3} {W : Type u_4} {U : Type u_5} [Semiring A] [Monoid G] [AddCommMonoid V] [AddCommMonoid W] [AddCommMonoid U] [Module A V] [Module A W] [Module A U] {ρ : Representation A G V} {σ : Representation A G W} {τ : Representation A G U} (φ : ρ.Equiv σ) (ψ : σ.Equiv τ) : (↑(φ.trans ψ)).toLinearMap = (↑ψ).toLinearMap ∘ₗ (↑φ).toLinearMap

@[simp]

theorem Representation.Equiv.trans_apply {A : Type u_1} {G : Type u_2} {V : Type u_3} {W : Type u_4} {U : Type u_5} [Semiring A] [Monoid G] [AddCommMonoid V] [AddCommMonoid W] [AddCommMonoid U] [Module A V] [Module A W] [Module A U] {ρ : Representation A G V} {σ : Representation A G W} {τ : Representation A G U} (φ : ρ.Equiv σ) (ψ : σ.Equiv τ) (v : V) : (φ.trans ψ) v = ψ (φ v)

@[simp]

theorem Representation.Equiv.apply_symm_apply {A : Type u_1} {G : Type u_2} {V : Type u_3} {W : Type u_4} [Semiring A] [Monoid G] [AddCommMonoid V] [AddCommMonoid W] [Module A V] [Module A W] {ρ : Representation A G V} {σ : Representation A G W} (φ : ρ.Equiv σ) (v : W) : φ (φ.symm v) = v

@[simp]

theorem Representation.Equiv.symm_apply_apply {A : Type u_1} {G : Type u_2} {V : Type u_3} {W : Type u_4} [Semiring A] [Monoid G] [AddCommMonoid V] [AddCommMonoid W] [Module A V] [Module A W] {ρ : Representation A G V} {σ : Representation A G W} (φ : ρ.Equiv σ) (v : V) : φ.symm (φ v) = v

@[simp]

theorem Representation.Equiv.trans_symm {A : Type u_1} {G : Type u_2} {V : Type u_3} {W : Type u_4} [Semiring A] [Monoid G] [AddCommMonoid V] [AddCommMonoid W] [Module A V] [Module A W] {ρ : Representation A G V} {σ : Representation A G W} (φ : ρ.Equiv σ) : φ.trans φ.symm = refl ρ

@[simp]

theorem Representation.Equiv.symm_trans {A : Type u_1} {G : Type u_2} {V : Type u_3} {W : Type u_4} [Semiring A] [Monoid G] [AddCommMonoid V] [AddCommMonoid W] [Module A V] [Module A W] {ρ : Representation A G V} {σ : Representation A G W} (φ : ρ.Equiv σ) : φ.symm.trans φ = refl σ

theorem Representation.Equiv.conj_apply_self {A : Type u_1} {G : Type u_2} {V : Type u_3} {W : Type u_4} [CommSemiring A] [Monoid G] [AddCommMonoid V] [AddCommMonoid W] [Module A V] [Module A W] {ρ : Representation A G V} {σ : Representation A G W} (g : G) (φ : ρ.Equiv σ) : φ.toLinearEquiv.conj (ρ g) = σ g

@[implicit_reducible]

instance Representation.IntertwiningMap.instSMul {A : Type u_1} {G : Type u_2} {V : Type u_3} {W : Type u_4} [CommSemiring A] [Monoid G] [AddCommMonoid V] [AddCommMonoid W] [Module A V] [Module A W] (ρ : Representation A G V) (σ : Representation A G W) : SMul A (ρ.IntertwiningMap σ)

Equations

• Representation.IntertwiningMap.instSMul ρ σ = { smul := fun (a : A) (f : ρ.IntertwiningMap σ) => { toLinearMap := a • f.toLinearMap, isIntertwining' := ⋯ } }

@[simp]

theorem Representation.IntertwiningMap.coe_smul {A : Type u_1} {G : Type u_2} {V : Type u_3} {W : Type u_4} [CommSemiring A] [Monoid G] [AddCommMonoid V] [AddCommMonoid W] [Module A V] [Module A W] (ρ : Representation A G V) (σ : Representation A G W) (a : A) (f : ρ.IntertwiningMap σ) : ⇑(a • f) = a • ⇑f

@[simp]

theorem Representation.IntertwiningMap.toLinearMap_smul {A : Type u_1} {G : Type u_2} {V : Type u_3} {W : Type u_4} [CommSemiring A] [Monoid G] [AddCommMonoid V] [AddCommMonoid W] [Module A V] [Module A W] (ρ : Representation A G V) (σ : Representation A G W) (a : A) (f : ρ.IntertwiningMap σ) : (a • f).toLinearMap = a • f.toLinearMap

@[implicit_reducible]

instance Representation.IntertwiningMap.instModule {A : Type u_1} {G : Type u_2} {V : Type u_3} {W : Type u_4} [CommSemiring A] [Monoid G] [AddCommMonoid V] [AddCommMonoid W] [Module A V] [Module A W] (ρ : Representation A G V) (σ : Representation A G W) : Module A (ρ.IntertwiningMap σ)

Equations

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

def Representation.IntertwiningMap.equivLinearMapAsModule {A : Type u_1} {G : Type u_2} {V : Type u_3} {W : Type u_4} [CommSemiring A] [Monoid G] [AddCommMonoid V] [AddCommMonoid W] [Module A V] [Module A W] (ρ : Representation A G V) (σ : Representation A G W) : ρ.IntertwiningMap σ ≃ₗ[A] ρ.asModule →ₗ[MonoidAlgebra A G] σ.asModule

An intertwining map is the same thing as a linear map over the group ring.

Equations

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

def Representation.IntertwiningMap.llcomp {A : Type u_1} {G : Type u_2} {V : Type u_3} {W : Type u_4} {U : Type u_5} [CommSemiring A] [Monoid G] [AddCommMonoid V] [AddCommMonoid W] [AddCommMonoid U] [Module A V] [Module A W] [Module A U] (ρ : Representation A G V) (σ : Representation A G W) (τ : Representation A G U) : σ.IntertwiningMap τ →ₗ[A] ρ.IntertwiningMap σ →ₗ[A] ρ.IntertwiningMap τ

Composition of intertwining maps.

Equations

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

theorem Representation.IntertwiningMap.comp_def {A : Type u_1} {G : Type u_2} {V : Type u_3} {W : Type u_4} {U : Type u_5} [CommSemiring A] [Monoid G] [AddCommMonoid V] [AddCommMonoid W] [AddCommMonoid U] [Module A V] [Module A W] [Module A U] (ρ : Representation A G V) (σ : Representation A G W) (τ : Representation A G U) (f : σ.IntertwiningMap τ) (g : ρ.IntertwiningMap σ) : f.comp g = ((llcomp ρ σ τ) f) g

theorem Representation.IntertwiningMap.smul_comp {A : Type u_1} {G : Type u_2} {V : Type u_3} {W : Type u_4} {U : Type u_5} [CommSemiring A] [Monoid G] [AddCommMonoid V] [AddCommMonoid W] [AddCommMonoid U] [Module A V] [Module A W] [Module A U] (ρ : Representation A G V) (σ : Representation A G W) (τ : Representation A G U) (a : A) (f : σ.IntertwiningMap τ) (g : ρ.IntertwiningMap σ) : (a • f).comp g = a • f.comp g

theorem Representation.IntertwiningMap.comp_smul {A : Type u_1} {G : Type u_2} {V : Type u_3} {W : Type u_4} {U : Type u_5} [CommSemiring A] [Monoid G] [AddCommMonoid V] [AddCommMonoid W] [AddCommMonoid U] [Module A V] [Module A W] [Module A U] (ρ : Representation A G V) (σ : Representation A G W) (τ : Representation A G U) (a : A) (f : σ.IntertwiningMap τ) (g : ρ.IntertwiningMap σ) : f.comp (a • g) = a • f.comp g

@[implicit_reducible]

instance Representation.IntertwiningMap.instMul {A : Type u_1} {G : Type u_2} {V : Type u_3} [CommSemiring A] [Monoid G] [AddCommMonoid V] [Module A V] (ρ : Representation A G V) : Mul (ρ.IntertwiningMap ρ)

Equations

• Representation.IntertwiningMap.instMul ρ = { mul := Representation.IntertwiningMap.comp }

@[simp]

theorem Representation.IntertwiningMap.coe_mul {A : Type u_1} {G : Type u_2} {V : Type u_3} [CommSemiring A] [Monoid G] [AddCommMonoid V] [Module A V] (ρ : Representation A G V) (f g : ρ.IntertwiningMap ρ) : (f * g).toLinearMap = f.toLinearMap * g.toLinearMap

@[simp]

theorem Representation.IntertwiningMap.mul_apply {A : Type u_1} {G : Type u_2} {V : Type u_3} [CommSemiring A] [Monoid G] [AddCommMonoid V] [Module A V] (ρ : Representation A G V) (f g : ρ.IntertwiningMap ρ) (v : V) : (f * g) v = f (g v)

@[implicit_reducible]

instance Representation.IntertwiningMap.instOne {A : Type u_1} {G : Type u_2} {V : Type u_3} [CommSemiring A] [Monoid G] [AddCommMonoid V] [Module A V] (ρ : Representation A G V) : One (ρ.IntertwiningMap ρ)

Equations

• Representation.IntertwiningMap.instOne ρ = { one := Representation.IntertwiningMap.id ρ }

@[simp]

theorem Representation.IntertwiningMap.coe_one {A : Type u_1} {G : Type u_2} {V : Type u_3} [CommSemiring A] [Monoid G] [AddCommMonoid V] [Module A V] (ρ : Representation A G V) : ⇑1 = _root_.id

@[implicit_reducible]

instance Representation.IntertwiningMap.instSemigroup {A : Type u_1} {G : Type u_2} {V : Type u_3} [CommSemiring A] [Monoid G] [AddCommMonoid V] [Module A V] (ρ : Representation A G V) : Semigroup (ρ.IntertwiningMap ρ)

Equations

• Representation.IntertwiningMap.instSemigroup ρ = Function.Injective.semigroup (fun (f : ρ.IntertwiningMap ρ) => f.toLinearMap) ⋯ ⋯

@[implicit_reducible]

instance Representation.IntertwiningMap.instPowNat {A : Type u_1} {G : Type u_2} {V : Type u_3} [CommSemiring A] [Monoid G] [AddCommMonoid V] [Module A V] (ρ : Representation A G V) : Pow (ρ.IntertwiningMap ρ) ℕ

Equations

• Representation.IntertwiningMap.instPowNat ρ = { pow := fun (f : ρ.IntertwiningMap ρ) (n : ℕ) => npowRecAuto n f }

@[implicit_reducible]

instance Representation.IntertwiningMap.instMonoid {A : Type u_1} {G : Type u_2} {V : Type u_3} [CommSemiring A] [Monoid G] [AddCommMonoid V] [Module A V] (ρ : Representation A G V) : Monoid (ρ.IntertwiningMap ρ)

Equations

• Representation.IntertwiningMap.instMonoid ρ = Function.Injective.monoid (fun (f : ρ.IntertwiningMap ρ) => f.toLinearMap) ⋯ ⋯ ⋯ ⋯

@[implicit_reducible]

instance Representation.IntertwiningMap.instNatCast {A : Type u_1} {G : Type u_2} {V : Type u_3} [CommSemiring A] [Monoid G] [AddCommMonoid V] [Module A V] (ρ : Representation A G V) : NatCast (ρ.IntertwiningMap ρ)

Equations

• Representation.IntertwiningMap.instNatCast ρ = { natCast := fun (n : ℕ) => n • 1 }

@[implicit_reducible]

instance Representation.IntertwiningMap.instSemiring {A : Type u_1} {G : Type u_2} {V : Type u_3} [CommSemiring A] [Monoid G] [AddCommMonoid V] [Module A V] (ρ : Representation A G V) : Semiring (ρ.IntertwiningMap ρ)

Equations

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

@[implicit_reducible]

instance Representation.IntertwiningMap.instAlgebra {A : Type u_1} {G : Type u_2} {V : Type u_3} [CommSemiring A] [Monoid G] [AddCommMonoid V] [Module A V] (ρ : Representation A G V) : Algebra A (ρ.IntertwiningMap ρ)

Equations

• Representation.IntertwiningMap.instAlgebra ρ = Algebra.ofModule ⋯ ⋯

@[simp]

theorem Representation.IntertwiningMap.algebraMap_apply {A : Type u_1} {G : Type u_2} {V : Type u_3} [CommSemiring A] [Monoid G] [AddCommMonoid V] [Module A V] (ρ : Representation A G V) (a : A) : (algebraMap A (ρ.IntertwiningMap ρ)) a = a • 1

noncomputable def Representation.IntertwiningMap.equivAlgEnd {A : Type u_1} {G : Type u_2} {V : Type u_3} [CommSemiring A] [Monoid G] [AddCommMonoid V] [Module A V] (ρ : Representation A G V) : ρ.IntertwiningMap ρ ≃ₐ[A] Module.End (MonoidAlgebra A G) ρ.asModule

Intertwining maps from ρ to itself are the same as A[G]-linear endomorphisms.

Equations

• Representation.IntertwiningMap.equivAlgEnd ρ = AlgEquiv.ofLinearEquiv (Representation.IntertwiningMap.equivLinearMapAsModule ρ ρ) ⋯ ⋯

theorem Representation.IntertwiningMap.isIntertwiningMap_of_mem_center {A : Type u_1} {G : Type u_2} {V : Type u_3} [CommSemiring A] [Monoid G] [AddCommMonoid V] [Module A V] (ρ : Representation A G V) (g : G) (hg : g ∈ Submonoid.center G) : ρ.IsIntertwiningMap ρ (ρ g)

def Representation.IntertwiningMap.centralMul {A : Type u_1} {G : Type u_2} {V : Type u_3} [CommSemiring A] [Monoid G] [AddCommMonoid V] [Module A V] (ρ : Representation A G V) (g : G) (hg : g ∈ Submonoid.center G) : ρ.IntertwiningMap ρ

If g is a central element of a monoid G, then this is the action of g, considered as an intertwining map from any representation of G to itself.

Equations

• Representation.IntertwiningMap.centralMul ρ g hg = { toLinearMap := ρ g, isIntertwining' := ⋯ }

def Representation.IntertwiningMap.toLinearMapl {A : Type u_1} {G : Type u_2} {V : Type u_3} {W : Type u_4} [CommSemiring A] [Monoid G] [AddCommMonoid V] [AddCommMonoid W] [Module A V] [Module A W] (ρ : Representation A G V) (σ : Representation A G W) : ρ.IntertwiningMap σ →ₗ[A] V →ₗ[A] W

IntertwiningMap.toLinearMap as a linear map.

Equations

• Representation.IntertwiningMap.toLinearMapl ρ σ = { toFun := Representation.IntertwiningMap.toLinearMap, map_add' := ⋯, map_smul' := ⋯ }

@[simp]

theorem Representation.IntertwiningMap.toLinearMapl_apply {A : Type u_1} {G : Type u_2} {V : Type u_3} {W : Type u_4} [CommSemiring A] [Monoid G] [AddCommMonoid V] [AddCommMonoid W] [Module A V] [Module A W] (ρ : Representation A G V) (σ : Representation A G W) (self : ρ.IntertwiningMap σ) : (toLinearMapl ρ σ) self = self.toLinearMap

instance Representation.IntertwiningMap.instFiniteOfIsNoetherian {A : Type u_6} {G : Type u_7} {V : Type u_8} {W : Type u_9} [CommRing A] [Monoid G] [AddCommGroup V] [AddCommGroup W] [Module A V] [Module A W] (ρ : Representation A G V) (σ : Representation A G W) [Module.Finite A V] [IsNoetherian A W] : Module.Finite A (ρ.IntertwiningMap σ)

noncomputable def Representation.IntertwiningMap.ofBijective {A : Type u_1} {G : Type u_2} {V : Type u_3} {W : Type u_4} [CommSemiring A] [Monoid G] [AddCommMonoid V] [AddCommMonoid W] [Module A V] [Module A W] {ρ : Representation A G V} {σ : Representation A G W} (f : ρ.IntertwiningMap σ) (hf : Function.Bijective ⇑f) : ρ.Equiv σ

A bijective intertwining map is an equivalence of representations.

Equations

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

@[simp]

theorem Representation.IntertwiningMap.coe_ofBijective {A : Type u_1} {G : Type u_2} {V : Type u_3} {W : Type u_4} [CommSemiring A] [Monoid G] [AddCommMonoid V] [AddCommMonoid W] [Module A V] [Module A W] (ρ : Representation A G V) (σ : Representation A G W) (f : ρ.IntertwiningMap σ) (hf : Function.Bijective ⇑f) : ⇑(f.ofBijective hf) = ⇑f

def Representation.IntertwiningMap.tensor {A : Type u_1} {G : Type u_2} {V : Type u_3} {W : Type u_4} {U : Type u_5} [CommSemiring A] [Monoid G] [AddCommMonoid V] [AddCommMonoid W] [AddCommMonoid U] [Module A V] [Module A W] [Module A U] {ρ : Representation A G V} {σ : Representation A G W} {τ : Representation A G U} {P : Type u_6} [AddCommMonoid P] [Module A P] {π : Representation A G P} (f : ρ.IntertwiningMap σ) (g : τ.IntertwiningMap π) : (ρ.tprod τ).IntertwiningMap (σ.tprod π)

The tensor product of intertwining maps induced from tensor product of linear maps.

Equations

• f.tensor g = { toLinearMap := TensorProduct.map f.toLinearMap g.toLinearMap, isIntertwining' := ⋯ }

@[simp]

theorem Representation.IntertwiningMap.toLinearMap_tensor {A : Type u_1} {G : Type u_2} {V : Type u_3} {W : Type u_4} {U : Type u_5} [CommSemiring A] [Monoid G] [AddCommMonoid V] [AddCommMonoid W] [AddCommMonoid U] [Module A V] [Module A W] [Module A U] {ρ : Representation A G V} {σ : Representation A G W} {τ : Representation A G U} {P : Type u_6} [AddCommMonoid P] [Module A P] {π : Representation A G P} (f : ρ.IntertwiningMap σ) (g : τ.IntertwiningMap π) : (f.tensor g).toLinearMap = TensorProduct.map f.toLinearMap g.toLinearMap

@[simp]

theorem Representation.IntertwiningMap.tensor_apply {A : Type u_1} {G : Type u_2} {V : Type u_3} {W : Type u_4} {U : Type u_5} [CommSemiring A] [Monoid G] [AddCommMonoid V] [AddCommMonoid W] [AddCommMonoid U] [Module A V] [Module A W] [Module A U] {ρ : Representation A G V} {σ : Representation A G W} {τ : Representation A G U} {P : Type u_6} [AddCommMonoid P] [Module A P] {π : Representation A G P} (f : ρ.IntertwiningMap σ) (g : τ.IntertwiningMap π) (v : V) (w : U) : (f.tensor g) (v ⊗ₜ[A] w) = f v ⊗ₜ[A] g w

def Representation.IntertwiningMap.lTensor {A : Type u_1} {G : Type u_2} {V : Type u_3} {W : Type u_4} {U : Type u_5} [CommSemiring A] [Monoid G] [AddCommMonoid V] [AddCommMonoid W] [AddCommMonoid U] [Module A V] [Module A W] [Module A U] (ρ : Representation A G V) {σ : Representation A G W} {τ : Representation A G U} (f : σ.IntertwiningMap τ) : (ρ.tprod σ).IntertwiningMap (ρ.tprod τ)

The intertwining map induced from f : σ → τ to ρ.tprod σ → ρ.tprod τ.

Equations

• Representation.IntertwiningMap.lTensor ρ f = (Representation.IntertwiningMap.id ρ).tensor f

@[simp]

theorem Representation.IntertwiningMap.toLinearMap_lTensor {A : Type u_1} {G : Type u_2} {V : Type u_3} {W : Type u_4} {U : Type u_5} [CommSemiring A] [Monoid G] [AddCommMonoid V] [AddCommMonoid W] [AddCommMonoid U] [Module A V] [Module A W] [Module A U] {ρ : Representation A G V} {σ : Representation A G W} {τ : Representation A G U} (f : ρ.IntertwiningMap σ) : (lTensor τ f).toLinearMap = LinearMap.lTensor U f.toLinearMap

@[simp]

theorem Representation.IntertwiningMap.lTensor_apply {A : Type u_1} {G : Type u_2} {V : Type u_3} {W : Type u_4} {U : Type u_5} [CommSemiring A] [Monoid G] [AddCommMonoid V] [AddCommMonoid W] [AddCommMonoid U] [Module A V] [Module A W] [Module A U] {ρ : Representation A G V} {σ : Representation A G W} {τ : Representation A G U} (f : σ.IntertwiningMap τ) (v : V) (w : W) : (lTensor ρ f) (v ⊗ₜ[A] w) = v ⊗ₜ[A] f w

@[simp]

theorem Representation.IntertwiningMap.lTensor_id {A : Type u_1} {G : Type u_2} {V : Type u_3} {W : Type u_4} [CommSemiring A] [Monoid G] [AddCommMonoid V] [AddCommMonoid W] [Module A V] [Module A W] {ρ : Representation A G V} {σ : Representation A G W} : lTensor ρ (id σ) = id (ρ.tprod σ)

def Representation.IntertwiningMap.rTensor {A : Type u_1} {G : Type u_2} {V : Type u_3} {W : Type u_4} {U : Type u_5} [CommSemiring A] [Monoid G] [AddCommMonoid V] [AddCommMonoid W] [AddCommMonoid U] [Module A V] [Module A W] [Module A U] (ρ : Representation A G V) {σ : Representation A G W} {τ : Representation A G U} (f : σ.IntertwiningMap τ) : (σ.tprod ρ).IntertwiningMap (τ.tprod ρ)

The natural intertwining map σ.tprod ρ → τ.tprod ρ induced by f : σ → τ.

Equations

• Representation.IntertwiningMap.rTensor ρ f = f.tensor (Representation.IntertwiningMap.id ρ)

@[simp]

theorem Representation.IntertwiningMap.toLinearMap_rTensor {A : Type u_1} {G : Type u_2} {V : Type u_3} {W : Type u_4} {U : Type u_5} [CommSemiring A] [Monoid G] [AddCommMonoid V] [AddCommMonoid W] [AddCommMonoid U] [Module A V] [Module A W] [Module A U] {ρ : Representation A G V} {σ : Representation A G W} {τ : Representation A G U} (f : σ.IntertwiningMap τ) : (rTensor ρ f).toLinearMap = LinearMap.rTensor V f.toLinearMap

@[simp]

theorem Representation.IntertwiningMap.rTensor_apply {A : Type u_1} {G : Type u_2} {V : Type u_3} {W : Type u_4} {U : Type u_5} [CommSemiring A] [Monoid G] [AddCommMonoid V] [AddCommMonoid W] [AddCommMonoid U] [Module A V] [Module A W] [Module A U] {ρ : Representation A G V} {σ : Representation A G W} {τ : Representation A G U} (f : σ.IntertwiningMap τ) (v : V) (w : W) : (rTensor ρ f) (w ⊗ₜ[A] v) = f w ⊗ₜ[A] v

@[simp]

theorem Representation.IntertwiningMap.rTensor_id {A : Type u_1} {G : Type u_2} {V : Type u_3} {W : Type u_4} [CommSemiring A] [Monoid G] [AddCommMonoid V] [AddCommMonoid W] [Module A V] [Module A W] {ρ : Representation A G V} {σ : Representation A G W} : rTensor ρ (id σ) = id (σ.tprod ρ)

theorem Representation.IntertwiningMap.rTensor_comp_lTensor {A : Type u_1} {G : Type u_2} {V : Type u_3} {W : Type u_4} {U : Type u_5} [CommSemiring A] [Monoid G] [AddCommMonoid V] [AddCommMonoid W] [AddCommMonoid U] [Module A V] [Module A W] [Module A U] {ρ : Representation A G V} {σ : Representation A G W} {τ : Representation A G U} (f : σ.IntertwiningMap ρ) (g : ρ.IntertwiningMap τ) : (rTensor τ f).comp (lTensor σ g) = f.tensor g

theorem Representation.IntertwiningMap.lTensor_comp_rTensor {A : Type u_1} {G : Type u_2} {V : Type u_3} {W : Type u_4} {U : Type u_5} [CommSemiring A] [Monoid G] [AddCommMonoid V] [AddCommMonoid W] [AddCommMonoid U] [Module A V] [Module A W] [Module A U] {ρ : Representation A G V} {σ : Representation A G W} {τ : Representation A G U} (f : σ.IntertwiningMap ρ) (g : ρ.IntertwiningMap τ) : (lTensor τ f).comp (rTensor σ g) = g.tensor f

noncomputable def Representation.TensorProduct.comm {A : Type u_1} {G : Type u_2} {V : Type u_3} {W : Type u_4} [CommSemiring A] [Monoid G] [AddCommMonoid V] [AddCommMonoid W] [Module A V] [Module A W] (ρ : Representation A G V) (σ : Representation A G W) : (ρ.tprod σ).Equiv (σ.tprod ρ)

Equivalence between representations induced from TensorProduct.comm.

Equations

• Representation.TensorProduct.comm ρ σ = Representation.Equiv.mk (TensorProduct.comm A V W) ⋯

@[simp]

theorem Representation.TensorProduct.toLinearMap_comm {A : Type u_1} {G : Type u_2} {V : Type u_3} {W : Type u_4} [CommSemiring A] [Monoid G] [AddCommMonoid V] [AddCommMonoid W] [Module A V] [Module A W] (ρ : Representation A G V) (σ : Representation A G W) : (↑(comm ρ σ)).toLinearMap = ↑(_root_.TensorProduct.comm A V W)

@[simp]

theorem Representation.TensorProduct.comm_apply {A : Type u_1} {G : Type u_2} {V : Type u_3} {W : Type u_4} [CommSemiring A] [Monoid G] [AddCommMonoid V] [AddCommMonoid W] [Module A V] [Module A W] (ρ : Representation A G V) (σ : Representation A G W) (v : V) (w : W) : (comm ρ σ) (v ⊗ₜ[A] w) = w ⊗ₜ[A] v

theorem Representation.TensorProduct.comm_comp_lTensor {A : Type u_1} {G : Type u_2} {V : Type u_3} {W : Type u_4} {U : Type u_5} [CommSemiring A] [Monoid G] [AddCommMonoid V] [AddCommMonoid W] [AddCommMonoid U] [Module A V] [Module A W] [Module A U] (ρ : Representation A G V) (σ : Representation A G W) (τ : Representation A G U) (f : σ.IntertwiningMap τ) : (↑(comm ρ τ)).comp (IntertwiningMap.lTensor ρ f) = (IntertwiningMap.rTensor ρ f).comp ↑(comm ρ σ)

theorem Representation.TensorProduct.comm_comp_rTensor {A : Type u_1} {G : Type u_2} {V : Type u_3} {W : Type u_4} {U : Type u_5} [CommSemiring A] [Monoid G] [AddCommMonoid V] [AddCommMonoid W] [AddCommMonoid U] [Module A V] [Module A W] [Module A U] (ρ : Representation A G V) (σ : Representation A G W) (τ : Representation A G U) (f : σ.IntertwiningMap τ) : (↑(comm τ ρ)).comp (IntertwiningMap.rTensor ρ f) = (IntertwiningMap.lTensor ρ f).comp ↑(comm σ ρ)

theorem Representation.TensorProduct.comm_symm {A : Type u_1} {G : Type u_2} {V : Type u_3} {W : Type u_4} [CommSemiring A] [Monoid G] [AddCommMonoid V] [AddCommMonoid W] [Module A V] [Module A W] (ρ : Representation A G V) (σ : Representation A G W) : (comm σ ρ).symm = comm ρ σ

noncomputable def Representation.TensorProduct.assoc {A : Type u_1} {G : Type u_2} {V : Type u_3} {W : Type u_4} {U : Type u_5} [CommSemiring A] [Monoid G] [AddCommMonoid V] [AddCommMonoid W] [AddCommMonoid U] [Module A V] [Module A W] [Module A U] (ρ : Representation A G V) (σ : Representation A G W) (τ : Representation A G U) : ((ρ.tprod σ).tprod τ).Equiv (ρ.tprod (σ.tprod τ))

The Equiv between representations induced from TensorProduct.assoc.

Equations

• Representation.TensorProduct.assoc ρ σ τ = Representation.Equiv.mk (TensorProduct.assoc A V W U) ⋯

@[simp]

theorem Representation.TensorProduct.toLinearMap_assoc {A : Type u_1} {G : Type u_2} {V : Type u_3} {W : Type u_4} {U : Type u_5} [CommSemiring A] [Monoid G] [AddCommMonoid V] [AddCommMonoid W] [AddCommMonoid U] [Module A V] [Module A W] [Module A U] (ρ : Representation A G V) (σ : Representation A G W) (τ : Representation A G U) : (↑(assoc ρ σ τ)).toLinearMap = ↑(_root_.TensorProduct.assoc A V W U)

@[simp]

theorem Representation.TensorProduct.assoc_symm_toLinearMap {A : Type u_1} {G : Type u_2} {V : Type u_3} {W : Type u_4} {U : Type u_5} [CommSemiring A] [Monoid G] [AddCommMonoid V] [AddCommMonoid W] [AddCommMonoid U] [Module A V] [Module A W] [Module A U] (ρ : Representation A G V) (σ : Representation A G W) (τ : Representation A G U) : (↑(assoc ρ σ τ).symm).toLinearMap = ↑(_root_.TensorProduct.assoc A V W U).symm

@[simp]

theorem Representation.TensorProduct.assoc_apply {A : Type u_1} {G : Type u_2} {V : Type u_3} {W : Type u_4} {U : Type u_5} [CommSemiring A] [Monoid G] [AddCommMonoid V] [AddCommMonoid W] [AddCommMonoid U] [Module A V] [Module A W] [Module A U] (ρ : Representation A G V) (σ : Representation A G W) (τ : Representation A G U) (v : V) (w : W) (u : U) : (assoc ρ σ τ) (v ⊗ₜ[A] w ⊗ₜ[A] u) = v ⊗ₜ[A] (w ⊗ₜ[A] u)

noncomputable def Representation.TensorProduct.rid (A : Type u_1) {G : Type u_2} {W : Type u_4} [CommSemiring A] [Monoid G] [AddCommMonoid W] [Module A W] (σ : Representation A G W) : (σ.tprod (trivial A G A)).Equiv σ

The Equiv between representations induced from TensorProduct.rid.

Equations

• Representation.TensorProduct.rid A σ = Representation.Equiv.mk (TensorProduct.rid A W) ⋯

@[simp]

theorem Representation.TensorProduct.toLinearMap_rid {A : Type u_1} {G : Type u_2} {W : Type u_4} [CommSemiring A] [Monoid G] [AddCommMonoid W] [Module A W] (σ : Representation A G W) : (↑(rid A σ)).toLinearMap = ↑(_root_.TensorProduct.rid A W)

@[simp]

theorem Representation.TensorProduct.rid_apply {A : Type u_1} {G : Type u_2} {W : Type u_4} [CommSemiring A] [Monoid G] [AddCommMonoid W] [Module A W] (σ : Representation A G W) (w : W) (a : A) : (rid A σ) (w ⊗ₜ[A] a) = a • w

@[simp]

theorem Representation.TensorProduct.rid_symm_apply {A : Type u_1} {G : Type u_2} {W : Type u_4} [CommSemiring A] [Monoid G] [AddCommMonoid W] [Module A W] (σ : Representation A G W) (w : W) : (rid A σ).symm w = w ⊗ₜ[A] 1

noncomputable def Representation.TensorProduct.lid (A : Type u_1) {G : Type u_2} {W : Type u_4} [CommSemiring A] [Monoid G] [AddCommMonoid W] [Module A W] (σ : Representation A G W) : ((trivial A G A).tprod σ).Equiv σ

The Equiv between representations induced from TensorProduct.lid.

Equations

• Representation.TensorProduct.lid A σ = Representation.Equiv.mk (TensorProduct.lid A W) ⋯

@[simp]

theorem Representation.TensorProduct.toLinearMap_lid {A : Type u_1} {G : Type u_2} {W : Type u_4} [CommSemiring A] [Monoid G] [AddCommMonoid W] [Module A W] (σ : Representation A G W) : (↑(lid A σ)).toLinearMap = ↑(_root_.TensorProduct.lid A W)

@[simp]

theorem Representation.TensorProduct.lid_apply {A : Type u_1} {G : Type u_2} {W : Type u_4} [CommSemiring A] [Monoid G] [AddCommMonoid W] [Module A W] (σ : Representation A G W) (a : A) (w : W) : (lid A σ) (a ⊗ₜ[A] w) = a • w

@[simp]

theorem Representation.TensorProduct.lid_symm_apply {A : Type u_1} {G : Type u_2} {W : Type u_4} [CommSemiring A] [Monoid G] [AddCommMonoid W] [Module A W] (σ : Representation A G W) (w : W) : (lid A σ).symm w = 1 ⊗ₜ[A] w

noncomputable def Representation.Equiv.dualTensorHom {G : Type u_6} {k : Type u_7} {V : Type u_8} {W : Type u_9} [Group G] [Field k] [AddCommGroup V] [Module k V] [AddCommGroup W] [Module k W] [FiniteDimensional k V] (ρ : Representation k G V) (σ : Representation k G W) : (ρ.dual.tprod σ).Equiv (ρ.linHom σ)

dualTensorHom as an equivalence of representations.

Equations

• Representation.Equiv.dualTensorHom ρ σ = { toLinearMap := ↑(dualTensorHomEquiv k V W), isIntertwining' := ⋯, invFun := (dualTensorHomEquiv k V W).invFun, left_inv := ⋯, right_inv := ⋯ }

@[simp]

theorem Representation.Equiv.dualTensorHom_toFun {G : Type u_6} {k : Type u_7} {V : Type u_8} {W : Type u_9} [Group G] [Field k] [AddCommGroup V] [Module k V] [AddCommGroup W] [Module k W] [FiniteDimensional k V] (ρ : Representation k G V) (σ : Representation k G W) (a✝ : TensorProduct k (Module.Dual k V) W) : (dualTensorHom ρ σ) a✝ = (TensorProduct.liftAux LinearMap.smulRightₗ) a✝

@[simp]

theorem Representation.Equiv.dualTensorHom_invFun {G : Type u_6} {k : Type u_7} {V : Type u_8} {W : Type u_9} [Group G] [Field k] [AddCommGroup V] [Module k V] [AddCommGroup W] [Module k W] [FiniteDimensional k V] (ρ : Representation k G V) (σ : Representation k G W) (a✝ : V →ₗ[k] W) : (dualTensorHom ρ σ).invFun a✝ = (dualTensorHomEquivOfBasis (Module.Free.chooseBasis k V)).symm a✝