dagger categories

Stream: maths

[Alex Ghorbani]

Hi all, im wondering if there is any work being done on defining dagger categories in the mathlib. I have the end goal of defining a compact closed dagger category: https://ncatlab.org/nlab/show/compact+closed+dagger+category

[Jakob von Raumer]

More work on all sorts of monoidal categories would be cool!

[Jakob von Raumer]

Even the definition of a dagger cat is still missing

[Alex Ghorbani]

I have started working on the definition of dagger categories and I'm running into an issue at the moment, any help would be appreciated:

class dagger_cat (C : Type u) [category.{v} C] :=
  (hom_dagger : ∀ x y : C, (x ⟶ y) → (y ⟶ x))
  (id_dagger : ∀ x : C, (hom_dagger x x ) = 𝟙 x)
  (double_dagger : ∀ f : C ⟶ C, hom_dagger (hom_dagger f) = f)
  (comp_dagger : ∀ f g : C ⟶ C, hom_dagger (f ≫ g) = hom_dagger f ≫ hom_dagger g)

I know that my line specifying the identity condition is written incorrectly as is, but im not quite sure how i should express it. I think I my have started off incorrectly in the way I defined the dagger function. What would be a correct way of writing this definition? Thanks

[Alex Ghorbani]

I seemed to have fixed my issue with the identity condition, so the code is now written as:

class dagger_cat (C : Type u) [category.{v} C] :=
  (hom_dagger : ∀ x y : C, (x ⟶ y) → (y ⟶ x))
  (id_dagger : ∀ x : C, (hom_dagger x x (𝟙 x)) = 𝟙 x)
  (double_dagger : ∀ f : C ⟶ C, hom_dagger (hom_dagger f) = f)
  (comp_dagger : ∀ f g : C ⟶ C, hom_dagger (f ≫ g) = hom_dagger f ≫ hom_dagger g)

However I now get an error saying

failed to synthesize type class instance for
C : Type u,
_inst_1 : category C,
hom_dagger : Π (x y : C), (x ⟶ y) → (y ⟶ x),
id_dagger : ∀ (x : C), hom_dagger x x (𝟙 x) = 𝟙 x
⊢ quiver (Type u)

I do not know what this error means so I don't know exactly why what I have written is wrong.

[Alex Ghorbani]

Ok i see that I have been writing \hom when I meant to be writing \-> which is why I got the quiver related error

[Antoine Labelle]

In double_dagger and comp_dagger, f shouldn't be of type C ⟶ C (which isn't even defined, that's why Lean complains). It should be of type x ⟶ y for x y : C.

[Antoine Labelle]

You do want to use \hom and not \-> though

[Alex Ghorbani]

Great thank you! I'll write that up and see what new errors I potentially encounter

[Alex Ghorbani]

I've made the suggested changes and now I have the following issue: with the following code

class dagger_cat (C : Type u) [category.{v} C] :=
  (hom_dagger : ∀ x y : C, (x → y) → (y → x))
  (id_dagger : ∀ x : C, (hom_dagger 𝟙 x) = 𝟙 x)
  (double_dagger : ∀ x y : C, hom_dagger (hom_dagger x → y) = x → y)
  (comp_dagger : ∀ x y z : C, hom_dagger (x → y ≫ y → z) = hom_dagger y → z ≫ hom_dagger x → y)

I get the error

type expected at
  x
term has type
  C

on the second line (the one with hom_dagger)

[Julian Külshammer]

I think now you have converted too many \hom to \->. Between x and y there should still be \hom

[Junyan Xu]

I think what you want is

import category_theory.category.basic
universes v u
open category_theory
class dagger_cat (C : Type u) [category.{v} C] :=
(hom_dagger {x y : C} : (x ⟶ y) → (y ⟶ x))
(id_dagger (x) : hom_dagger (𝟙 x) = 𝟙 x)
(double_dagger {x y} (f : x ⟶ y) : hom_dagger (hom_dagger f) = f)
/- `dagger_involutive` seems a better name. -/
(comp_dagger {x y z} (f : x ⟶ y) (g : y ⟶ z) : hom_dagger (f ≫ g) = hom_dagger g ≫ hom_dagger f)

