Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2022-03-07 14:11 9ed43666

View on Github →

feat(category_theory/limits): limit preservation properties of functor.left_op and similar (#12168)

Estimated changes

Created src/category_theory/limits/preserves/opposites.lean

added def category_theory.limits.perserves_colimits_op

added def category_theory.limits.preserves_colimit_left_op

added def category_theory.limits.preserves_colimit_op

added def category_theory.limits.preserves_colimit_right_op

added def category_theory.limits.preserves_colimit_unop

added def category_theory.limits.preserves_colimits_left_op

added def category_theory.limits.preserves_colimits_of_shape_left_op

added def category_theory.limits.preserves_colimits_of_shape_op

added def category_theory.limits.preserves_colimits_of_shape_right_op

added def category_theory.limits.preserves_colimits_of_shape_unop

added def category_theory.limits.preserves_colimits_right_op

added def category_theory.limits.preserves_colimits_unop

added def category_theory.limits.preserves_finite_colimits_left_op

added def category_theory.limits.preserves_finite_colimits_op

added def category_theory.limits.preserves_finite_colimits_right_op

added def category_theory.limits.preserves_finite_colimits_unop

added def category_theory.limits.preserves_finite_limits_left_op

added def category_theory.limits.preserves_finite_limits_op

added def category_theory.limits.preserves_finite_limits_right_op

added def category_theory.limits.preserves_finite_limits_unop

added def category_theory.limits.preserves_limit_left_op

added def category_theory.limits.preserves_limit_op

added def category_theory.limits.preserves_limit_right_op

added def category_theory.limits.preserves_limit_unop

added def category_theory.limits.preserves_limits_left_op

added def category_theory.limits.preserves_limits_of_shape_left_op

added def category_theory.limits.preserves_limits_of_shape_op

added def category_theory.limits.preserves_limits_of_shape_right_op

added def category_theory.limits.preserves_limits_of_shape_unop

added def category_theory.limits.preserves_limits_op

added def category_theory.limits.preserves_limits_right_op

added def category_theory.limits.preserves_limits_unop