Product and coproduct in the opposite category

Stream: Is there code for X?

[Riccardo Brasca]

Do we have something like the following?

import Mathlib.CategoryTheory.Limits.Preserves.Opposites

open CategoryTheory Opposite Limits

variable {C : Type _} [Category C] {α : Type} [Finite α]
  (Z : α → C) [HasFiniteProducts C]

example : op (∏ Z) ≅ ∐ (fun z => op (Z z)) := sorry

I had a look in around docs#CategoryTheory.Limits.hasFiniteCoproducts_opposite, where the instance HasFiniteCoproduct on Cᵒᵖ is defined, but I don't see it.

[Adam Topaz]

import Mathlib.CategoryTheory.Limits.Preserves.Opposites

open CategoryTheory Opposite Limits

variable {C : Type _} [Category C] {α : Type} [Finite α]
  (Z : α → C) [HasFiniteProducts C]

noncomputable
example : op (∏ Z) ≅ ∐ (fun z => op (Z z)) :=
  let ee := Discrete.opposite α
  let E := (limit.cone (Discrete.functor Z)).op
  let hE : IsColimit E := (limit.isLimit (Discrete.functor Z)).op
  let E' := E.whisker (Discrete.opposite α).inverse
  let hE' : IsColimit E' := IsColimit.whiskerEquivalence hE ee.symm
  (hE'.coconePointsIsoOfEquivalence hE ee.symm <| Iso.refl _).symm
    ≪≫ hE'.coconePointUniqueUpToIso (colimit.isColimit _) ≪≫
    HasColimit.isoOfNatIso (Discrete.natIso fun _ => Iso.refl _)

Maybe this can be done with fewer lego blocks?

[Adam Topaz]

It's annoying because you need to use the equivalence between Discrete X and its opposite.

[Adam Topaz]

It would be easier to just construct the isomorphism by hand, I suppose.

[Riccardo Brasca]

Thanks! I will see what I can do with it tomorrow

[Adam Topaz]

I think this is much more manageable, but a few lines longer:

import Mathlib.CategoryTheory.Limits.Preserves.Opposites

open CategoryTheory Opposite Limits

variable {C : Type _} [Category C] {α : Type} [Finite α]
  (Z : α → C) [HasFiniteProducts C]

@[simps!]
noncomputable
def oppositeCofan : Cofan (fun z => op (Z z)) :=
  Cofan.mk (op <| ∏ Z) fun i => (Pi.π _ i).op

noncomputable
def isColimitOppositeCofan : IsColimit (oppositeCofan Z) where
  desc := fun S =>
    let e : S.pt.unop ⟶ ∏ Z := Pi.lift fun j => (S.ι.app _).unop
    e.op
  fac := fun S j => by
    dsimp only [oppositeCofan_pt, Functor.const_obj_obj,
      oppositeCofan_ι_app, Discrete.functor_obj]
    simp only [← op_comp, limit.lift_π,
      Fan.mk_pt, Fan.mk_π_app, Quiver.Hom.op_unop]
  uniq := fun S m hm => by
    rw [← m.op_unop]
    congr 1
    apply limit.hom_ext
    intro j
    simpa using congr_arg Quiver.Hom.unop (hm j)

noncomputable
example : op (∏ Z) ≅ ∐ (fun z => op (Z z)) :=
  isColimitOppositeCofan Z |>.coconePointUniqueUpToIso <| colimit.isColimit _