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 : \mathcal{A} \to \mathcal{B}$ be a fully faithful functor. Suppose for every $X \in Ob(\mathcal{B})$ given an object $j(X)$ of $\mathcal{A}$ and an isomorphism $i_X : X \to F(j(X))$. Then there is a unique functor $j : \mathcal{B} \to \mathcal{A}$ such that $j$ extends the rule on objects, and the isomorphisms $i_X$ define an isomorphism of functors $\text{id}_\mathcal{B} \to F \circ j$. Moreover, $j$ and $F$ 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: May 11 2021 at 00:31 UTC