[Merged by Bors] - feat(CategoryTheory/Adjunction): left adjoint is faithful iff unit is mono, etc.

[dagurtomas]

We prove the full Lemma 4.5.13 in Riehl's Category Theory in Context, characterizing when a left/right adjoint is full, resp. faithful, resp fully faithful in terms of the unit/counit being various types of epi/mono/iso. Earlier we only had the statements for fully faithful functors.

---

This can be used to show that the functor from topological spaces to condensed sets is faithful, see #14455

[github-actions]

PR summary 5d53958806

Import changes for modified files

Dependency changes

File	Base Count	Head Count	Change
Mathlib.CategoryTheory.Adjunction.FullyFaithful	366	363	-3 (-0.82%)

Import changes for all files

Files	Import difference
20 files Mathlib.CategoryTheory.Monoidal.Center Mathlib.CategoryTheory.Monoidal.CoherenceLemmas Mathlib.CategoryTheory.Monoidal.Free.Basic Mathlib.CategoryTheory.Bicategory.SingleObj Mathlib.CategoryTheory.Monoidal.Functorial Mathlib.CategoryTheory.Monoidal.End Mathlib.CategoryTheory.Monoidal.FunctorCategory Mathlib.CategoryTheory.Monoidal.Transport Mathlib.CategoryTheory.Monoidal.Opposite Mathlib.CategoryTheory.Monoidal.Braided.Opposite Mathlib.CategoryTheory.Monoidal.Functor Mathlib.CategoryTheory.Monoidal.NaturalTransformation Mathlib.CategoryTheory.Adjunction.FullyFaithful Mathlib.CategoryTheory.Monoidal.Braided.Basic Mathlib.CategoryTheory.Monad.Adjunction Mathlib.CategoryTheory.Monoidal.Discrete Mathlib.Tactic.CategoryTheory.Coherence Mathlib.CategoryTheory.Adjunction.Reflective Mathlib.CategoryTheory.Monoidal.Free.Coherence Mathlib.CategoryTheory.Bicategory.Adjunction	-3
5 files Mathlib.CategoryTheory.Monoidal.Skeleton Mathlib.CategoryTheory.Localization.Adjunction Mathlib.Mathport.Syntax Mathlib.Tactic Mathlib.CategoryTheory.Localization.Bousfield	-2

---

Declarations diff

+ counitSplitMonoOfRFull
+ counit_epi_of_R_faithful
+ counit_isSplitMono_of_R_full
+ faithful_L_of_mono_unit_app
+ faithful_R_of_epi_counit_app
+ full_L_of_isSplitEpi_unit_app
+ full_R_of_isSplitMono_counit_app
+ instance [L.Full] [L.Faithful] (X : C) : IsIso (h.unit.app X)
+ instance [R.Full] [R.Faithful] (X : D) : IsIso (h.counit.app X)
+ unitSplitEpiOfLFull
+ unit_isSplitEpi_of_L_full
+ unit_mono_of_L_faithful

You can run this locally as follows

## summary with just the declaration names:
./scripts/no_lost_declarations.sh short <optional_commit>

## more verbose report:
./scripts/no_lost_declarations.sh <optional_commit>

[dagurtomas]

Thanks for the review!

[b-mehta]

bors merge

[mathlib-bors]

Pull request successfully merged into master.

Build succeeded:

• Build
• Lint style