Tensoring a representation with an invariant

For an invariant y of a representation N, this file constructs the morphism of representations M ⟶ M ⊗ N that sends m to m ⊗ₜ y. It also records its additivity, linearity, naturality in both representations, and compatibility with the associator and braiding, as well as restriction along arbitrary homomorphisms of groups.

noncomputable def Rep.tensorInvariant {k : Type u} {G : Type v} [CommRing k] [Group G] (M : Rep k G) {N : Rep k G} (y : ↥N.ρ.invariants) : M ⟶ CategoryTheory.MonoidalCategoryStruct.tensorObj M N

For an invariant y of the representation N, the morphism of representations M ⟶ M ⊗ N, m ↦ m ⊗ₜ y.

@[simp]

theorem Rep.tensorInvariant_hom_apply {k : Type u} {G : Type v} [CommRing k] [Group G] (M : Rep k G) {N : Rep k G} (y : ↥N.ρ.invariants) (m : ↑M) : (Hom.hom (M.tensorInvariant y)) m = m ⊗ₜ[k] ↑y

The morphism m ↦ m ⊗ₜ y evaluated at m.

@[simp]

theorem Rep.resMap_tensorInvariant {k : Type u} {G : Type v} [CommRing k] [Group G] (M N : Rep k G) {H : Type w} [Group H] (f : H →* G) (y : ↥N.ρ.invariants) : resMap f (M.tensorInvariant y) = (res f M).tensorInvariant ((Submodule.inclusion ⋯) y)

Restricting the map m ↦ m ⊗ y along a homomorphism of groups gives the map defined by the restricted invariant.

@[simp]

theorem Rep.tensorInvariant_zero {k : Type u} {G : Type v} [CommRing k] [Group G] (M : Rep k G) {N : Rep k G} : M.tensorInvariant 0 = 0

m ↦ m ⊗ 0 is the zero morphism.

@[simp]

theorem Rep.tensorInvariant_add {k : Type u} {G : Type v} [CommRing k] [Group G] (M : Rep k G) {N : Rep k G} (y z : ↥N.ρ.invariants) : M.tensorInvariant (y + z) = M.tensorInvariant y + M.tensorInvariant z

m ↦ m ⊗ y is additive in y.

@[simp]

theorem Rep.tensorInvariant_smul {k : Type u} {G : Type v} [CommRing k] [Group G] (M : Rep k G) {N : Rep k G} (c : k) (y : ↥N.ρ.invariants) : M.tensorInvariant (c • y) = c • M.tensorInvariant y

m ↦ m ⊗ y is k-linear in y.

theorem Rep.hom_comp_tensorInvariant {k : Type u} {G : Type v} [CommRing k] [Group G] (M : Rep k G) {N M' : Rep k G} (f : M ⟶ M') (y : ↥N.ρ.invariants) : CategoryTheory.CategoryStruct.comp f (M'.tensorInvariant y) = CategoryTheory.CategoryStruct.comp (M.tensorInvariant y) (CategoryTheory.MonoidalCategoryStruct.whiskerRight f N)

m ↦ m ⊗ y is natural in M.

theorem Rep.hom_comp_tensorInvariant_assoc {k : Type u} {G : Type v} [CommRing k] [Group G] (M : Rep k G) {N M' : Rep k G} (f : M ⟶ M') (y : ↥N.ρ.invariants) {Z : Rep k G} (h : CategoryTheory.MonoidalCategoryStruct.tensorObj M' N ⟶ Z) : CategoryTheory.CategoryStruct.comp f (CategoryTheory.CategoryStruct.comp (M'.tensorInvariant y) h) = CategoryTheory.CategoryStruct.comp (M.tensorInvariant y) (CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.whiskerRight f N) h)

m ↦ m ⊗ y is natural in M.

theorem Rep.hom_comp_tensorInvariant_braiding {k : Type u} {G : Type v} [CommRing k] [Group G] (M : Rep k G) {M' : Rep k G} (f : M ⟶ M') {P : Rep k G} (x : ↥P.ρ.invariants) : CategoryTheory.CategoryStruct.comp f (CategoryTheory.CategoryStruct.comp (M'.tensorInvariant x) (β_ M' P).hom) = CategoryTheory.CategoryStruct.comp (M.tensorInvariant x) (CategoryTheory.CategoryStruct.comp (β_ M P).hom (CategoryTheory.MonoidalCategoryStruct.whiskerLeft P f))

After braiding, tensoring with an invariant is natural in the other factor.

