Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2020-03-06 09:04 8fb9881a

View on Github →

fix(category_theory/limits): Add some missing instances for special shapes of limits (#2083)

Add some instances for limit shapes
Deduce has_(equalizers|kernels|pullbacks) from has_finite_limits

Estimated changes

Modified src/category_theory/limits/shapes/equalizers.lean

added def category_theory.limits.has_coequalizers_of_has_finite_colimits

added def category_theory.limits.has_equalizers_of_has_finite_limits

modified inductive category_theory.limits.walking_parallel_pair_hom

Modified src/category_theory/limits/shapes/kernels.lean

added def category_theory.limits.has_cokernels_of_has_finite_colimits

added def category_theory.limits.has_kernels_of_has_finite_limits

Modified src/category_theory/limits/shapes/pullbacks.lean

added def category_theory.limits.has_pullbacks_of_has_finite_limits

added def category_theory.limits.has_pushouts_of_has_finite_colimits

modified inductive category_theory.limits.walking_cospan.hom

modified inductive category_theory.limits.walking_span.hom