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