Zulip Chat Archive

Stream: general

Topic: ultimate tactic

Patrick Massot (Feb 27 2018 at 18:24):

I found the ultimate Lean tactic: https://stacks.math.columbia.edu/tag/05SG

Patrick Massot (Feb 27 2018 at 18:24):

I think this is my new favorite Stacks tag

Sean Leather (Feb 27 2018 at 18:34):

Lemma 4.2.18. Let F:ABF : \mathcal{A} \to \mathcal{B} be a fully faithful functor. Suppose for every XOb(B)X \in Ob(\mathcal{B}) given an object j(X)j(X) of A\mathcal{A} and an isomorphism iX:XF(j(X))i_X : X \to F(j(X)). Then there is a unique functor j:BAj : \mathcal{B} \to \mathcal{A} such that jj extends the rule on objects, and the isomorphisms iXi_X define an isomorphism of functors idBFj\text{id}_\mathcal{B} \to F \circ j. Moreover, jj and FF are quasi-inverse equivalences of categories.

Proof. This lemma proves itself. \square

Simon Hudon (Feb 27 2018 at 18:49):

I think this recursive proof is not well founded :stuck_out_tongue:

Last updated: Aug 03 2023 at 10:10 UTC