theorem Rep.hom_comp_tensorInvariant_braiding_assoc {k : Type u} {G : Type v} [CommRing k] [Group G] (M : Rep k G) {M' : Rep k G} (f : M ⟶ M') {P : Rep k G} (x : ↥P.ρ.invariants) {Z : Rep k G} (h : CategoryTheory.MonoidalCategoryStruct.tensorObj P M' ⟶ Z) : CategoryTheory.CategoryStruct.comp f (CategoryTheory.CategoryStruct.comp (M'.tensorInvariant x) (CategoryTheory.CategoryStruct.comp (β_ M' P).hom h)) = CategoryTheory.CategoryStruct.comp (M.tensorInvariant x) (CategoryTheory.CategoryStruct.comp (β_ M P).hom (CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.whiskerLeft P f) h))

After braiding, tensoring with an invariant is natural in the other factor.

theorem Rep.tensorInvariant_comp_whiskerLeft {k : Type u} {G : Type v} [CommRing k] [Group G] (M : Rep k G) {N N' : Rep k G} (g : N ⟶ N') (y : ↥N.ρ.invariants) (y' : ↥N'.ρ.invariants) (hy : (Hom.hom g) ↑y = ↑y') : CategoryTheory.CategoryStruct.comp (M.tensorInvariant y) (CategoryTheory.MonoidalCategoryStruct.whiskerLeft M g) = M.tensorInvariant y'

m ↦ m ⊗ y is natural in N: composing with M ◁ g gives m ↦ m ⊗ g y.

theorem Rep.tensorInvariant_comp_associator {k : Type u} {G : Type v} [CommRing k] [Group G] (M N : Rep k G) {P : Rep k G} (z : ↥P.ρ.invariants) : CategoryTheory.CategoryStruct.comp ((CategoryTheory.MonoidalCategoryStruct.tensorObj M N).tensorInvariant z) (CategoryTheory.MonoidalCategoryStruct.associator M N P).hom = CategoryTheory.MonoidalCategoryStruct.whiskerLeft M (N.tensorInvariant z)

Tensoring M ⊗ N with an invariant and then reassociating is tensoring the second factor N with that invariant.

theorem Rep.tensorInvariant_comp_associator_assoc {k : Type u} {G : Type v} [CommRing k] [Group G] (M N : Rep k G) {P : Rep k G} (z : ↥P.ρ.invariants) {Z : Rep k G} (h : CategoryTheory.MonoidalCategoryStruct.tensorObj M (CategoryTheory.MonoidalCategoryStruct.tensorObj N P) ⟶ Z) : CategoryTheory.CategoryStruct.comp ((CategoryTheory.MonoidalCategoryStruct.tensorObj M N).tensorInvariant z) (CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.associator M N P).hom h) = CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.whiskerLeft M (N.tensorInvariant z)) h

Tensoring M ⊗ N with an invariant and then reassociating is tensoring the second factor N with that invariant.

theorem Rep.tensorInvariant_whiskerRight_comp_associator {k : Type u} {G : Type v} [CommRing k] [Group G] (M : Rep k G) {N : Rep k G} (P : Rep k G) (y : ↥N.ρ.invariants) : CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.whiskerRight (M.tensorInvariant y) P) (CategoryTheory.MonoidalCategoryStruct.associator M N P).hom = CategoryTheory.MonoidalCategoryStruct.whiskerLeft M (CategoryTheory.CategoryStruct.comp (P.tensorInvariant y) (β_ P N).hom)

Tensoring M with an invariant of N, tensoring the result on the right by P, and reassociating puts that invariant between the two original factors.

theorem Rep.tensorInvariant_whiskerRight_comp_associator_assoc {k : Type u} {G : Type v} [CommRing k] [Group G] (M : Rep k G) {N : Rep k G} (P : Rep k G) (y : ↥N.ρ.invariants) {Z : Rep k G} (h : CategoryTheory.MonoidalCategoryStruct.tensorObj M (CategoryTheory.MonoidalCategoryStruct.tensorObj N P) ⟶ Z) : CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.whiskerRight (M.tensorInvariant y) P) (CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.associator M N P).hom h) = CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.whiskerLeft M (CategoryTheory.CategoryStruct.comp (P.tensorInvariant y) (β_ P N).hom)) h

Tensoring M with an invariant of N, tensoring the result on the right by P, and reassociating puts that invariant between the two original factors.

theorem TauCeti.Rep.tensorInvariant_braiding_hom_apply {k : Type u} {G : Type v} [CommRing k] [Group G] {M N : Rep k G} (x : ↥M.ρ.invariants) (y : ↑N) : (Rep.Hom.hom (CategoryTheory.CategoryStruct.comp (N.tensorInvariant x) (β_ N M).hom)) y = ↑x ⊗ₜ[k] y

Braiding the tensor of a vector with an invariant puts the invariant first.

@[simp]

theorem TauCeti.Rep.tensorInvariant_braiding_rightUnitor_hom_apply {k : Type u} {G : Type v} [CommRing k] [Group G] {M : Rep k G} (x : ↥M.ρ.invariants) (c : k) : (Representation.TensorProduct.rid k M.ρ) ((Representation.TensorProduct.comm (Representation.trivial k G k) M.ρ) ((Rep.Hom.hom ((Rep.trivial k G k).tensorInvariant x)) c)) = c • ↑x

Tensoring a scalar of the trivial representation with an invariant x, braiding, and applying the right unitor sends c to c • x.

@[simp]

theorem Rep.tensorInvariant_one_braiding_leftUnitor {k : Type u} {G : Type v} [CommRing k] [Group G] (M : Rep k G) : CategoryTheory.CategoryStruct.comp (M.tensorInvariant ⟨1, ⋯⟩) (CategoryTheory.CategoryStruct.comp (β_ M (trivial k G k)).hom (CategoryTheory.MonoidalCategoryStruct.leftUnitor M).hom) = CategoryTheory.CategoryStruct.id M

Tensoring with the invariant 1 of the trivial representation, then braiding and applying the left unitor, is the identity.

theorem Rep.resMap_tensorInvariant_braiding {k : Type u} {G : Type v} [CommRing k] [Group G] {M : Rep k G} (N : Rep k G) {H : Type w} [Group H] (f : H →* G) (x : ↥M.ρ.invariants) (x' : ↥(res f M).ρ.invariants) (hx : ↑x' = ↑x) : resMap f (CategoryTheory.CategoryStruct.comp (N.tensorInvariant x) (β_ N M).hom) = CategoryTheory.CategoryStruct.comp ((res f N).tensorInvariant x') (β_ (res f N) (res f M)).hom

Restricting y ↦ x ⊗ₜ y along a monoid homomorphism gives the same map for the restricted representations, tensoring with x viewed as an invariant of the restriction.