Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2018-12-02 17:36 de4f6897

View on Github →

feat(category_theory/limits): (co)limits, and (co)limits in Type

Estimated changes

Created category_theory/limits/limits.lean

added theorem category_theory.limits.colim.ι_map

added def category_theory.limits.colim

added def category_theory.limits.colimit.cocone

added def category_theory.limits.colimit.cocone_morphism

added theorem category_theory.limits.colimit.cocone_morphism_hom

added theorem category_theory.limits.colimit.cocone_ι

added def category_theory.limits.colimit.desc

added theorem category_theory.limits.colimit.hom_ext

added def category_theory.limits.colimit.hom_iso'

added def category_theory.limits.colimit.hom_iso

added theorem category_theory.limits.colimit.hom_iso_hom

added def category_theory.limits.colimit.is_colimit

added theorem category_theory.limits.colimit.is_colimit_desc

added theorem category_theory.limits.colimit.map_desc

added theorem category_theory.limits.colimit.map_post

added def category_theory.limits.colimit.post

added theorem category_theory.limits.colimit.post_desc

added theorem category_theory.limits.colimit.post_post

added def category_theory.limits.colimit.pre

added theorem category_theory.limits.colimit.pre_desc

added theorem category_theory.limits.colimit.pre_map

added theorem category_theory.limits.colimit.pre_post

added theorem category_theory.limits.colimit.pre_pre

added theorem category_theory.limits.colimit.w

added def category_theory.limits.colimit.ι

added theorem category_theory.limits.colimit.ι_cocone_morphism

added theorem category_theory.limits.colimit.ι_desc

added theorem category_theory.limits.colimit.ι_post

added theorem category_theory.limits.colimit.ι_pre

added def category_theory.limits.colimit

added def category_theory.limits.has_colimits

added def category_theory.limits.has_colimits_of_shape

added def category_theory.limits.has_limits

added def category_theory.limits.has_limits_of_shape

added def category_theory.limits.is_colimit.desc_cocone_morphism

added theorem category_theory.limits.is_colimit.hom_desc

added theorem category_theory.limits.is_colimit.hom_ext

added def category_theory.limits.is_colimit.hom_iso'

added def category_theory.limits.is_colimit.hom_iso

added theorem category_theory.limits.is_colimit.hom_iso_hom

added def category_theory.limits.is_colimit.mk_cocone_morphism

added def category_theory.limits.is_colimit.nat_iso

added def category_theory.limits.is_colimit.of_iso_colimit

added theorem category_theory.limits.is_colimit.uniq_cocone_morphism

added def category_theory.limits.is_colimit.unique

added structure category_theory.limits.is_colimit

added theorem category_theory.limits.is_limit.hom_ext

added def category_theory.limits.is_limit.hom_iso'

added def category_theory.limits.is_limit.hom_iso

added theorem category_theory.limits.is_limit.hom_iso_hom

added theorem category_theory.limits.is_limit.hom_lift

added def category_theory.limits.is_limit.lift_cone_morphism

added def category_theory.limits.is_limit.mk_cone_morphism

added def category_theory.limits.is_limit.nat_iso

added def category_theory.limits.is_limit.of_iso_limit

added theorem category_theory.limits.is_limit.uniq_cone_morphism

added def category_theory.limits.is_limit.unique

added structure category_theory.limits.is_limit

added theorem category_theory.limits.lim.map_π

added def category_theory.limits.lim

added def category_theory.limits.limit.cone

added def category_theory.limits.limit.cone_morphism

added theorem category_theory.limits.limit.cone_morphism_hom

added theorem category_theory.limits.limit.cone_morphism_π

added theorem category_theory.limits.limit.cone_π

added theorem category_theory.limits.limit.hom_ext

added def category_theory.limits.limit.hom_iso'

added def category_theory.limits.limit.hom_iso

added theorem category_theory.limits.limit.hom_iso_hom

added def category_theory.limits.limit.is_limit

added theorem category_theory.limits.limit.is_limit_lift

added def category_theory.limits.limit.lift

added theorem category_theory.limits.limit.lift_map

added theorem category_theory.limits.limit.lift_post

added theorem category_theory.limits.limit.lift_pre

added theorem category_theory.limits.limit.lift_π

added theorem category_theory.limits.limit.map_post

added theorem category_theory.limits.limit.map_pre

added def category_theory.limits.limit.post

added theorem category_theory.limits.limit.post_post

added theorem category_theory.limits.limit.post_π

added def category_theory.limits.limit.pre

added theorem category_theory.limits.limit.pre_post

added theorem category_theory.limits.limit.pre_pre

added theorem category_theory.limits.limit.pre_π

added theorem category_theory.limits.limit.w

added def category_theory.limits.limit.π

added def category_theory.limits.limit

Created category_theory/limits/types.lean

added def category_theory.limits.types.colimit

added def category_theory.limits.types.colimit_is_colimit

added def category_theory.limits.types.limit

added def category_theory.limits.types.limit_is_limit

added theorem category_theory.limits.types.types_colimit

added theorem category_theory.limits.types.types_colimit_desc

added theorem category_theory.limits.types.types_colimit_map

added theorem category_theory.limits.types.types_colimit_pre

added theorem category_theory.limits.types.types_colimit_ι

added theorem category_theory.limits.types.types_limit

added theorem category_theory.limits.types.types_limit_lift

added theorem category_theory.limits.types.types_limit_map

added theorem category_theory.limits.types.types_limit_pre

added theorem category_theory.limits.types.types_limit_π