Commit 2025-07-31 04:45 4907ae44

View on Github →

feat(CategoryTheory/Adjunction): more results on adjoint triples. (#27650) Lemmas about adjoint triples F ⊣ G ⊣ H where either G is fully faithful or F and H are.

Estimated changes

Modified Mathlib/CategoryTheory/Adjunction/Triple.lean

added theorem CategoryTheory.Adjunction.Triple.adj₁_counit_app_rightToLeft_app

added theorem CategoryTheory.Adjunction.Triple.epi_rightToLeft_app_iff

added theorem CategoryTheory.Adjunction.Triple.epi_rightToLeft_app_iff_epi_map_adj₁_unit_app

added theorem CategoryTheory.Adjunction.Triple.epi_rightToLeft_app_iff_epi_map_adj₂_counit_app

added theorem CategoryTheory.Adjunction.Triple.isIso_unit_iff_isIso_counit

added theorem CategoryTheory.Adjunction.Triple.leftToRight_app

added theorem CategoryTheory.Adjunction.Triple.leftToRight_app_map_adj₁_unit_app

added theorem CategoryTheory.Adjunction.Triple.leftToRight_app_obj

added theorem CategoryTheory.Adjunction.Triple.leftToRight_eq_counits

added theorem CategoryTheory.Adjunction.Triple.map_adj₂_counit_app_leftToRight_app

added theorem CategoryTheory.Adjunction.Triple.map_rightToLeft_app

added theorem CategoryTheory.Adjunction.Triple.mono_leftToRight_app_iff

added theorem CategoryTheory.Adjunction.Triple.mono_leftToRight_app_iff_mono_adj₁_counit_app

added theorem CategoryTheory.Adjunction.Triple.mono_leftToRight_app_iff_mono_adj₂_unit_app

added theorem CategoryTheory.Adjunction.Triple.rightToLeft_app_adj₂_unit_app

added theorem CategoryTheory.Adjunction.Triple.rightToLeft_eq_counits

added theorem CategoryTheory.Adjunction.Triple.rightToLeft_eq_units

added theorem CategoryTheory.Adjunction.Triple.whiskerLeft_leftToRight

added theorem CategoryTheory.Adjunction.Triple.whiskerRight_rightToLeft

added structure CategoryTheory.Adjunction.Triple

deleted theorem CategoryTheory.Adjunction.isIso_unit_iff_isIso_counit

Modified Mathlib/CategoryTheory/EpiMono.lean

added theorem CategoryTheory.epi_comp_iff_of_epi

added theorem CategoryTheory.epi_comp_iff_of_isIso

added theorem CategoryTheory.mono_comp_iff_of_isIso

added theorem CategoryTheory.mono_comp_iff_of_mono