[Junyan Xu]

You were omitting two many parentheses (hom_dagger 𝟙 x instead of hom_dagger (𝟙 x), hom_dagger x → y instead of hom_dagger (x → y)), and you didn't make x and y implicit in hom_dagger so you were bound to get an error when not providing x and y (for example you would need to write hom_dagger x x (𝟙 x)).

[Alex Ghorbani]

Ah that makes sense thank you so much @Junyan Xu !

[Alex Ghorbani]

My next step is to define dagger functors. Is the following definition coherent?

variables (C : Type u₁) [category.{v₁} C] [dagger_category C]
          (D : Type u₂) [category.{v₂} D] [dagger_category D]

structure dagger_functor extends C ⥤ D :=
  (blank {x y : C} (f : x ⟶ y) :
    map (dagger_category.hom_dagger f) = dagger_category.hom_dagger (map f))

Thanks again

[Alex Ghorbani]

Ok ive made some more progress and have now defined monoidal dagger categories and am now trying to define braided monoidal dagger categories. The idea is that the braiding for a braided monoidal dagger category must be a natural isomorphism between dagger functors. My question is that if I want to define something like a dagger natural transformation, do I first need to define the category of dagger categories?

[Andrew Yang]

For dagger natural transformations, I think you only need the category of dagger functors, which should be a docs#category_theory.full_subcategory of the category of functors.

[Alex Ghorbani]

Hi all. Im trying to implement what is suggested here (showing that the category of dagger functors is a full subcategory of the category of functors) and I wanted to ask how I should go about doing this. Should I create the category of dagger functors as an instance of the category of functors? Will that give me immediate access to dagger natural transformations? If not, what is required? Thanks

[Antoine Labelle]

If you follow that approach then you can define
def dagger_functor (C D : Type*) [dagger_category C] [dagger_category D] := full_subcategory is_dagger_functor where
is_dagger_functor : (C \functor D) \to Prop is the predicate saying that a given functor preserves the dagger structure.

[Antoine Labelle]

Assuming that a dagger natural transformation is really just any natural transformation between dagger_functors, i.e. the dagger functor subcategory is full in the functor category.

[Antoine Labelle]

And then yes you get dagger natural transformations for free, the hom-set of a full_subcategory is defined to be just the hom-set in the parent category.

[Antoine Labelle]

By the way, you should probably start PRing what you have so far in small chunks! :smile: I'd love to have dagger categories personally for doing representation theory.

[Alex Ghorbani]

Awesome thanks for the help. I'll make a PR soon with what I have

[Bhavik Mehta]

It's worth noting that most structure on categories in mathlib is given as propositions, for example limits and colimits; whereas your dagger structure is given as data - you should think about what's the right choice here, bearing in mind that the rest of cathlib would do this differently

[Antoine Labelle]

Bhavik Mehta said:

It's worth noting that most structure on categories in mathlib is given as propositions, for example limits and colimits; whereas your dagger structure is given as data - you should think about what's the right choice here, bearing in mind that the rest of cathlib would do this differently

How would you give the dagger structure as a proposition? It seems to me that the dagger map is extra data that has to be specified.

[Bhavik Mehta]

Antoine Labelle said:

Bhavik Mehta said:

It's worth noting that most structure on categories in mathlib is given as propositions, for example limits and colimits; whereas your dagger structure is given as data - you should think about what's the right choice here, bearing in mind that the rest of cathlib would do this differently

How would you give the dagger structure as a proposition? It seems to me that the dagger map is extra data that has to be specified.

In exactly the same way as we do for, eg, the terminal object right now: the class says it exists and then the data is produced by choice. I'm not arguing that one option is better than the other by the way, just a warning that there are two options here! I invested quite a bit of time into the data-version of limits and colimits which is now wasted because it's now propositional; I don't want the same to happen to others!

[Antoine Labelle]

But that's not the same thing, the dagger of a morphism is not defined by a universal property. There's in general more than one dagger structure on a given category (even up to isomorphism).

[Antoine Labelle]

So you need to give data.