Commit 2024-09-03 09:13 9ca5d4da

View on Github →

feat(CategoryTheory/Adjunction): dualize adjoint lifting theorem (#16066) This PR renames the file CategoryTheory.Adjunction.Lifting to CategoryTheory.Adjunction.Lifting.Left and dualizes it in a new file CategoryTheory.Adjunction.Lifting.Right to lift right adjoints through comonads. It also changes some names in the original file which didn't follow naming conventions, as well as renaming the implementation namespace.

Estimated changes

Modified Mathlib.lean

Renamed Mathlib/CategoryTheory/Adjunction/Lifting.lean to Mathlib/CategoryTheory/Adjunction/Lifting/Left.lean

deleted def CategoryTheory.LiftAdjoint.counitCoequalises

deleted def CategoryTheory.LiftAdjoint.otherMap

added def CategoryTheory.LiftLeftAdjoint.counitCoequalises

added def CategoryTheory.LiftLeftAdjoint.otherMap

deleted theorem CategoryTheory.adjointSquareLift

deleted theorem CategoryTheory.adjointTriangleLift

added theorem CategoryTheory.isRightAdjoint_square_lift

added theorem CategoryTheory.isRightAdjoint_square_lift_monadic

added theorem CategoryTheory.isRightAdjoint_triangle_lift

added theorem CategoryTheory.isRightAdjoint_triangle_lift_monadic

deleted theorem CategoryTheory.monadicAdjointSquareLift

deleted theorem CategoryTheory.monadicAdjointTriangleLift

Created Mathlib/CategoryTheory/Adjunction/Lifting/Right.lean

added def CategoryTheory.LiftRightAdjoint.otherMap

added def CategoryTheory.LiftRightAdjoint.unitEqualises

added theorem CategoryTheory.isLeftAdjoint_square_lift

added theorem CategoryTheory.isLeftAdjoint_square_lift_comonadic

added theorem CategoryTheory.isLeftAdjoint_triangle_lift

added theorem CategoryTheory.isLeftAdjoint_triangle_lift_comonadic