Commit 2025-10-25 11:48 aa1b475d

View on Github →

feat(CategoryTheory/Adjunction/PartialAdjunction): add symm naturality lemmas for HomEquiv and lift functor (#30143) Add two lemmas for partialRightAdjointHomEquiv to help work with partialRightAdjointHomEquiv.symm.

Estimated changes

Modified Mathlib/CategoryTheory/Adjunction/PartialAdjoint.lean

added theorem CategoryTheory.Functor.partialLeftAdjointHomEquiv_comp_symm

added theorem CategoryTheory.Functor.partialLeftAdjointHomEquiv_symm_comp

added theorem CategoryTheory.Functor.partialRightAdjointHomEquiv_comp_symm

added theorem CategoryTheory.Functor.partialRightAdjointHomEquiv_symm_comp