Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2019-07-05 15:44 05550eac

View on Github →

feat(category_theory/limits): equivalences create limits (#1175)

feat(category_theory/limits): equivalences create limits
equivalence lemma
add @[simp]
use right_adjoint_preserves_limits
undo weird changes in topology files
formatting
do colimits too

Estimated changes

Modified src/category_theory/adjunction/basic.lean

deleted def category_theory.adjunction.equivalence.to_adjunction

added def category_theory.equivalence.to_adjunction

added def category_theory.functor.adjunction

Modified src/category_theory/adjunction/limits.lean

added def category_theory.adjunction.has_colimit_of_comp_equivalence

added def category_theory.adjunction.has_limit_of_comp_equivalence

added def category_theory.adjunction.is_colimit_map_cocone

added def category_theory.adjunction.is_limit_map_cone

deleted def category_theory.adjunction.left_adjoint_preserves_colimits

deleted def category_theory.adjunction.right_adjoint_preserves_limits

Modified src/category_theory/equivalence.lean

modified theorem category_theory.equivalence.counit_inv_functor_comp

modified theorem category_theory.equivalence.functor_unit_comp

modified theorem category_theory.equivalence.inverse_counit_inv_comp

modified theorem category_theory.equivalence.unit_inverse_comp

added theorem category_theory.is_equivalence.counit_inv_functor_comp

added theorem category_theory.is_equivalence.functor_unit_comp

Modified src/category_theory/limits/cones.lean

added theorem category_theory.functor.map_cocone_X

added theorem category_theory.functor.map_cone_X

added def category_theory.functor.map_cone_inv

added theorem category_theory.functor.map_cone_inv_X

Modified src/category_theory/limits/limits.lean