Mathlib Changelog
v4
Changelog
About
Github
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