Categorical tensor power

Stream: Is there code for X?

[Yaël Dillies]

Do we have the tensor power in a monoidal category defined anywhere? I can't find it at a glance.

[Kevin Buzzard]

Do you want $(M\times M)\times M$ or $M\times (M\times M)$ for $M^3$?

[Adam Topaz]

I would associate everything to the right as usual (and even add a tensor product with the unit on the right!). Then use the coherence stuff to get isomorphisms to reassociate as needed.

[Kim Morrison]

We don't have this.

It may be worthwhile (eventually?) to have tensor products indexed by finite linearly ordered types (and then in a symmetric monoidal category, products indexed by finite types --- either by internally choosing an order, or defining the product as a section of the bundle of products over the space of choices).

[Yaël Dillies]

My motivation is the following:

import Mathlib.CategoryTheory.Monoidal.Braided.Basic

open CategoryTheory MonoidalCategory

variable {C : Type*} [Category C] [MonoidalCategory C] {A : C} {m n : ℕ}

def tensorPow (A : C) (n : ℕ) : C := sorry

infix:80 " ^⊗ " => tensorPow

def tensorPow_add : A ^⊗ (m + n) ≅ A ^⊗ m ⊗ A ^⊗ n := sorry

structure InducedPRO (A : C) : Type where ofExp :: exp : ℕ

namespace InducedPRO
variable {X X₁ X₂ Y Y₁ Y₂ Z : InducedPRO A}

structure Hom (X Y : InducedPRO A) : Type _ where
  ofHom :: hom : A ^⊗ X.exp ⟶ A ^⊗ Y.exp

instance instCategory : Category (InducedPRO A) := sorry

def Iso.ofEq (h : X.exp = Y.exp) : X ≅ Y := sorry

def Iso.mk (e : A ^⊗ X.exp ≅ A ^⊗ Y.exp) : X ≅ Y := sorry

instance instMonoidalCategoryStruct : MonoidalCategoryStruct (InducedPRO A) := sorry

instance instMonoidalCategory : MonoidalCategory (InducedPRO A) := sorry

variable [SymmetricCategory C]

instance instBraidedCategory : BraidedCategory (InducedPRO A) := sorry

instance instSymmetricCategory : SymmetricCategory (InducedPRO A) := sorry

[Johan Commelin]

What does PRO mean?

[Yaël Dillies]

https://ncatlab.org/nlab/show/PRO says that it stands for PROduct

[Antoine Chambert-Loir]

:fear: There, PROPis the acronym for “products and permutations category”…

[Yaël Dillies]

Yeah, it's not amazing terminology...

[Eric Wieser]

Kim Morrison said:

It may be worthwhile (eventually?) to have tensor products indexed by finite linearly ordered types (and then in a symmetric monoidal category, products indexed by finite types --- either by internally choosing an order, or defining the product as a section of the bundle of products over the space of choices).

How does this compare to docs#PiTensorProduct (apart from that being only in the category of modules, of course)?

[Yaël Dillies]

Most monoidal categories don't have arbitrary tensor products, but only finitely-indexed ones.

[Joël Riou]

Yaël Dillies said:

My motivation is the following:

