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 {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.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.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_reducible]

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' := ⋯ }

@[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_reducible]

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_reducible]

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_reducible]

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_reducible]

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_reducible]

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_reducible]

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.

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' := ⋯ }

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.

Equations

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

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.

Equations

• f.comp g = ((Representation.IntertwiningMap.llcomp ρ σ τ) f) g

@[instance_reducible]

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

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} [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_reducible]

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

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} [CommRing A] [Monoid G] [AddCommMonoid V] [Module A V] (ρ : Representation A G V) : ⇑1 = _root_.id

@[instance_reducible]

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

Equations

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

@[instance_reducible]

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 ρ) ℕ

Equations

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

@[instance_reducible]

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

Equations

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

@[instance_reducible]

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

Equations

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

@[instance_reducible]

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

Equations

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

@[instance_reducible]

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

Equations

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

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

noncomputable 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.

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} [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' := ⋯ }