Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2020-06-25 13:06 80a08778

View on Github →

feat(category_theory): show a pullback of a regular mono is regular (#2780) And adds two methods for constructing limits which I've found much easier to use in practice.

Estimated changes

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

added def category_theory.limits.cofork.is_colimit.mk'

added def category_theory.limits.fork.is_limit.mk'

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

added def category_theory.limits.pullback_cone.flip_is_limit

added def category_theory.limits.pullback_cone.is_limit.mk'

added def category_theory.limits.pushout_cocone.flip_is_colimit

added def category_theory.limits.pushout_cocone.is_colimit.mk'

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

added def category_theory.normal_of_is_pullback_fst_of_normal

added def category_theory.normal_of_is_pullback_snd_of_normal

added def category_theory.normal_of_is_pushout_fst_of_normal

added def category_theory.normal_of_is_pushout_snd_of_normal

added def category_theory.regular_of_is_pullback_fst_of_regular

added def category_theory.regular_of_is_pullback_snd_of_regular

added def category_theory.regular_of_is_pushout_fst_of_regular

added def category_theory.regular_of_is_pushout_snd_of_regular