Zulip Chat Archive

Stream: Is there code for X?

Topic: Filtered category equivalence


view this post on Zulip Bhavik Mehta (Dec 14 2020 at 19:15):

Do we have that a category equivalent to a filtered category is filtered?

view this post on Zulip Adam Topaz (Dec 15 2020 at 00:33):

I don't know the answer, but I wish we had a tactic for this :)

view this post on Zulip Ken Lee (Dec 23 2020 at 17:08):

Yes!

view this post on Zulip Bhavik Mehta (Dec 23 2020 at 17:08):

(in mathlib soon :) )

view this post on Zulip Adam Topaz (Dec 23 2020 at 17:08):

:congratulations:

view this post on Zulip Bhavik Mehta (Dec 23 2020 at 21:11):

This is #5485

view this post on Zulip Kevin Buzzard (Dec 24 2020 at 15:15):

Adam Topaz said:

I don't know the answer, but I wish we had a tactic for this :)

This is yet another point for Mario. He has long argued that a lot of the time we want to transfer stuff along some notion of "the same", there is a more general theorem which transfers stuff along a weaker notion which is reflexive and transitive but not symmetric, and which should not be proved by a tactic. For example when I said "a machine should prove that if top spaces X and Y are homeomorphic, and X is compact, then Y is compact", and Mario said "no. A human should notice, and prove in the API, that if X surjects onto Y and X is compact then Y is compact, and the translation along a homeo is a trivial special case". The same is true here. Ken has actually proved that if C -> D is a right adjoint and C is filtered then D is filtered, and deduces the result from this and the fact that equivalences (symmetric) are right adjoints (and this concept is not symmetric -- if there's a right adjoint from C to D there might not be a right adjoint from D to C).


Last updated: May 17 2021 at 16:26 UTC