## Stream: new members

### Topic: opposite Hom in the opposite category

#### Yakov Pechersky (May 19 2023 at 13:04):

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 (May 19 2023 at 13:04):

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

#### Jireh Loreaux (May 19 2023 at 13:11):

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 (May 19 2023 at 13:12):

docs4#Opposite aah it's a one field structure

#### Joël Riou (May 19 2023 at 18:59):

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

Last updated: Dec 20 2023 at 11:08 UTC