Dealing with `op` doing Category Theory in Mathlib

Stream: mathlib4

[Joey Eremondi]

I'm wondering if people have any advice for dealing with ᵒᵖ when doing CategoryTheory in mathlib. I'm working with presheaves right now, so they show up all over the place. Are there tactics that are made to handle this?

For example, right now I've got X : Cᵒᵖ in a premise and unop X showing up in a goal. Of course, I can pattern match on X, and then the unop will reduce, but doing this every time for every single ᵒᵖ seems cumbersome, and the exact kind of thing Lean's tactics are good at dealing with. And I'm sure I'm hardly the first person who's had to deal with ᵒᵖ a bunch.

I'm not new to dependent types but I'm still very new to Lean and its tactics, so it's likely I'm missing something obvious.

[Adam Topaz]

We tend to use the simplifier extensively in the CategoryTheory library. The simp lemmas should have been set up to make things as seamless as possible (although I concede that some pain points still exist when dealing with opposites).

[Adam Topaz]

If you have an example illustrating some frustrations, please share it and we can try to give some advice about how to do things in an idiomatic way

[Notification Bot]

Kevin Buzzard has marked this topic as resolved.

[Notification Bot]

Kevin Buzzard has marked this topic as unresolved.

[Kevin Buzzard]

Sorry, that was me wildly clicking in an attempt to move this thread to #mathlib4 where it belongs (I've concluded that I can't do it).

[Joey Eremondi]

@Adam Topaz Here's an example of a goal I feel should be trivial that isn't (as far as I can see)

import Mathlib.CategoryTheory.Types
import Mathlib.CategoryTheory.Category.Basic
import Mathlib.Data.Opposite


open CategoryTheory
open Opposite

def test {C : Type u} [CCat : Category.{v}  C]
  (F : C -> Type u)
  (opMap : {Γ Δ : C} -> (θ : Δ ⟶ Γ) -> F Γ -> F Δ)
  (Γ Δ : Cᵒᵖ)
  (θ : Δ ⟶ Γ)
  : F (unop Γ) ⟶ F (unop Δ) := by
    intros a
    aesop_cat --fails

Basically this is the first part of a "constructor" for a presheaf: you have a mapping from objects to sets (types), and a contravariant way to lift arrows into functions between sets. I want to show that this gives a way to take an arrow in Cᵒᵖ into an arrow in Type, like what the map field of Functor wants.

It seems like it should be trivial, but the only way I can see to do it is pattern matching on Γ and Δ, which is very verbose, and isn't going to scale well as the number of objects in scope increases.

[Adam Topaz]

can you please provide a #mwe ?

[Notification Bot]

2 messages were moved here from #lean4 > Dealing with op doing Category Theory in Mathlib by Adam Topaz.

[Adam Topaz]

@Joey Eremondi I moved your messages to the #mathlib4 stream which is more appropriate for this question, as Kevin mentions above.

[Joey Eremondi]

@Adam Topaz Sorry, I added the imports so it's now self-contained

[Adam Topaz]

are you sure you don't need to flip the domain and codomain of theta?

[Adam Topaz]

I mean, in this case it's quite straightforward and one shouldn't use a heavy tactic such as aesop anyway:

import Mathlib

open CategoryTheory Opposite

def test {C : Type u} [Category.{v}  C]
    (F : C -> Type u)
    (opMap : {Γ Δ : C} -> (θ : Δ ⟶ Γ) -> F Γ -> F Δ)
    (Γ Δ : Cᵒᵖ)
    (θ : Γ ⟶ Δ) :
    F (unop Γ) ⟶ F (unop Δ) := opMap θ.unop

[Joey Eremondi]

@Adam Topaz Ah shoot you're right, I had it right in my actual version but messed it up making the MWE. Thanks.
And I missed that you can directly unop morphisms too. So I think I'm just (a) massively overthinking this and (b) still needing to read more docs.

Thanks for the help and sorry for the foncusion

[Adam Topaz]

I would say that in general the automation could have some issues with op/unop because many tactics work by looking at terms syntactically.

[Adam Topaz]

For example in this case if there were no ops, then aesop_cat would(should?) be able to solve the goal (modulo flipping the domain/codomain of theta again). But it doesn't work with op, I think essentially for this reason.

[Adam Topaz]

And yes, once you get used to docs#Opposite.op docs#Opposite.unop docs#Quiver.Hom.op and docs#Quiver.Hom.unop (and the associated API) things do become much more manageable

[Joey Eremondi]

@Adam Topaz One more quick question since you're here and know your stuff, are there tactics for dealing with category-theoretic isomorphisms? E.g. that let you rw or simp by an isomorphism between objects? Or is the best thing just to call .hom on the isomorphism and explicitly apply that?

[Adam Topaz]

You can't rewrite/simp with an isomorphism, but there are tools that help in constructing isomorphisms (like calc mode). Again, it would be helpful to see an example.

[Adam Topaz]

Again, the simplifier is the key here. When you define an isomorphism and use simps that will automatically generate simp lemmas that let you work with the isomorphism using the simplifier.

[Brendan Seamas Murphy]

To rewrite with isomorphisms we'd likely need to implement something like this: https://cs.au.dk/~spitters/Emil.pdf (congruence closure type stuff but with univalent equality instead of proof irrelevant equality)