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

@[simp]

theorem Representation.IntertwiningMap.coe_mk {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) (h : ∀ (g : G) (v : V), f.toFun ((ρ g) v) = (σ g) (f.toFun v)) : ⇑{ toLinearMap := f, isIntertwining' := h } = ⇑f

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 σ)

@[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 σ)

@[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 σ)

@[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 σ)

@[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 σ)

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.

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 σ)

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.

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.

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

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

instance Representation.IntertwiningMap.instMul {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) : Mul (ρ.IntertwiningMap ρ)

@[simp]

theorem Representation.IntertwiningMap.coe_mul {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) (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} [CommRing A] [Monoid G] [AddCommMonoid V] [Module A V] (ρ : Representation A G V) (f g : ρ.IntertwiningMap ρ) (v : V) : (f * g) v = f (g v)

instance Representation.IntertwiningMap.instOne {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) : One (ρ.IntertwiningMap ρ)

@[simp]

theorem Representation.IntertwiningMap.coe_one {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) : ⇑1 = _root_.id

instance Representation.IntertwiningMap.instSemigroup {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) : Semigroup (ρ.IntertwiningMap ρ)

instance Representation.IntertwiningMap.instPowNat {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) : Pow (ρ.IntertwiningMap ρ) ℕ

instance Representation.IntertwiningMap.instMonoid {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) : Monoid (ρ.IntertwiningMap ρ)

instance Representation.IntertwiningMap.instNatCast {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) : NatCast (ρ.IntertwiningMap ρ)

instance Representation.IntertwiningMap.instSemiring {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) : Semiring (ρ.IntertwiningMap ρ)

instance Representation.IntertwiningMap.instAlgebra {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) : Algebra A (ρ.IntertwiningMap ρ)

@[simp]

theorem Representation.IntertwiningMap.algebraMap_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) (a : A) : (algebraMap A (ρ.IntertwiningMap ρ)) a = a • 1

def Representation.IntertwiningMap.equivAlgEnd {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 ρ ≃ₐ[A] Module.End (MonoidAlgebra A G) ρ.asModule

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

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.