Commit 2024-10-27 10:17 7e4aaba2

View on Github →

feat(CategoryTheory/Monoidal): Day's reflection theorem (#15894)

Estimated changes

Modified Mathlib.lean

Modified Mathlib/CategoryTheory/Monad/Basic.lean

added theorem CategoryTheory.Comonad.isSplitEpi_iff_isIso_counit

added theorem CategoryTheory.Comonad.map_counit_app

added theorem CategoryTheory.Monad.isSplitMono_iff_isIso_unit

added theorem CategoryTheory.Monad.map_unit_app

Created Mathlib/CategoryTheory/Monoidal/Braided/Reflection.lean

added theorem CategoryTheory.Monoidal.Reflective.isIso_tfae

Modified Mathlib/CategoryTheory/Yoneda.lean

added theorem CategoryTheory.isIso_iff_coyoneda_map_bijective

added theorem CategoryTheory.isIso_iff_isIso_coyoneda_map

added theorem CategoryTheory.isIso_iff_isIso_yoneda_map

added theorem CategoryTheory.isIso_iff_yoneda_map_bijective

Modified docs/references.bib