Commit 2024-05-12 16:16 3fc1e3dd

View on Github →

refactor(CategoryTheory/Adjunction): make uniqueness of adjoints independent of opposites (#12625)

Estimated changes

Modified Mathlib.lean

Modified Mathlib/CategoryTheory/Adjunction/Opposites.lean

deleted theorem CategoryTheory.Adjunction.homEquiv_leftAdjointUniq_hom_app

deleted theorem CategoryTheory.Adjunction.homEquiv_symm_rightAdjointUniq_hom_app

deleted def CategoryTheory.Adjunction.leftAdjointUniq

deleted theorem CategoryTheory.Adjunction.leftAdjointUniq_hom_app_counit

deleted theorem CategoryTheory.Adjunction.leftAdjointUniq_hom_counit

deleted theorem CategoryTheory.Adjunction.leftAdjointUniq_inv_app

deleted theorem CategoryTheory.Adjunction.leftAdjointUniq_refl

deleted theorem CategoryTheory.Adjunction.leftAdjointUniq_trans

deleted theorem CategoryTheory.Adjunction.leftAdjointUniq_trans_app

deleted def CategoryTheory.Adjunction.rightAdjointUniq

deleted theorem CategoryTheory.Adjunction.rightAdjointUniq_hom_app_counit

deleted theorem CategoryTheory.Adjunction.rightAdjointUniq_hom_counit

deleted theorem CategoryTheory.Adjunction.rightAdjointUniq_inv_app

deleted theorem CategoryTheory.Adjunction.rightAdjointUniq_refl

deleted theorem CategoryTheory.Adjunction.rightAdjointUniq_trans

deleted theorem CategoryTheory.Adjunction.rightAdjointUniq_trans_app

deleted theorem CategoryTheory.Adjunction.unit_leftAdjointUniq_hom

deleted theorem CategoryTheory.Adjunction.unit_leftAdjointUniq_hom_app

deleted theorem CategoryTheory.Adjunction.unit_rightAdjointUniq_hom

deleted theorem CategoryTheory.Adjunction.unit_rightAdjointUniq_hom_app

Created Mathlib/CategoryTheory/Adjunction/Unique.lean

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.natIsoEquiv

added def CategoryTheory.Adjunction.natTransEquiv

added theorem CategoryTheory.Adjunction.natTransEquiv_comp

added theorem CategoryTheory.Adjunction.natTransEquiv_comp_symm

added theorem CategoryTheory.Adjunction.natTransEquiv_id

added theorem CategoryTheory.Adjunction.natTransEquiv_id_symm

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

Modified Mathlib/CategoryTheory/Limits/Over.lean

Modified Mathlib/CategoryTheory/Limits/Presheaf.lean

Modified Mathlib/CategoryTheory/Sites/CoverLifting.lean

Modified Mathlib/CategoryTheory/Sites/Sheafification.lean

Modified Mathlib/Order/Category/BddLat.lean

Modified Mathlib/Topology/Sheaves/Presheaf.lean