Commit 2023-02-22 17:44 2576ab9b

View on Github →

feat: port CategoryTheory.LiftingProperties.Adjunction (#2329)

Estimated changes

Modified Mathlib.lean

Created Mathlib/CategoryTheory/LiftingProperties/Adjunction.lean

added theorem CategoryTheory.Adjunction.hasLiftingProperty_iff

added def CategoryTheory.CommSq.leftAdjointLiftStructEquiv

added theorem CategoryTheory.CommSq.left_adjoint

added theorem CategoryTheory.CommSq.left_adjoint_hasLift_iff

added def CategoryTheory.CommSq.rightAdjointLiftStructEquiv

added theorem CategoryTheory.CommSq.right_adjoint

added theorem CategoryTheory.CommSq.right_adjoint_hasLift_iff