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} [CommRing 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} [CommRing 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} [CommRing 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) (v : V) : self.toFun ((ρ g) v) = (σ g) (self.toFun v)

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

theorem Representation.IntertwiningMap.ext_iff {A : Type u_1} {G : Type u_2} {V : Type u_3} {W : Type u_4} {inst✝ : CommRing A} {inst✝¹ : Monoid G} {inst✝² : AddCommMonoid V} {inst✝³ : AddCommMonoid W} {inst✝⁴ : Module A V} {inst✝⁵ : Module A W} {ρ : Representation A G V} {σ : Representation A G W} {x y : ρ.IntertwiningMap σ} : x = y ↔ x.toFun = y.toFun

theorem Representation.IntertwiningMap.ext {A : Type u_1} {G : Type u_2} {V : Type u_3} {W : Type u_4} {inst✝ : CommRing A} {inst✝¹ : Monoid G} {inst✝² : AddCommMonoid V} {inst✝³ : AddCommMonoid W} {inst✝⁴ : Module A V} {inst✝⁵ : Module A W} {ρ : Representation A G V} {σ : Representation A G W} {x y : ρ.IntertwiningMap σ} (toFun : x.toFun = y.toFun) : x = y

theorem Representation.IntertwiningMap.toLinearMap_injective {A : Type u_1} {G : Type u_2} {V : Type u_3} {W : Type u_4} [CommRing 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} [CommRing 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

instance Representation.IntertwiningMap.instFunLike {A : Type u_1} {G : Type u_2} {V : Type u_3} {W : Type u_4} [CommRing 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' := ⋯ }

theorem Representation.IntertwiningMap.isIntertwining {A : Type u_1} {G : Type u_2} {V : Type u_3} {W : Type u_4} [CommRing 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 ((ρ g) v) = (σ g) (f v)

@[simp]

theorem Representation.IntertwiningMap.toLinearMap_apply {A : Type u_1} {G : Type u_2} {V : Type u_3} {W : Type u_4} [CommRing 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

instance Representation.IntertwiningMap.instZero {A : Type u_1} {G : Type u_2} {V : Type u_3} {W : Type u_4} [CommRing 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} [CommRing A] [Monoid G] [AddCommMonoid V] [AddCommMonoid W] [Module A V] [Module A W] (ρ : Representation A G V) (σ : Representation A G W) : ⇑0 = 0

instance Representation.IntertwiningMap.instAdd {A : Type u_1} {G : Type u_2} {V : Type u_3} {W : Type u_4} [CommRing 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} [CommRing 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

instance Representation.IntertwiningMap.instSMul {A : Type u_1} {G : Type u_2} {V : Type u_3} {W : Type u_4} [CommRing 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} [CommRing 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

instance Representation.IntertwiningMap.instSMulNat {A : Type u_1} {G : Type u_2} {V : Type u_3} {W : Type u_4} [CommRing 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} [CommRing A] [Monoid G] [AddCommMonoid V] [AddCommMonoid W] [Module A V] [Module A W] (ρ : Representation A G V) (σ : Representation A G W) (n : ℕ) (f : ρ.IntertwiningMap σ) : ⇑(n • f) = n • ⇑f

instance Representation.IntertwiningMap.instAddCommMonoid {A : Type u_1} {G : Type u_2} {V : Type u_3} {W : Type u_4} [CommRing 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.

def Representation.IntertwiningMap.coeFnAddMonoidHom {A : Type u_1} {G : Type u_2} {V : Type u_3} {W : Type u_4} [CommRing 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' := ⋯ }

instance Representation.IntertwiningMap.instModule {A : Type u_1} {G : Type u_2} {V : Type u_3} {W : Type u_4} [CommRing 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} [CommRing 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.

noncomputable def Representation.IntertwiningMap.id {A : Type u_1} {G : Type u_2} {V : Type u_3} [CommRing 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.id_apply {A : Type u_1} {G : Type u_2} {V : Type u_3} [CommRing A] [Monoid G] [AddCommMonoid V] [Module A V] (ρ : Representation A G V) (v : V) : (id ρ) v = v

theorem Representation.IntertwiningMap.isIntertwiningMap_of_mem_center {A : Type u_1} {G : Type u_2} {V : Type u_3} [CommRing 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} [CommRing 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' := ⋯ }