Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2020-06-30 04:15 1588d81e

View on Github →

feat(category_theory): remove nearly all universe annotations (#3221) Due to some recent changes to mathlib (does someone know the relevant versions/commits?) most of the universe annotations .{v} and include 𝒞 statements that were previously needed in the category_theory library are no longer necessary. This PR removes them!

Estimated changes

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

modified def category_theory.iso.to_alg_equiv

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

modified def CommRing.free

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

modified def category_theory.iso.CommRing_iso_to_ring_equiv

modified def category_theory.iso.Ring_iso_to_ring_equiv

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

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

modified def CommRing.CommRing_has_limits.limit

modified def CommRing.CommRing_has_limits.limit_is_limit

modified def CommRing.limit_π_ring_hom

Modified src/algebra/category/Group/adjunctions.lean

modified def AddCommGroup.free

Modified src/algebra/category/Group/basic.lean

modified def category_theory.iso.CommGroup_iso_to_mul_equiv

modified def category_theory.iso.Group_iso_to_mul_equiv

Modified src/algebra/category/Group/biproducts.lean

Modified src/algebra/category/Group/colimits.lean

Modified src/algebra/category/Group/images.lean

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

modified def AddCommGroup.AddCommGroup_has_limits.limit

modified def AddCommGroup.AddCommGroup_has_limits.limit_is_limit

modified def AddCommGroup.limit_π_add_monoid_hom

Modified src/algebra/category/Group/preadditive.lean

Modified src/algebra/category/Group/zero.lean

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

modified def category_theory.iso.to_linear_equiv

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

modified theorem Module.monoidal_category.left_unitor_hom

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

modified def category_theory.iso.CommMon_iso_to_mul_equiv

modified def category_theory.iso.Mon_iso_to_mul_equiv

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

Modified src/algebra/homology/chain_complex.lean

modified theorem chain_complex.d_squared

modified theorem cochain_complex.d_squared

Modified src/algebra/homology/homology.lean

modified def cochain_complex.cohomology_functor

modified def cochain_complex.cohomology_map

modified theorem cochain_complex.cohomology_map_comp

modified theorem cochain_complex.cohomology_map_condition

modified theorem cochain_complex.cohomology_map_id

modified def cochain_complex.image_map

modified theorem cochain_complex.image_map_ι

modified theorem cochain_complex.induced_maps_commute

modified def cochain_complex.kernel_functor

modified theorem cochain_complex.kernel_map_comp

modified theorem cochain_complex.kernel_map_id

Modified src/algebraic_geometry/presheafed_space.lean

modified theorem algebraic_geometry.PresheafedSpace.as_coe

modified def algebraic_geometry.PresheafedSpace.comp

modified theorem algebraic_geometry.PresheafedSpace.comp_c_app

modified theorem algebraic_geometry.PresheafedSpace.comp_coe

modified theorem algebraic_geometry.PresheafedSpace.ext

modified theorem algebraic_geometry.PresheafedSpace.f_as_coe

modified def algebraic_geometry.PresheafedSpace.forget

modified structure algebraic_geometry.PresheafedSpace.hom

modified theorem algebraic_geometry.PresheafedSpace.hom_mk_coe

modified def algebraic_geometry.PresheafedSpace.id

modified theorem algebraic_geometry.PresheafedSpace.id_c

modified theorem algebraic_geometry.PresheafedSpace.id_c_app

modified theorem algebraic_geometry.PresheafedSpace.id_coe

modified theorem algebraic_geometry.PresheafedSpace.id_coe_fn

modified def category_theory.functor.map_presheaf

modified theorem category_theory.functor.map_presheaf_map_c

modified theorem category_theory.functor.map_presheaf_map_f

modified theorem category_theory.functor.map_presheaf_obj_X

modified theorem category_theory.functor.map_presheaf_obj_𝒪

Modified src/algebraic_geometry/stalks.lean

modified def algebraic_geometry.PresheafedSpace.stalk

modified theorem algebraic_geometry.PresheafedSpace.stalk_map.comp

modified theorem algebraic_geometry.PresheafedSpace.stalk_map.id

modified def algebraic_geometry.PresheafedSpace.stalk_map

Modified src/category_theory/abelian/basic.lean

modified def category_theory.abelian.has_pullbacks

modified def category_theory.abelian.has_pushouts

Modified src/category_theory/action.lean

Modified src/category_theory/category/Rel.lean

Modified src/category_theory/category/default.lean

Modified src/category_theory/closed/cartesian.lean

modified def category_theory.binary_product_exponentiable

modified def category_theory.cartesian_closed

modified def category_theory.exponentiable

modified def category_theory.mul_zero

modified def category_theory.pow_zero

modified def category_theory.prod_coprod_distrib

modified def category_theory.terminal_exponentiable

modified def category_theory.zero_mul

Modified src/category_theory/conj.lean

modified theorem category_theory.iso.refl_conj

Modified src/category_theory/differential_object.lean

modified theorem category_theory.differential_object.comp_f

modified def category_theory.differential_object.forget

modified def category_theory.differential_object.hom.comp

modified def category_theory.differential_object.hom.id

modified structure category_theory.differential_object.hom

modified theorem category_theory.differential_object.id_f

modified theorem category_theory.differential_object.zero_f

Modified src/category_theory/elements.lean

Modified src/category_theory/endomorphism.lean

modified def category_theory.End

Modified src/category_theory/epi_mono.lean

modified def category_theory.retraction

modified def category_theory.section_

Modified src/category_theory/graded_object.lean

modified theorem category_theory.graded_object.zero_apply

Modified src/category_theory/groupoid.lean

modified def category_theory.groupoid.of_is_iso

Modified src/category_theory/limits/connected.lean

Modified src/category_theory/limits/creates.lean

Modified src/category_theory/limits/functor_category.lean

modified def category_theory.limits.functor_category_is_colimit_cocone

Modified src/category_theory/limits/lattice.lean

Modified src/category_theory/limits/limits.lean

modified theorem category_theory.limits.colimit.pre_map'

modified theorem category_theory.limits.limit.map_pre'

Modified src/category_theory/limits/opposites.lean

Modified src/category_theory/limits/over.lean

modified def category_theory.over.construct_products.over_binary_product_of_pullback

modified def category_theory.over.construct_products.over_finite_products_of_finite_wide_pullbacks

modified def category_theory.over.construct_products.over_product_of_wide_pullback

modified def category_theory.over.construct_products.over_products_of_wide_pullbacks

Modified src/category_theory/limits/preserves.lean

modified def category_theory.limits.preserves_colimit_iso

modified def category_theory.limits.preserves_limit_iso

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

modified def category_theory.limits.coprod.map

modified def category_theory.limits.prod.map

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

modified def category_theory.limits.binary_bicone.to_cocone

modified theorem category_theory.limits.binary_bicone.to_cocone_X

modified theorem category_theory.limits.binary_bicone.to_cocone_ι_app_left

modified theorem category_theory.limits.binary_bicone.to_cocone_ι_app_right

modified def category_theory.limits.binary_bicone.to_cone

modified theorem category_theory.limits.binary_bicone.to_cone_X

modified theorem category_theory.limits.binary_bicone.to_cone_π_app_left

modified theorem category_theory.limits.binary_bicone.to_cone_π_app_right

modified def category_theory.limits.biprod.desc

modified def category_theory.limits.biprod.fst

modified theorem category_theory.limits.biprod.hom_ext'

modified theorem category_theory.limits.biprod.hom_ext

modified def category_theory.limits.biprod.inl

modified theorem category_theory.limits.biprod.inl_fst

modified theorem category_theory.limits.biprod.inl_map

modified theorem category_theory.limits.biprod.inl_snd

modified def category_theory.limits.biprod.inr

modified theorem category_theory.limits.biprod.inr_fst

modified theorem category_theory.limits.biprod.inr_map

modified theorem category_theory.limits.biprod.inr_snd

modified def category_theory.limits.biprod.lift

modified def category_theory.limits.biprod.map'

modified def category_theory.limits.biprod.map

modified theorem category_theory.limits.biprod.map_eq

modified theorem category_theory.limits.biprod.map_eq_map'

modified theorem category_theory.limits.biprod.map_fst

modified def category_theory.limits.biprod.map_iso

modified theorem category_theory.limits.biprod.map_snd

modified def category_theory.limits.biprod.snd

modified def category_theory.limits.biprod

modified def category_theory.limits.biprod_iso

modified theorem category_theory.limits.biproduct.hom_ext'

modified theorem category_theory.limits.biproduct.hom_ext

modified theorem category_theory.limits.biproduct.inl_map

modified def category_theory.limits.biproduct.map'

modified def category_theory.limits.biproduct.map

modified theorem category_theory.limits.biproduct.map_eq

modified theorem category_theory.limits.biproduct.map_eq_map'

modified def category_theory.limits.has_binary_biproduct.of_has_binary_coproduct

modified def category_theory.limits.has_binary_biproduct.of_has_binary_product

modified def category_theory.limits.has_binary_biproducts.of_has_binary_coproducts

modified def category_theory.limits.has_binary_biproducts.of_has_binary_products

modified def category_theory.limits.has_binary_biproducts_of_finite_biproducts

modified def category_theory.limits.has_biproduct.of_has_coproduct

modified def category_theory.limits.has_biproduct.of_has_product

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

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

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

Modified src/category_theory/limits/shapes/constructions/preserve_binary_products.lean

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

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

modified theorem category_theory.limits.cofork.of_cocone_ι

modified def category_theory.limits.diagram_iso_parallel_pair

modified theorem category_theory.limits.fork.of_cone_π

modified def category_theory.limits.has_coequalizers_of_has_finite_colimits

modified def category_theory.limits.has_equalizers_of_has_finite_limits

modified def category_theory.limits.parallel_pair

modified theorem category_theory.limits.walking_parallel_pair_hom_id

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

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

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

modified structure category_theory.limits.strong_epi_mono_factorisation

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

modified def category_theory.limits.has_cokernels_of_has_finite_colimits

modified def category_theory.limits.has_kernels_of_has_finite_limits

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

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

modified def category_theory.limits.cospan

modified def category_theory.limits.has_pullbacks_of_has_finite_limits

modified def category_theory.limits.has_pushouts_of_has_finite_colimits

modified def category_theory.limits.span

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

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

modified def category_theory.limits.has_initial_of_unique

modified def category_theory.limits.has_terminal_of_unique

modified def category_theory.limits.initial.to

modified def category_theory.limits.initial

modified def category_theory.limits.terminal.from

modified def category_theory.limits.terminal

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

modified def has_finite_wide_pullbacks_of_has_finite_limits

modified def has_finite_wide_pushouts_of_has_finite_limits

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

modified theorem category_theory.limits.has_zero_morphisms.ext

modified def category_theory.limits.has_zero_object.has_initial

modified def category_theory.limits.has_zero_object.has_terminal

modified def category_theory.limits.has_zero_object.zero_morphisms_of_zero_object

Modified src/category_theory/limits/types.lean

Modified src/category_theory/monad/adjunction.lean

Modified src/category_theory/monad/algebra.lean

modified structure category_theory.comonad.coalgebra

modified structure category_theory.monad.algebra

Modified src/category_theory/monad/limits.lean

modified def category_theory.has_limits_of_reflective

modified def category_theory.monadic_creates_limits

Modified src/category_theory/monoidal/category.lean

Modified src/category_theory/monoidal/functorial.lean

Modified src/category_theory/monoidal/of_has_finite_products.lean

modified def category_theory.monoidal_of_has_finite_coproducts

modified def category_theory.monoidal_of_has_finite_products

Modified src/category_theory/preadditive.lean

modified def category_theory.preadditive.has_coequalizers_of_has_cokernels

modified def category_theory.preadditive.has_equalizers_of_has_kernels

Modified src/category_theory/schur.lean

modified def category_theory.is_iso_of_hom_simple

Modified src/category_theory/shift.lean

modified def category_theory.shift

Modified src/category_theory/simple.lean

modified def category_theory.is_iso_of_epi_of_nonzero

modified def category_theory.is_iso_of_mono_of_nonzero

modified theorem category_theory.simple.ext

modified def category_theory.simple_of_cosimple

modified theorem category_theory.zero_not_simple