As it seems you do not need the action of the symmetric group on the powers of A, if may be possible to use the free monoidal category F on a singleton (https://leanprover-community.github.io/mathlib4_docs/Mathlib/CategoryTheory/Monoidal/Free/Basic.html), there is a monoidal functor from this free category to C which sends the unique element of the singleton to A. It is know (to mathlib) that in this free category F, sets of morphisms are subsingletons, so that it should not be too hard to show that F is equivalent to the discrete category on ℕ (which may then be endowed with a monoidal category structure). Then, we get a monoidal functor G : Discrete ℕ ⥤ C which sends n to the nth power of A. Finally, if G : D ⥤ C is a monoidal functor, it may be possible to define a monoidal category structure on Fullsubcategory G.obj: if we apply this to Discrete ℕ ⥤ C, we would get a monoidal category whose type of objects would identify to ℕ and morphisms would identify to types of morphisms between powers of A. (I am not sure how to get the braided/symmetric structures though.)

[Joël Riou]

(Update: Discrete ℕ is already known to be a monoidal category, but the free category could be used to show a certain universal property of it.)

[Yaël Dillies]

Joël Riou said:

we would get a monoidal category whose type of objects would identify to ℕ and morphisms would identify to types of morphisms between powers of A.

I didn't dare to ask but yes a quick way to creating this category is exactly what I'm after!

[Yaël Dillies]

Joël Riou said:

if G : D ⥤ C is a monoidal functor, it may be possible to define a monoidal category structure on Fullsubcategory G.obj

I don't understand this, however. G.obj : D → C.

[Yaël Dillies]

It seems that what I want is the pullback of a category along a plain function. Does this exist?

[Eric Wieser]

Yaël Dillies said:

Most monoidal categories don't have arbitrary tensor products, but only finitely-indexed ones.

I think we concluded that PiTensorProduct is effectively finitely-supported, even if not finitely-indexed

[Markus Himmel]

Yaël Dillies said:

It seems that what I want is the pullback of a category along a plain function. Does this exist?

Yes, that's docs#CategoryTheory.InducedCategory

[Yaël Dillies]

Ahah! And is it customary to wrap a concrete InducedCategory in a type synonym?

[Yaël Dillies]

And do we agree that nothing exists about the monoidal structure of an InducedCategory?

[Markus Himmel]

FullSubcategory is a special case of InducedCategory, so it is possible that there is material on full subcategories that is easily generalized to induced categories.

[Joël Riou]

Yaël Dillies said:

And do we agree that nothing exists about the monoidal structure of an InducedCategory?

Yes, this is the reason why I have written it may be possible. I can try to do this part...

[Yaël Dillies]

That would be great :pray:

[Yaël Dillies]

The greater context is that my computer science friend is writing a categorical interpretation of resource theory and I am trying to convince her to formalise it in Lean. For my (non-categorical) scheme to work, I need at least the basics to be there, and it seems that the PRO induced by an object in a monoidal category is the first missing piece

[Yaël Dillies]

But exams are in three weeks, so I don't really have the luxury to do any more than toying around

[Yaël Dillies]

Yaël Dillies said:

And do we agree that nothing exists about the monoidal structure of an InducedCategory?

I think the way to go to construct MonoidalCategory (InducedCategory D F) is to take, tensorUnit, a function tensorObj : C → C → C along with a family of isomorphisms ∀ X Y, F (tensorObj X Y) ≅ F X ⊗ F Y. I don't think you need any more compatibility than that?

[Eric Wieser]

I think we already have that?

[Eric Wieser]

I built this pullback stuff for when I build the monoidal category of algebras

[Eric Wieser]

docs#CategoryTheory.Monoidal.induced

[Joël Riou]

Yaël Dillies said:

I think the way to go to construct MonoidalCategory (InducedCategory D F) is to take, tensorUnit, a function tensorObj : C → C → C along with a family of isomorphisms ∀ X Y, F (tensorObj X Y) ≅ F X ⊗ F Y. I don't think you need any more compatibility than that?

This is actually more simple, because we already have a monoidal functor C ⥤ D:

import Mathlib.CategoryTheory.Monoidal.Functor

namespace CategoryTheory.MonoidalCategory

variable {C D : Type*} [Category C] [Category D]
  [MonoidalCategory C] [MonoidalCategory D] (F : MonoidalFunctor C D)

noncomputable instance : MonoidalCategoryStruct (InducedCategory D F.obj) where
  tensorObj X Y := ((X : C) ⊗ (Y : C) : C)
  tensorUnit := (tensorUnit : C)
  whiskerLeft X {Y₁ Y₂} g := ((F.μIso X Y₁).inv ≫ _ ◁ g ≫ (F.μIso X Y₂).hom : F.obj _ ⟶ F.obj _)
  whiskerRight := sorry
  tensorHom := sorry
  associator X Y Z :=
    { hom := F.map (associator (C := C) X Y Z).hom
      inv := F.map (associator (C := C) X Y Z).inv
      hom_inv_id := sorry
      inv_hom_id := sorry }
  leftUnitor := sorry
  rightUnitor := sorry

end CategoryTheory.MonoidalCategory

(This construction is different from what @Eric Wieser refers to also.)

[Yaël Dillies]

Something I'm noticing with docs#CategoryTheory.InducedCategory is that it's a semireducible type synonym without explicit transport functions, making it very hard to get the types right. Any objection to turning it and its hom type into one-field structures?

[Joël Riou]

Yes, I agree.

[Yaël Dillies]

Where is the monoidal category structure on ℕ given by addition with only the trivial morphisms?

[Joël Riou]

Monoidal/Discrete.lean

[Joël Riou]

A very draft PR for the construction of the induced monoidal category structure #12926

[Adam Topaz]

Yaël Dillies said:

Something I'm noticing with docs#CategoryTheory.InducedCategory is that it's a semireducible type synonym without explicit transport functions, making it very hard to get the types right. Any objection to turning it and its hom type into one-field structures?

We have had some discussions about doing this a long time ago, and I am very much in favor.

[Adam Topaz]

This reminds me that I should start PRing all that stuff about Lawvere theories...