Commit 2023-02-21 09:17 13138c85

View on Github →

feat: port CategoryTheory.Adjunction.Basic (#2198)

Estimated changes

Modified Mathlib.lean

Created Mathlib/CategoryTheory/Adjunction/Basic.lean

added theorem CategoryTheory.Adjunction.CoreHomEquiv.homEquiv_naturality_left

added theorem CategoryTheory.Adjunction.CoreHomEquiv.homEquiv_naturality_left_aux

added theorem CategoryTheory.Adjunction.CoreHomEquiv.homEquiv_naturality_right_symm

added theorem CategoryTheory.Adjunction.CoreHomEquiv.homEquiv_naturality_right_symm_aux

added structure CategoryTheory.Adjunction.CoreHomEquiv

added structure CategoryTheory.Adjunction.CoreUnitCounit

added def CategoryTheory.Adjunction.adjunctionOfEquivLeft

added def CategoryTheory.Adjunction.adjunctionOfEquivRight

added def CategoryTheory.Adjunction.comp

added theorem CategoryTheory.Adjunction.counit_naturality

added theorem CategoryTheory.Adjunction.eq_homEquiv_apply

added def CategoryTheory.Adjunction.equivHomsetLeftOfNatIso

added def CategoryTheory.Adjunction.equivHomsetRightOfNatIso

added theorem CategoryTheory.Adjunction.homEquiv_apply_eq

added theorem CategoryTheory.Adjunction.homEquiv_id

added theorem CategoryTheory.Adjunction.homEquiv_naturality_left

added theorem CategoryTheory.Adjunction.homEquiv_naturality_left_symm

added theorem CategoryTheory.Adjunction.homEquiv_naturality_right

added theorem CategoryTheory.Adjunction.homEquiv_naturality_right_symm

added theorem CategoryTheory.Adjunction.homEquiv_symm_id

added def CategoryTheory.Adjunction.id

added def CategoryTheory.Adjunction.leftAdjointOfEquiv

added def CategoryTheory.Adjunction.leftAdjointOfNatIso

added theorem CategoryTheory.Adjunction.left_triangle

added theorem CategoryTheory.Adjunction.left_triangle_components

added def CategoryTheory.Adjunction.mkOfHomEquiv

added def CategoryTheory.Adjunction.mkOfUnitCounit

added def CategoryTheory.Adjunction.ofLeftAdjoint

added def CategoryTheory.Adjunction.ofNatIsoLeft

added def CategoryTheory.Adjunction.ofNatIsoRight

added def CategoryTheory.Adjunction.ofRightAdjoint

added def CategoryTheory.Adjunction.rightAdjointOfEquiv

added def CategoryTheory.Adjunction.rightAdjointOfNatIso

added theorem CategoryTheory.Adjunction.right_triangle

added theorem CategoryTheory.Adjunction.right_triangle_components

added theorem CategoryTheory.Adjunction.unit_naturality

added structure CategoryTheory.Adjunction

added theorem CategoryTheory.Equivalence.asEquivalence_toAdjunction_counit

added theorem CategoryTheory.Equivalence.asEquivalence_toAdjunction_unit

added def CategoryTheory.Equivalence.toAdjunction

added def CategoryTheory.Functor.adjunction

added theorem CategoryTheory.Functor.leftAdjoint_of_isEquivalence

added theorem CategoryTheory.Functor.rightAdjoint_of_isEquivalence

added def CategoryTheory.leftAdjoint

added def CategoryTheory.rightAdjoint