Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2020-08-20 21:33 9f525c74

View on Github →

chore(category_theory/limits/types): cleanup (#3871) Backporting some cleaning up work from prop_limits, while it rumbles onwards.

Estimated changes

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

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

Modified src/category_theory/limits/limits.lean

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

added def category_theory.limits.preserves_colimit_of_reflects_of_preserves

added def category_theory.limits.preserves_limit_of_reflects_of_preserves

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

Modified src/category_theory/limits/types.lean

deleted def category_theory.limits.types.colimit_

added def category_theory.limits.types.colimit_cocone

added def category_theory.limits.types.colimit_cocone_is_colimit

added def category_theory.limits.types.colimit_equiv_quot

added theorem category_theory.limits.types.colimit_equiv_quot_symm_apply

deleted def category_theory.limits.types.colimit_is_colimit_

added theorem category_theory.limits.types.lift_π_apply

deleted def category_theory.limits.types.limit_

added def category_theory.limits.types.limit_cone

added def category_theory.limits.types.limit_cone_is_limit

added def category_theory.limits.types.limit_equiv_sections

added theorem category_theory.limits.types.limit_equiv_sections_apply

added theorem category_theory.limits.types.limit_equiv_sections_symm_apply

added theorem category_theory.limits.types.limit_ext

deleted def category_theory.limits.types.limit_is_limit_

added def category_theory.limits.types.quot

deleted theorem category_theory.limits.types.types_colimit

deleted theorem category_theory.limits.types.types_colimit_desc

deleted theorem category_theory.limits.types.types_colimit_map

deleted theorem category_theory.limits.types.types_colimit_pre

deleted theorem category_theory.limits.types.types_colimit_ι

deleted theorem category_theory.limits.types.types_limit

deleted theorem category_theory.limits.types.types_limit_lift

deleted theorem category_theory.limits.types.types_limit_map

deleted theorem category_theory.limits.types.types_limit_pre

deleted theorem category_theory.limits.types.types_limit_π