Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2021-12-30 14:54 7b1c7751

View on Github →

chore(category_theory/adjunction/limits): generalize universe (#11070)

Estimated changes

Modified src/category_theory/adjunction/limits.lean

modified def category_theory.adjunction.cocones_iso

modified def category_theory.adjunction.cocones_iso_component_hom

modified def category_theory.adjunction.cocones_iso_component_inv

modified def category_theory.adjunction.cones_iso

modified def category_theory.adjunction.cones_iso_component_hom

modified def category_theory.adjunction.cones_iso_component_inv

modified theorem category_theory.adjunction.has_colimits_of_equivalence

modified theorem category_theory.adjunction.has_limits_of_equivalence

modified def category_theory.adjunction.left_adjoint_preserves_colimits

modified def category_theory.adjunction.right_adjoint_preserves_limits

Modified src/category_theory/closed/ideal.lean

Modified src/category_theory/limits/cone_category.lean

Modified src/category_theory/limits/has_limits.lean

added theorem category_theory.limits.has_colimits.has_colimits_of_shape

deleted theorem category_theory.limits.has_colimits.has_limits_of_shape

Modified src/category_theory/limits/preserves/shapes/terminal.lean

modified theorem category_theory.limits.has_initial_of_has_initial_of_preserves_colimit

modified theorem category_theory.limits.has_terminal_of_has_terminal_of_preserves_limit

modified def category_theory.limits.is_colimit_of_has_initial_of_preserves_colimit

modified def category_theory.limits.is_initial.is_initial_obj

modified def category_theory.limits.is_initial.is_initial_of_obj

modified def category_theory.limits.is_limit_of_has_terminal_of_preserves_limit

modified def category_theory.limits.is_terminal.is_terminal_obj

modified def category_theory.limits.is_terminal.is_terminal_of_obj

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

modified def category_theory.limits.as_empty_cocone

modified def category_theory.limits.as_empty_cone

modified def category_theory.limits.has_initial

added theorem category_theory.limits.has_initial_change_diagram

added theorem category_theory.limits.has_initial_change_universe

modified def category_theory.limits.has_terminal

added theorem category_theory.limits.has_terminal_change_diagram

added theorem category_theory.limits.has_terminal_change_universe

modified def category_theory.limits.initial

added def category_theory.limits.is_colimit_change_empty_cocone

added def category_theory.limits.is_colimit_empty_cocone_equiv

modified def category_theory.limits.is_initial

added def category_theory.limits.is_limit_change_empty_cone

added def category_theory.limits.is_limit_empty_cone_equiv

modified def category_theory.limits.is_terminal

modified def category_theory.limits.terminal

Modified src/category_theory/monad/limits.lean

modified theorem category_theory.has_colimits_of_reflective

modified theorem category_theory.has_limits_of_reflective

Modified src/category_theory/monoidal/of_chosen_finite_products.lean

modified def category_theory.limits.binary_fan.left_unitor

modified def category_theory.limits.binary_fan.right_unitor

Modified src/category_theory/pempty.lean

modified def category_theory.functor.empty

added def category_theory.functor.empty_equivalence

modified theorem category_theory.functor.empty_ext'

modified def category_theory.functor.empty_ext

modified def category_theory.functor.unique_from_empty