Injectivity of functor.op

Stream: Is there code for X?

[Yaël Dillies]

Not that it's hard to prove but do we really not have this anywhere?

import category_theory.opposites

open category_theory

example (C D : Type*) [category C] [category D] :
  function.injective (functor.op : C ⥤ D → Cᵒᵖ ⥤ Dᵒᵖ) :=
sorry```

[Riccardo Brasca]

To be honest I don't even understand what this means. The meaningful notion is faithfulness, and we have docs@category_theory.functor.op.category_theory.faithful.

[Yaël Dillies]

Sorry, got confused with docs#quiver.hom.op and indeed we have docs#quiver.hom.op_inj

[Riccardo Brasca]

Ah sorry, you mean that "taking the opposite" is an injective function!

[Riccardo Brasca]

Then this is true because it is idempotent

[Yaël Dillies]

...part of an equiv, you mean? :grinning:

[Riccardo Brasca]

Ahahah, yes... but beware that this a rare case in category theory, where two categories are really isomorphic (this is what we probably call an equiv). The correct notion is docs#category_theory.equivalence (it is weaker, but the other one, having a bijection between the objects such that blah blah is very often a bad notion).

[Yaël Dillies]

Yaël Dillies said:

Sorry, got confused with docs#quiver.hom.op and indeed we have docs#quiver.hom.op_inj

Equality of morphisms is well-behaved.

[Riccardo Brasca]

Yes, sure. I mean that functors form a category (with natural transformation as morphisms), and op gives an equivalence of categories C ⥤ D ≌ Cᵒᵖ ⥤ Dᵒᵖ. In this specific case this is more that an equivalence of categories (indeed nobody usually even consider this operation), but this is pretty rare.

[Yaël Dillies]

But I'm not talking about functors (anymore)! :upside_down: