Commit 2021-05-07 04:59 154fda29

View on Github →

feat(category_theory/subobjects): more about kernel and image subobjects (#7467) Lemmas about factoring through kernel subobjects, and functoriality of kernel subobjects.

Estimated changes

Modified src/algebraic_geometry/presheafed_space.lean

Modified src/category_theory/subobject/limits.lean

added def category_theory.limits.factor_thru_kernel_subobject

added theorem category_theory.limits.factor_thru_kernel_subobject_comp_arrow

added theorem category_theory.limits.image_subobject_arrow_comp_eq_zero

added def category_theory.limits.kernel_subobject_map

added theorem category_theory.limits.kernel_subobject_map_arrow

added theorem category_theory.limits.kernel_subobject_map_comp

added theorem category_theory.limits.kernel_subobject_map_id