Zulip Chat Archive

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