Filtered category equivalence

Stream: Is there code for X?

[Bhavik Mehta]

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

[Adam Topaz]

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

[Ken Lee]

Yes!

[Bhavik Mehta]

(in mathlib soon :) )

[Adam Topaz]

:congratulations:

[Bhavik Mehta]

This is #5485

[Kevin Buzzard]

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).