Currently, both Equivalences.CompositesAndInverses and Equivalences.FullyFaithful each have a lemma about fully faithfulness and one about essentially surjectiveness, which should be grouped together and one should be derived from the other:
FullyFaithful.fully_faithful_from_equivalence
: ∏ (A B : category) (F : A ⟶ B),
adj_equivalence_of_cats F → fully_faithful F
CompositesAndInverses.right_adj_equiv_is_ff
: ∏ (D1 D2 : category) (F : D1 ⟶ D2) (GG : adj_equivalence_of_cats F),
fully_faithful (Core.right_adjoint GG)
FullyFaithful.functor_from_equivalence_is_essentially_surjective
: ∏ (A B : category) (F : A ⟶ B),
adj_equivalence_of_cats F → essentially_surjective F
CompositesAndInverses.right_adj_equiv_is_ess_sur
: ∏ (D1 D2 : category) (F : D1 ⟶ D2) (GG : adj_equivalence_of_cats F),
essentially_surjective (Core.right_adjoint GG)Also, we have adj_equivalence_of_cats_inv both in Adjunctions.Core and Adjunctions.CompositesAndInverses. As long as we have a file CompositesAndInverses, it makes most sense to have the lemma there, but the one in Core is a one-line definition because Core already provides a lot of machinery for constructing equivalences in multiple different ways.
Currently, both
Equivalences.CompositesAndInversesandEquivalences.FullyFaithfuleach have a lemma about fully faithfulness and one about essentially surjectiveness, which should be grouped together and one should be derived from the other:FullyFaithful.fully_faithful_from_equivalence : ∏ (A B : category) (F : A ⟶ B), adj_equivalence_of_cats F → fully_faithful F CompositesAndInverses.right_adj_equiv_is_ff : ∏ (D1 D2 : category) (F : D1 ⟶ D2) (GG : adj_equivalence_of_cats F), fully_faithful (Core.right_adjoint GG) FullyFaithful.functor_from_equivalence_is_essentially_surjective : ∏ (A B : category) (F : A ⟶ B), adj_equivalence_of_cats F → essentially_surjective F CompositesAndInverses.right_adj_equiv_is_ess_sur : ∏ (D1 D2 : category) (F : D1 ⟶ D2) (GG : adj_equivalence_of_cats F), essentially_surjective (Core.right_adjoint GG)Also, we have
adj_equivalence_of_cats_invboth inAdjunctions.CoreandAdjunctions.CompositesAndInverses. As long as we have a fileCompositesAndInverses, it makes most sense to have the lemma there, but the one inCoreis a one-line definition becauseCorealready provides a lot of machinery for constructing equivalences in multiple different ways.