Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2021-11-26 11:04 36f33d0d

View on Github →

chore(category_theory/limits): Generalize universes for limits (#10243)

Estimated changes

Modified src/algebra/category/Algebra/limits.lean

modified def Algebra.has_limits.limit_cone

Modified src/algebra/category/CommRing/limits.lean

modified def SemiRing.has_limits.limit_cone

Modified src/algebra/category/Module/limits.lean

modified def Module.has_limits.limit_cone

Modified src/algebra/category/Mon/limits.lean

modified def Mon.has_limits.limit_cone

Modified src/category_theory/category/ulift.lean

deleted def category_theory.ulift.down

added def category_theory.ulift.down_functor

deleted def category_theory.ulift.up

added def category_theory.ulift.up_functor

added def category_theory.{v'

Modified src/category_theory/discrete_category.lean

modified def category_theory.discrete.equiv_of_equivalence

modified def category_theory.discrete.equivalence

Modified src/category_theory/fin_category.lean

added def category_theory.fin_category.as_type

added def category_theory.fin_category.obj_as_type

added def category_theory.fin_category.obj_as_type_equiv_as_type

Modified src/category_theory/graded_object.lean

Modified src/category_theory/is_connected.lean

Modified src/category_theory/limits/comma.lean

Modified src/category_theory/limits/cones.lean

modified def category_theory.cocones

modified def category_theory.cones

modified def category_theory.functor.cocones

modified def category_theory.functor.cones

modified def category_theory.limits.cocone.extensions

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

Modified src/category_theory/limits/creates.lean

Modified src/category_theory/limits/functor_category.lean

Modified src/category_theory/limits/has_limits.lean

modified def category_theory.limits.colim_coyoneda

modified def category_theory.limits.colimit.hom_iso

modified theorem category_theory.limits.colimit.hom_iso_hom

modified theorem category_theory.limits.colimit.map_post

modified theorem category_theory.limits.colimit.pre_post

modified theorem category_theory.limits.has_colimit.of_cocones_iso

added theorem category_theory.limits.has_colimits.has_limits_of_shape

added def category_theory.limits.has_colimits

modified theorem category_theory.limits.has_colimits_of_shape_of_equivalence

added theorem category_theory.limits.has_colimits_of_size_shrink

modified theorem category_theory.limits.has_limit.of_cones_iso

added theorem category_theory.limits.has_limits.has_limits_of_shape

added def category_theory.limits.has_limits

modified theorem category_theory.limits.has_limits_of_shape_of_equivalence

added theorem category_theory.limits.has_limits_of_size_shrink

modified def category_theory.limits.lim_yoneda

modified def category_theory.limits.limit.hom_iso

modified theorem category_theory.limits.limit.hom_iso_hom

modified theorem category_theory.limits.limit.map_post

modified theorem category_theory.limits.limit.pre_post

Modified src/category_theory/limits/is_limit.lean

modified def category_theory.limits.is_colimit.hom_iso

modified theorem category_theory.limits.is_colimit.hom_iso_hom

modified def category_theory.limits.is_colimit.map_cocone_equiv

modified def category_theory.limits.is_colimit.nat_iso

modified def category_theory.limits.is_colimit.of_cocone_equiv

modified theorem category_theory.limits.is_colimit.of_cocone_equiv_apply_desc

modified theorem category_theory.limits.is_colimit.of_cocone_equiv_symm_apply_desc

modified def category_theory.limits.is_colimit.of_faithful

modified def category_theory.limits.is_colimit.of_left_adjoint

modified def category_theory.limits.is_colimit.of_nat_iso.hom_of_cocone

modified def category_theory.limits.is_colimit.of_nat_iso

modified def category_theory.limits.is_limit.hom_iso

modified theorem category_theory.limits.is_limit.hom_iso_hom

modified def category_theory.limits.is_limit.map_cone_equiv

modified def category_theory.limits.is_limit.nat_iso

modified def category_theory.limits.is_limit.of_cone_equiv

modified theorem category_theory.limits.is_limit.of_cone_equiv_apply_desc

modified theorem category_theory.limits.is_limit.of_cone_equiv_symm_apply_desc

modified def category_theory.limits.is_limit.of_faithful

modified def category_theory.limits.is_limit.of_nat_iso.hom_of_cone

modified def category_theory.limits.is_limit.of_nat_iso

modified def category_theory.limits.is_limit.of_right_adjoint

Modified src/category_theory/limits/opposites.lean

modified theorem category_theory.limits.has_colimits_op_of_has_limits

modified theorem category_theory.limits.has_limits_op_of_has_colimits

Modified src/category_theory/limits/over.lean

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

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

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

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

Modified src/category_theory/limits/presheaf.lean

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

modified theorem category_theory.limits.coprod.map_comp_inl_inr_codiag

modified def category_theory.limits.has_binary_coproducts

modified def category_theory.limits.has_binary_products

modified def category_theory.limits.pair

modified theorem category_theory.limits.prod.diag_map_fst_snd_comp

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

modified def category_theory.limits.has_coequalizers

modified def category_theory.limits.has_equalizers

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

modified theorem category_theory.limits.has_finite_limits_of_has_limits

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

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

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

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

modified def category_theory.limits.has_pullbacks

modified def category_theory.limits.has_pushouts

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

modified def category_theory.limits.has_initial

modified def category_theory.limits.has_terminal

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

modified def category_theory.limits.has_wide_coequalizers

modified def category_theory.limits.has_wide_equalizers

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

Modified src/category_theory/monad/monadicity.lean

Modified src/category_theory/sites/limits.lean

Modified src/topology/category/Top/limits.lean

modified theorem Top.coequalizer_is_open_iff

Modified src/topology/sheaves/forget.lean

Modified src/topology/sheaves/sheaf_condition/sites.lean