Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2020-03-11 22:56 7c8dc2ad

View on Github →

feat(category_theory/limits): construct equalizers from pullbacks and products (#2124)

construct equalizers from pullbacks and products
...
changes from review
Add docstrings
golf proofs a little
linter

Estimated changes

Modified src/category_theory/category/default.lean

added theorem category_theory.eq_whisker

added theorem category_theory.whisker_eq

Created src/category_theory/limits/shapes/constructions/equalizers.lean

added def category_theory.limits.has_equalizers_of_pullbacks_and_binary_products.construct_equalizer

added def category_theory.limits.has_equalizers_of_pullbacks_and_binary_products.equalizer_cone

added def category_theory.limits.has_equalizers_of_pullbacks_and_binary_products.equalizer_cone_is_limit

added def category_theory.limits.has_equalizers_of_pullbacks_and_binary_products.pullback_fst

added theorem category_theory.limits.has_equalizers_of_pullbacks_and_binary_products.pullback_fst_eq_pullback_snd

added def category_theory.limits.has_equalizers_of_pullbacks_and_binary_products