Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2020-05-24 15:07 292fc042

View on Github →

feat(category_theory): adjunction convenience defs (#2754) Transport adjunctions along natural isomorphisms, and is_left_adjoint or is_right_adjoint versions of existing adjunction properties.

Estimated changes

Modified src/category_theory/adjunction/basic.lean

added def category_theory.adjunction.equiv_homset_left_of_nat_iso

added theorem category_theory.adjunction.equiv_homset_left_of_nat_iso_apply

added theorem category_theory.adjunction.equiv_homset_left_of_nat_iso_symm_apply

added def category_theory.adjunction.equiv_homset_right_of_nat_iso

added theorem category_theory.adjunction.equiv_homset_right_of_nat_iso_apply

added theorem category_theory.adjunction.equiv_homset_right_of_nat_iso_symm_apply

added def category_theory.adjunction.left_adjoint_of_nat_iso

added def category_theory.adjunction.of_nat_iso_left

added def category_theory.adjunction.of_nat_iso_right

added def category_theory.adjunction.right_adjoint_of_nat_iso