Commit 2023-03-08 11:50 2b66476e

View on Github →

feat: port CategoryTheory.Limits.Preserves.Shapes.Zero (#2622)

Estimated changes

Modified Mathlib.lean

Created Mathlib/CategoryTheory/Limits/Preserves/Shapes/Zero.lean

added def CategoryTheory.Functor.mapZeroObject

added theorem CategoryTheory.Functor.map_eq_zero_iff

added def CategoryTheory.Functor.preservesInitialObjectOfPreservesZeroMorphisms

added def CategoryTheory.Functor.preservesTerminalObjectOfPreservesZeroMorphisms

added theorem CategoryTheory.Functor.preservesZeroMorphisms_of_map_zero_object

added theorem CategoryTheory.Functor.zero_of_map_zero