Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2021-02-26 19:47 ddefd965

View on Github →

feat(category_theory/subobject): kernels and images as subobjects (#6301) Further work on subobjects, building on the initial definition in #6278.

Add noncomputable functions to obtain representatives of subobjects.
Realise kernel/equalizer/image as subobjects.

Estimated changes

Modified src/category_theory/subobject.lean

added def category_theory.limits.equalizer_subobject

added theorem category_theory.limits.equalizer_subobject_arrow'

added theorem category_theory.limits.equalizer_subobject_arrow

added theorem category_theory.limits.equalizer_subobject_arrow_comp

added def category_theory.limits.equalizer_subobject_iso

added def category_theory.limits.factor_thru_image_subobject

added def category_theory.limits.image_subobject

added theorem category_theory.limits.image_subobject_arrow'

added theorem category_theory.limits.image_subobject_arrow

added theorem category_theory.limits.image_subobject_arrow_comp

added def category_theory.limits.image_subobject_iso

added def category_theory.limits.kernel_subobject

added theorem category_theory.limits.kernel_subobject_arrow'

added theorem category_theory.limits.kernel_subobject_arrow

added theorem category_theory.limits.kernel_subobject_arrow_comp

added def category_theory.limits.kernel_subobject_iso

modified theorem category_theory.mono_over.bot_left

modified theorem category_theory.mono_over.forget_obj_left

added def category_theory.mono_over.image_mono_over

modified theorem category_theory.mono_over.top_left

added def category_theory.subobject.arrow

added def category_theory.subobject.representative

added def category_theory.subobject.representative_iso

added def category_theory.subobject.underlying

added theorem category_theory.subobject.underlying_arrow

added theorem category_theory.subobject.underlying_as_coe

added def category_theory.subobject.underlying_iso