Commit 2024-08-30 13:02 b05a8650

View on Github →

feat(CategoryTheory/Adjunction): left adjoint in adjoint triple is fully faithful iff right adjoint is (#16167)

Estimated changes

Modified Mathlib.lean

Created Mathlib/CategoryTheory/Adjunction/Triple.lean

added theorem CategoryTheory.Adjunction.isIso_unit_iff_isIso_counit

Modified Mathlib/CategoryTheory/Functor/FullyFaithful.lean