Commit 2023-03-28 22:14 b15c183f

View on Github →

feat: Port CategoryTheory.Adjunction.Opposites (#2424)

Estimated changes

Modified Mathlib.lean

Created Mathlib/CategoryTheory/Adjunction/Opposites.lean

added def CategoryTheory.Adjunction.adjointOfOpAdjointOp

added def CategoryTheory.Adjunction.adjointOfUnopAdjointUnop

added def CategoryTheory.Adjunction.adjointOpOfAdjointUnop

added def CategoryTheory.Adjunction.adjointUnopOfAdjointOp

added theorem CategoryTheory.Adjunction.homEquiv_leftAdjointUniq_hom_app

added theorem CategoryTheory.Adjunction.homEquiv_symm_rightAdjointUniq_hom_app

added def CategoryTheory.Adjunction.leftAdjointUniq

added theorem CategoryTheory.Adjunction.leftAdjointUniq_hom_app_counit

added theorem CategoryTheory.Adjunction.leftAdjointUniq_hom_counit

added theorem CategoryTheory.Adjunction.leftAdjointUniq_inv_app

added theorem CategoryTheory.Adjunction.leftAdjointUniq_refl

added theorem CategoryTheory.Adjunction.leftAdjointUniq_trans

added theorem CategoryTheory.Adjunction.leftAdjointUniq_trans_app

added def CategoryTheory.Adjunction.leftAdjointsCoyonedaEquiv

added def CategoryTheory.Adjunction.natIsoOfLeftAdjointNatIso

added def CategoryTheory.Adjunction.natIsoOfRightAdjointNatIso

added def CategoryTheory.Adjunction.opAdjointOfUnopAdjoint

added def CategoryTheory.Adjunction.opAdjointOpOfAdjoint

added def CategoryTheory.Adjunction.rightAdjointUniq

added theorem CategoryTheory.Adjunction.rightAdjointUniq_hom_app_counit

added theorem CategoryTheory.Adjunction.rightAdjointUniq_hom_counit

added theorem CategoryTheory.Adjunction.rightAdjointUniq_inv_app

added theorem CategoryTheory.Adjunction.rightAdjointUniq_refl

added theorem CategoryTheory.Adjunction.rightAdjointUniq_trans

added theorem CategoryTheory.Adjunction.rightAdjointUniq_trans_app

added theorem CategoryTheory.Adjunction.unit_leftAdjointUniq_hom

added theorem CategoryTheory.Adjunction.unit_leftAdjointUniq_hom_app

added theorem CategoryTheory.Adjunction.unit_rightAdjointUniq_hom

added theorem CategoryTheory.Adjunction.unit_rightAdjointUniq_hom_app

added def CategoryTheory.Adjunction.unopAdjointOfOpAdjoint

added def CategoryTheory.Adjunction.unopAdjointUnopOfAdjoint