Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2020-04-11 22:53 ee8cb15a

View on Github →

feat(category_theory): functorial images (#2373) This is the first in a series of most likely three PRs about the cohomology functor. In this PR, I

add documentation for comma.lean,
introduce the arrow category as a special case of the comma construction, and
introduce the notion of functorial images, which means that commutative squares induce morphisms on images making the obvious diagram commute.

Estimated changes

Modified src/category_theory/comma.lean

added def category_theory.arrow.hom_mk'

added theorem category_theory.arrow.hom_mk'_left

added theorem category_theory.arrow.hom_mk'_right

added def category_theory.arrow.hom_mk

added theorem category_theory.arrow.hom_mk_left

added theorem category_theory.arrow.hom_mk_right

added theorem category_theory.arrow.id_left

added theorem category_theory.arrow.id_right

added def category_theory.arrow.mk

added theorem category_theory.arrow.mk_hom

added def category_theory.arrow

added theorem category_theory.comma.id_left

added theorem category_theory.comma.id_right

modified def category_theory.comma.map_right_comp

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

added def category_theory.limits.has_image_map_comp

added def category_theory.limits.has_image_map_id

added def category_theory.limits.im

added theorem category_theory.limits.image.factor_map

added def category_theory.limits.image.map

added theorem category_theory.limits.image.map_comp

added theorem category_theory.limits.image.map_hom_mk'_ι

added theorem category_theory.limits.image.map_id

added theorem category_theory.limits.image.map_ι