Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2021-12-13 07:53 7cd8adb7

View on Github →

chore(category_theory/limits): Generalize universe for preserving limits (#10736)

Estimated changes

Modified src/category_theory/closed/functor.lean

Modified src/category_theory/closed/ideal.lean

Modified src/category_theory/limits/comma.lean

Modified src/category_theory/limits/constructions/finite_products_of_binary_products.lean

Modified src/category_theory/limits/constructions/limits_of_products_and_equalizers.lean

Modified src/category_theory/limits/creates.lean

added def category_theory.creates_colimits

modified def category_theory.creates_colimits_of_nat_iso

added def category_theory.creates_limits

modified def category_theory.creates_limits_of_nat_iso

modified theorem category_theory.has_colimits_of_has_colimits_creates_colimits

modified theorem category_theory.has_limits_of_has_limits_creates_limits

Modified src/category_theory/limits/functor_category.lean

Modified src/category_theory/limits/preserves/basic.lean

modified def category_theory.limits.fully_faithful_reflects_colimits

modified def category_theory.limits.fully_faithful_reflects_limits

added def category_theory.limits.preserves_colimits

modified def category_theory.limits.preserves_colimits_of_nat_iso

modified def category_theory.limits.preserves_colimits_of_reflects_of_preserves

modified def category_theory.limits.preserves_colimits_of_shape_of_equiv

added def category_theory.limits.preserves_limits

modified def category_theory.limits.preserves_limits_of_nat_iso

modified def category_theory.limits.preserves_limits_of_reflects_of_preserves

modified def category_theory.limits.preserves_limits_of_shape_of_equiv

added def category_theory.limits.reflects_colimits

modified def category_theory.limits.reflects_colimits_of_nat_iso

added def category_theory.limits.reflects_limits

modified def category_theory.limits.reflects_limits_of_nat_iso

Modified src/category_theory/limits/preserves/finite.lean

Modified src/category_theory/limits/preserves/functor_category.lean

Modified src/category_theory/monad/limits.lean

Modified src/category_theory/monad/monadicity.lean

Modified src/category_theory/sites/limits.lean

Modified src/category_theory/sites/sheaf.lean