Commit 2022-02-24 03:44 f3ee4628

View on Github →

chore(category_theory/adjunction/opposites): Forgotten category_theory namespace (#12256) The forgotten category_theory namespace means that dot notation doesn't work on category_theory.adjunction.

Estimated changes

Modified src/category_theory/adjunction/opposites.lean

deleted def adjunction.adjoint_of_op_adjoint_op

deleted def adjunction.adjoint_of_unop_adjoint_unop

deleted def adjunction.adjoint_op_of_adjoint_unop

deleted def adjunction.adjoint_unop_of_adjoint_op

deleted theorem adjunction.hom_equiv_left_adjoint_uniq_hom_app

deleted theorem adjunction.hom_equiv_symm_right_adjoint_uniq_hom_app

deleted def adjunction.left_adjoint_uniq

deleted theorem adjunction.left_adjoint_uniq_hom_app_counit

deleted theorem adjunction.left_adjoint_uniq_hom_counit

deleted theorem adjunction.left_adjoint_uniq_inv_app

deleted theorem adjunction.left_adjoint_uniq_refl

deleted theorem adjunction.left_adjoint_uniq_trans

deleted theorem adjunction.left_adjoint_uniq_trans_app

deleted def adjunction.left_adjoints_coyoneda_equiv

deleted def adjunction.nat_iso_of_left_adjoint_nat_iso

deleted def adjunction.nat_iso_of_right_adjoint_nat_iso

deleted def adjunction.op_adjoint_of_unop_adjoint

deleted def adjunction.op_adjoint_op_of_adjoint

deleted def adjunction.right_adjoint_uniq

deleted theorem adjunction.right_adjoint_uniq_hom_app_counit

deleted theorem adjunction.right_adjoint_uniq_hom_counit

deleted theorem adjunction.right_adjoint_uniq_inv_app

deleted theorem adjunction.right_adjoint_uniq_refl

deleted theorem adjunction.right_adjoint_uniq_trans

deleted theorem adjunction.right_adjoint_uniq_trans_app

deleted theorem adjunction.unit_left_adjoint_uniq_hom

deleted theorem adjunction.unit_left_adjoint_uniq_hom_app

deleted theorem adjunction.unit_right_adjoint_uniq_hom

deleted theorem adjunction.unit_right_adjoint_uniq_hom_app

deleted def adjunction.unop_adjoint_of_op_adjoint

deleted def adjunction.unop_adjoint_unop_of_adjoint

added def category_theory.adjunction.adjoint_of_op_adjoint_op

added def category_theory.adjunction.adjoint_of_unop_adjoint_unop

added def category_theory.adjunction.adjoint_op_of_adjoint_unop

added def category_theory.adjunction.adjoint_unop_of_adjoint_op

added theorem category_theory.adjunction.hom_equiv_left_adjoint_uniq_hom_app

added theorem category_theory.adjunction.hom_equiv_symm_right_adjoint_uniq_hom_app

added def category_theory.adjunction.left_adjoint_uniq

added theorem category_theory.adjunction.left_adjoint_uniq_hom_app_counit

added theorem category_theory.adjunction.left_adjoint_uniq_hom_counit

added theorem category_theory.adjunction.left_adjoint_uniq_inv_app

added theorem category_theory.adjunction.left_adjoint_uniq_refl

added theorem category_theory.adjunction.left_adjoint_uniq_trans

added theorem category_theory.adjunction.left_adjoint_uniq_trans_app

added def category_theory.adjunction.left_adjoints_coyoneda_equiv

added def category_theory.adjunction.nat_iso_of_left_adjoint_nat_iso

added def category_theory.adjunction.nat_iso_of_right_adjoint_nat_iso

added def category_theory.adjunction.op_adjoint_of_unop_adjoint

added def category_theory.adjunction.op_adjoint_op_of_adjoint

added def category_theory.adjunction.right_adjoint_uniq

added theorem category_theory.adjunction.right_adjoint_uniq_hom_app_counit

added theorem category_theory.adjunction.right_adjoint_uniq_hom_counit

added theorem category_theory.adjunction.right_adjoint_uniq_inv_app

added theorem category_theory.adjunction.right_adjoint_uniq_refl

added theorem category_theory.adjunction.right_adjoint_uniq_trans

added theorem category_theory.adjunction.right_adjoint_uniq_trans_app

added theorem category_theory.adjunction.unit_left_adjoint_uniq_hom

added theorem category_theory.adjunction.unit_left_adjoint_uniq_hom_app

added theorem category_theory.adjunction.unit_right_adjoint_uniq_hom

added theorem category_theory.adjunction.unit_right_adjoint_uniq_hom_app

added def category_theory.adjunction.unop_adjoint_of_op_adjoint

added def category_theory.adjunction.unop_adjoint_unop_of_adjoint