opposite Hom in the opposite category

Stream: new members

[Yakov Pechersky]

Just starting to learn categories from Aluffi. What are the differences between the two C^op I defined here, and why does mathlib go for the second one?

import Mathlib.CategoryTheory.Category.Basic

set_option autoImplicit false

open CategoryTheory

-- 3.1.  Let C be a category. Consider a structure Cᵒᵖ with Obj(Cᵒᵖ) := Obj(C);
-- for A, B objects of Cᵒᵖ (hence objects of C), Hom_Cᵒᵖ(A, B) := Hom_C(B, A).
-- Show how to make this into a category (that is, define composition of morphisms in Cᵒᵖ
-- and verify the properties listed in §3.1).
-- Intuitively, the 'opposite' category Cᵒᵖ is simply obtained by `reversing all the arrows' in C.
-- [5.1, §VIII.1.1, §IX.1.2, IX.1.10]
example {C : Type _} [hC : Category C] : Category (Cᵒᵖ) where
  Hom a b := (hC.Hom b.unop a.unop)
  id X := 𝟙 X.unop
  comp f g := g ≫ f
  id_comp f := hC.comp_id f
  comp_id f := hC.id_comp f
  assoc f g h := (hC.assoc h g f).symm

example {C : Type _} [hC : Category C] : Category (Cᵒᵖ) where
  Hom a b := (hC.Hom b.unop a.unop)ᵒᵖ
  id X := (𝟙 X.unop).op
  comp f g := (g.unop ≫ f.unop).op
  id_comp f := Opposite.unop_injective (hC.comp_id f.unop)
  comp_id f := Opposite.unop_injective (hC.id_comp f.unop)
  assoc f g h := Opposite.unop_injective (hC.assoc h.unop g.unop f.unop).symm

[Notification Bot]

This topic was moved here from #new members > opposite Him in the opposite category by Yakov Pechersky.

[Jireh Loreaux]

I could be wrong, but I suspect that the choice of the second one has to do with avoiding seeing through the defeq of the morphisms. This way it is protected under the op. But I'm speculating.

[Kevin Buzzard]

docs4#Opposite aah it's a one field structure

[Joël Riou]

I made the change in this PR !4#3193. The reason was what @Jireh Loreaux guessed.