Commit 2026-03-12 08:06 3024fb6d

View on Github →

chore(CategoryTheory/Adjunction): fix Adjunction.ofNatIsoLeft to not use Adjunction.mkOfHomEquiv (#36493) This gives the correct def-eqs for the unit and counit.

Estimated changes

Modified Mathlib/CategoryTheory/Adjunction/Basic.lean

added theorem CategoryTheory.Adjunction.homEquiv_ofNatIsoLeft_apply

added theorem CategoryTheory.Adjunction.homEquiv_ofNatIsoLeft_symm_apply

added theorem CategoryTheory.Adjunction.homEquiv_ofNatIsoRight_apply

added theorem CategoryTheory.Adjunction.homEquiv_ofNatIsoRight_symm_apply

modified def CategoryTheory.Adjunction.ofNatIsoLeft

modified def CategoryTheory.Adjunction.ofNatIsoRight

Modified Mathlib/CategoryTheory/Monoidal/Closed/Basic.lean

Modified Mathlib/RepresentationTheory/FiniteIndex.lean