Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2022-05-09 11:26 c43486ec

View on Github →

feat(category_theory/limits): allow (co)limits over lower universes in algebraic categories (#13990) I'm concerned about the new universe annotations required in places. It was not so impossible to add them when proofs broke, but the proofs might have been hard to construct in the first place ....

Estimated changes

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

modified def Algebra.has_limits.limit_cone

modified def Algebra.has_limits.limit_cone_is_limit

modified def Algebra.limit_π_alg_hom

modified def Algebra.sections_subalgebra

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

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

modified def CommGroup.filtered_colimits.G

modified def Group.filtered_colimits.G

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

modified def AddCommGroup.kernel_iso_ker

modified def CommGroup.forget₂_CommMon_preserves_limits_aux

modified def CommGroup.limit_cone

modified def CommGroup.limit_cone_is_limit

modified def Group.limit_cone

modified def Group.limit_cone_is_limit

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

modified theorem Module.coe_of

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

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

modified def Module.forget₂_AddCommGroup_preserves_limits_aux

modified def Module.has_limits.limit_cone

modified def Module.has_limits.limit_cone_is_limit

modified def Module.sections_submodule

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

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

modified def CommMon.filtered_colimits.M

modified def Mon.filtered_colimits.M

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

modified def CommMon.limit_cone

modified def CommMon.limit_cone_is_limit

modified def Mon.has_limits.limit_cone

modified def Mon.has_limits.limit_cone_is_limit

modified def Mon.limit_π_monoid_hom

modified def Mon.sections_submonoid

Modified src/algebra/category/Ring/filtered_colimits.lean

modified def SemiRing.filtered_colimits.R

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

modified def CommRing.forget₂_CommSemiRing_preserves_limits_aux

modified def CommRing.limit_cone

modified def CommRing.limit_cone_is_limit

modified def CommSemiRing.limit_cone

modified def CommSemiRing.limit_cone_is_limit

modified def Ring.forget₂_AddCommGroup_preserves_limits_aux

modified def Ring.limit_cone

modified def Ring.limit_cone_is_limit

modified def Ring.sections_subring

modified def SemiRing.forget₂_AddCommMon_preserves_limits_aux

modified def SemiRing.forget₂_Mon_preserves_limits_aux

modified def SemiRing.has_limits.limit_cone

modified def SemiRing.has_limits.limit_cone_is_limit

modified def SemiRing.limit_π_ring_hom

modified def SemiRing.sections_subsemiring

Modified src/algebraic_geometry/locally_ringed_space/has_colimits.lean

Modified src/algebraic_geometry/open_immersion.lean

Modified src/algebraic_topology/fundamental_groupoid/product.lean

Modified src/category_theory/category/Cat/limit.lean

Modified src/category_theory/limits/concrete_category.lean

Modified src/category_theory/limits/filtered_colimit_commutes_finite_limit.lean

Modified src/category_theory/limits/final.lean

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

Modified src/category_theory/limits/types.lean

added theorem category_theory.limits.types.colimit.w_apply'

modified theorem category_theory.limits.types.colimit.w_apply

added theorem category_theory.limits.types.colimit.ι_desc_apply'

modified theorem category_theory.limits.types.colimit.ι_desc_apply

added theorem category_theory.limits.types.colimit.ι_map_apply'

modified theorem category_theory.limits.types.colimit.ι_map_apply

modified def category_theory.limits.types.colimit_cocone

modified def category_theory.limits.types.colimit_cocone_is_colimit

modified theorem category_theory.limits.types.colimit_eq

modified def category_theory.limits.types.colimit_equiv_quot

modified theorem category_theory.limits.types.colimit_equiv_quot_apply

modified theorem category_theory.limits.types.colimit_equiv_quot_symm_apply

modified def category_theory.limits.types.is_limit_equiv_sections

modified theorem category_theory.limits.types.jointly_surjective'

modified theorem category_theory.limits.types.jointly_surjective

added theorem category_theory.limits.types.limit.lift_π_apply'

modified theorem category_theory.limits.types.limit.lift_π_apply

added theorem category_theory.limits.types.limit.map_π_apply'

modified theorem category_theory.limits.types.limit.map_π_apply

modified def category_theory.limits.types.limit.mk

added theorem category_theory.limits.types.limit.w_apply'

modified theorem category_theory.limits.types.limit.w_apply

added theorem category_theory.limits.types.limit.π_mk'

modified theorem category_theory.limits.types.limit.π_mk

modified def category_theory.limits.types.limit_cone

modified def category_theory.limits.types.limit_cone_is_limit

modified def category_theory.limits.types.limit_equiv_sections

modified theorem category_theory.limits.types.limit_equiv_sections_apply

added theorem category_theory.limits.types.limit_equiv_sections_symm_apply'

modified theorem category_theory.limits.types.limit_equiv_sections_symm_apply

added theorem category_theory.limits.types.limit_ext'

modified theorem category_theory.limits.types.limit_ext

added theorem category_theory.limits.types.limit_ext_iff'

modified theorem category_theory.limits.types.limit_ext_iff

modified def category_theory.limits.types.quot.rel

modified def category_theory.limits.types.quot

Modified src/category_theory/sites/sheaf_of_types.lean

Modified src/topology/category/CompHaus/default.lean

modified def CompHaus.limit_cone

modified def CompHaus.limit_cone_is_limit

Modified src/topology/category/Profinite/cofiltered_limit.lean

Modified src/topology/category/Profinite/default.lean

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

modified theorem Top.coinduced_of_is_colimit

modified def Top.colimit_cocone

modified def Top.colimit_cocone_is_colimit

modified theorem Top.colimit_is_open_iff

modified theorem Top.colimit_topology

modified theorem Top.induced_of_is_limit

modified def Top.limit_cone

modified def Top.limit_cone_infi

modified def Top.limit_cone_infi_is_limit

modified def Top.limit_cone_is_limit

modified theorem Top.limit_topology

modified def Top.pi_fan

modified def Top.pi_fan_is_limit

modified def Top.pi_iso_pi

modified theorem Top.pi_iso_pi_hom_apply

modified theorem Top.pi_iso_pi_inv_π

modified theorem Top.pi_iso_pi_inv_π_apply

modified def Top.pi_π

modified def Top.sigma_cofan

modified def Top.sigma_cofan_is_colimit

modified def Top.sigma_iso_sigma

modified theorem Top.sigma_iso_sigma_hom_ι

modified theorem Top.sigma_iso_sigma_hom_ι_apply

modified theorem Top.sigma_iso_sigma_inv_apply

modified def Top.sigma_ι

Modified src/topology/gluing.lean

Modified src/topology/sheaves/local_predicate.lean

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

Modified src/topology/sheaves/stalks.lean