Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2019-05-03 11:30 f5060c40

View on Github →

feat(category_theory/limits): support for special shapes of (co)limits (#938) feat(category_theory/limits): support for special shapes of (co)limits

Estimated changes

Created docs/tutorial/category_theory/calculating_colimits_in_Top.lean

added def I

added def I_0

added def I_1

added def R

added def X

added def Y

added def cylinder

added def cylinder_0

added def cylinder_1

added def d

added def f

added def g

added def mapping_cone

added def mapping_cylinder

added def mapping_cylinder_0

added def pt

added def q

added def to_pt

added def w

Modified src/category_theory/discrete_category.lean

Modified src/category_theory/instances/Top/basic.lean

added def category_theory.instances.Top.of

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

added def category_theory.limits.binary_cofan.mk

added def category_theory.limits.binary_cofan

added def category_theory.limits.binary_fan.mk

added def category_theory.limits.binary_fan

added def category_theory.limits.pair

added def category_theory.limits.pair_function

added inductive category_theory.limits.walking_pair

Created src/category_theory/limits/shapes/default.lean

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

added def category_theory.limits.cocone.of_cofork

added theorem category_theory.limits.cocone.of_cofork_ι

added def category_theory.limits.cofork.condition

added def category_theory.limits.cofork.of_cocone

added theorem category_theory.limits.cofork.of_cocone_ι

added def category_theory.limits.cofork.of_π

added def category_theory.limits.cofork.π

added def category_theory.limits.cofork

added def category_theory.limits.cone.of_fork

added theorem category_theory.limits.cone.of_fork_π

added def category_theory.limits.fork.condition

added def category_theory.limits.fork.of_cone

added theorem category_theory.limits.fork.of_cone_π

added def category_theory.limits.fork.of_ι

added theorem category_theory.limits.fork.of_ι_app_one

added theorem category_theory.limits.fork.of_ι_app_zero

added def category_theory.limits.fork.ι

added def category_theory.limits.fork

added def category_theory.limits.parallel_pair

added theorem category_theory.limits.parallel_pair_functor_obj

added theorem category_theory.limits.parallel_pair_map_left

added theorem category_theory.limits.parallel_pair_map_right

added inductive category_theory.limits.walking_parallel_pair

added def category_theory.limits.walking_parallel_pair_hom.comp

added inductive category_theory.limits.walking_parallel_pair_hom

added theorem category_theory.limits.walking_parallel_pair_hom_id

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

added def category_theory.limits.cofan.mk

added def category_theory.limits.cofan

added def category_theory.limits.fan.mk

added def category_theory.limits.fan

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

added def category_theory.limits.cocone.of_pushout_cocone

added theorem category_theory.limits.cocone.of_pushout_cocone_ι

added def category_theory.limits.cone.of_pullback_cone

added theorem category_theory.limits.cone.of_pullback_cone_π

added def category_theory.limits.cospan

added theorem category_theory.limits.cospan_left

added theorem category_theory.limits.cospan_map_id

added theorem category_theory.limits.cospan_map_inl

added theorem category_theory.limits.cospan_map_inr

added theorem category_theory.limits.cospan_one

added theorem category_theory.limits.cospan_right

added theorem category_theory.limits.pullback_cone.condition

added def category_theory.limits.pullback_cone.mk

added def category_theory.limits.pullback_cone.of_cone

added theorem category_theory.limits.pullback_cone.of_cone_π

added def category_theory.limits.pullback_cone.π₁

added def category_theory.limits.pullback_cone.π₂

added def category_theory.limits.pullback_cone

added theorem category_theory.limits.pushout_cocone.condition

added def category_theory.limits.pushout_cocone.mk

added def category_theory.limits.pushout_cocone.of_cocone

added theorem category_theory.limits.pushout_cocone.of_cocone_ι

added def category_theory.limits.pushout_cocone.ι₁

added def category_theory.limits.pushout_cocone.ι₂

added def category_theory.limits.pushout_cocone

added def category_theory.limits.span

added theorem category_theory.limits.span_left

added theorem category_theory.limits.span_map_fst

added theorem category_theory.limits.span_map_id

added theorem category_theory.limits.span_map_snd

added theorem category_theory.limits.span_right

added theorem category_theory.limits.span_zero

added def category_theory.limits.walking_cospan.hom.comp

added inductive category_theory.limits.walking_cospan.hom

added theorem category_theory.limits.walking_cospan.hom_id

added inductive category_theory.limits.walking_cospan

added def category_theory.limits.walking_span.hom.comp

added inductive category_theory.limits.walking_span.hom

added theorem category_theory.limits.walking_span.hom_id

added inductive category_theory.limits.walking_span

Created src/category_theory/sparse.lean

added def category_theory.sparse_category

Modified src/tactic/basic.lean