Do adjunctions CC -| Discrete -| Objects already exists ?

Stream: mathlib4

[Nicolas Rolland]

I have some code about some easy adjunctions and wanted to make sure that it wasn't already somewhere in the library

Discrete : Type => Cat -| Type <= Cat : Objects
Connected components : Type <= Cat -| Discrete : Type => Cat

I didn't see it in obvious files, in the list of IsRightAdjoint or IsLeftAdjoint

Do you confirm it's not already in there ?
Is there a more systematic way to check that ?

[Kim Morrison]

I don't recall seeing these.

For statements like this where there aren't to many ways to state it, using import Mathlib, starting the result, and then by exact? can be a useful way to check.

[Kim Morrison]

Asking moogle.ai is often surprisingly successful.

[Kim Morrison]

You can also grep (just via the VSCode search interface) for the adjunction symbol and Discrete on the same line.

[Kim Morrison]

Or use Loogle for the same effect!

[Kim Morrison]

(Despite the arrival of all these new search tools I admit I still use grep. :-)

[Yaël Dillies]

Me too :innocent:

[Nicolas Rolland]

Good to know, a new PR incoming soon then !

Those basic functors/properties can be very useful
For instance, given P : C -> Set, we have that colim (P) = CC(P.Elements) because

Set (CC(P.Elements), X) = Cat (P.Elements, discrete X ) = [C,Set] (P, constant X)

A very short proof which begs to be in Lean :)