Commit 2023-02-11 09:23 e0f1859a

View on Github →

feat: port CategoryTheory.Equivalence (#1287) This is missing slice_lhs which is only used in two proofs though. Update: slice_lhs (and other slice tactics) have now been ported

Estimated changes

Modified Mathlib.lean

Created Mathlib/CategoryTheory/Equivalence.lean

added theorem CategoryTheory.Equivalence.Equivalence_mk'_counit

added theorem CategoryTheory.Equivalence.Equivalence_mk'_counitInv

added theorem CategoryTheory.Equivalence.Equivalence_mk'_unit

added theorem CategoryTheory.Equivalence.Equivalence_mk'_unitInv

added theorem CategoryTheory.Equivalence.adjointify_η_ε

added def CategoryTheory.Equivalence.adjointifyη

added theorem CategoryTheory.Equivalence.cancel_counitInv_right

added theorem CategoryTheory.Equivalence.cancel_counitInv_right_assoc'

added theorem CategoryTheory.Equivalence.cancel_counitInv_right_assoc

added theorem CategoryTheory.Equivalence.cancel_counit_right

added theorem CategoryTheory.Equivalence.cancel_unitInv_right

added theorem CategoryTheory.Equivalence.cancel_unit_right

added theorem CategoryTheory.Equivalence.cancel_unit_right_assoc'

added theorem CategoryTheory.Equivalence.cancel_unit_right_assoc

added def CategoryTheory.Equivalence.congrLeft

added def CategoryTheory.Equivalence.congrRight

added theorem CategoryTheory.Equivalence.counitInv_app_functor

added theorem CategoryTheory.Equivalence.counitInv_functor_comp

added theorem CategoryTheory.Equivalence.counit_app_functor

added theorem CategoryTheory.Equivalence.ess_surj_of_equivalence

added def CategoryTheory.Equivalence.funInvIdAssoc

added theorem CategoryTheory.Equivalence.funInvIdAssoc_hom_app

added theorem CategoryTheory.Equivalence.funInvIdAssoc_inv_app

added theorem CategoryTheory.Equivalence.fun_inv_map

added theorem CategoryTheory.Equivalence.functor_asEquivalence

added theorem CategoryTheory.Equivalence.functor_inv

added theorem CategoryTheory.Equivalence.functor_map_inj_iff

added theorem CategoryTheory.Equivalence.functor_unit_comp

added def CategoryTheory.Equivalence.invFunIdAssoc

added theorem CategoryTheory.Equivalence.invFunIdAssoc_hom_app

added theorem CategoryTheory.Equivalence.invFunIdAssoc_inv_app

added theorem CategoryTheory.Equivalence.inv_fun_map

added theorem CategoryTheory.Equivalence.inverse_asEquivalence

added theorem CategoryTheory.Equivalence.inverse_counitInv_comp

added theorem CategoryTheory.Equivalence.inverse_inv

added theorem CategoryTheory.Equivalence.inverse_map_inj_iff

added def CategoryTheory.Equivalence.pow

added def CategoryTheory.Equivalence.powNat

added theorem CategoryTheory.Equivalence.pow_neg_one

added theorem CategoryTheory.Equivalence.pow_one

added theorem CategoryTheory.Equivalence.pow_zero

added def CategoryTheory.Equivalence.refl

added def CategoryTheory.Equivalence.symm

added def CategoryTheory.Equivalence.trans

added theorem CategoryTheory.Equivalence.unitInv_app_inverse

added theorem CategoryTheory.Equivalence.unit_app_inverse

added theorem CategoryTheory.Equivalence.unit_inverse_comp

added structure CategoryTheory.Equivalence

added def CategoryTheory.Functor.asEquivalence

added theorem CategoryTheory.Functor.asEquivalence_counit

added theorem CategoryTheory.Functor.asEquivalence_functor

added theorem CategoryTheory.Functor.asEquivalence_inverse

added theorem CategoryTheory.Functor.asEquivalence_unit

added def CategoryTheory.Functor.inv

added theorem CategoryTheory.Functor.inv_inv

added def CategoryTheory.IsEquivalence.cancelCompLeft

added def CategoryTheory.IsEquivalence.cancelCompRight

added def CategoryTheory.IsEquivalence.equivOfIso

added theorem CategoryTheory.IsEquivalence.fun_inv_map

added theorem CategoryTheory.IsEquivalence.inv_fun_map

added def CategoryTheory.IsEquivalence.ofIso

added theorem CategoryTheory.IsEquivalence.ofIso_refl

added theorem CategoryTheory.IsEquivalence.ofIso_trans

Modified Mathlib/CategoryTheory/Iso.lean