Commit 2025-08-31 11:17 b4980152

feat(CategoryTheory/Adjunction): lemmas on adjoint quadruples (#27720) Lemmas about adjoint quadruples L ⊣ F ⊣ G ⊣ R where some of the functors are fully faithful:

• If F and R are fully faithful, the components of the induced natural transformation G ⟶ L are epic iff the components of the natural transformation F ⟶ R are monic.
• If L and G are fully faithful, the components of the induced natural transformation L ⟶ G are epic iff the components of the natural transformation R ⟶ F are monic. A variant of the first case appears as proposition 2.7 on the nlab here; the second case is dual. From lean-orbifolds.