# Zulip Chat Archive

## Stream: maths

### Topic: over and under categories

#### Johan Commelin (Dec 17 2018 at 03:49):

Over and under categories show up all over the place (notably covers and structure maps can use over categories, and algebras can use under categories). I've written the definitions and a bunch of simp lemmas in https://github.com/leanprover-community/mathlib/blob/over_under/category_theory/comma.lean#L195

Now I would like to prove some facts about limits/colimits in these categories. What would be the right file in mathlib to put these?

#### Reid Barton (Dec 17 2018 at 04:33):

I guess the current "convention" would be a new file `category_theory.limits.<something>`

#### Johan Commelin (Dec 17 2018 at 05:49):

Ok, I'll do that. So that would probably be `category_theory.limits.over`

.

#### Chris Hughes (Dec 17 2018 at 08:03):

(deleted)

#### Johan Commelin (Dec 18 2018 at 19:42):

It seems I'm pushing the limits of the category library again.

I'm trying to prove an equivalence of two categories: https://github.com/leanprover-community/mathlib/blob/over_under/category_theory/comma.lean#L238

This is completely math-trivial: If I take `Y`

in the category `over X`

, then `over Y`

is equivalent to `over (Y.left)`

. There is almost no content... just composing some arrows. Still I'm running into deterministic timeouts and such. Is this just stuff that should wait?

#### Reid Barton (Dec 18 2018 at 20:06):

I think you should write out the components of the natural isomorphisms anyways

#### Patrick Massot (Dec 18 2018 at 21:58):

Does it mean that Scott's magic auto-param are failing here?

#### Johan Commelin (Dec 19 2018 at 04:20):

Partly, yes. Maybe that would be fixed once `back`

and `rewrite_search`

are part of mathlib. But another problem is that the code is just terribly slow. At some point I close a goal by `exact foobar`

and this takes several seconds. I guess that is just exhibiting that we are stacking lots of stuff on top of each other. (In particular the `pp.all`

output is usually not much fun to look at.)

Last updated: May 14 2021 at 18:28 UTC