Commit 2023-04-17 18:22 74a7c849

View on Github →

feat: port CategoryTheory.Subobject.Limits (#3450)

Estimated changes

Modified Mathlib.lean

Created Mathlib/CategoryTheory/Subobject/Limits.lean

added def CategoryTheory.Limits.cokernelOrderHom

added def CategoryTheory.Limits.equalizerSubobjectIso

added theorem CategoryTheory.Limits.equalizerSubobject_arrow'

added theorem CategoryTheory.Limits.equalizerSubobject_arrow

added theorem CategoryTheory.Limits.equalizerSubobject_arrow_comp

added theorem CategoryTheory.Limits.equalizerSubobject_factors

added theorem CategoryTheory.Limits.equalizerSubobject_factors_iff

added def CategoryTheory.Limits.factorThruImageSubobject

added theorem CategoryTheory.Limits.factorThruImageSubobject_comp_self

added theorem CategoryTheory.Limits.factorThruImageSubobject_comp_self_assoc

added def CategoryTheory.Limits.factorThruKernelSubobject

added theorem CategoryTheory.Limits.factorThruKernelSubobject_comp_arrow

added theorem CategoryTheory.Limits.factorThruKernelSubobject_comp_kernelSubobjectIso

added def CategoryTheory.Limits.imageSubobjectCompIso

added theorem CategoryTheory.Limits.imageSubobjectCompIso_hom_arrow

added theorem CategoryTheory.Limits.imageSubobjectCompIso_inv_arrow

added def CategoryTheory.Limits.imageSubobjectIso

added theorem CategoryTheory.Limits.imageSubobjectIso_comp_image_map

added def CategoryTheory.Limits.imageSubobjectMap

added theorem CategoryTheory.Limits.imageSubobjectMap_arrow

added theorem CategoryTheory.Limits.imageSubobject_arrow'

added theorem CategoryTheory.Limits.imageSubobject_arrow

added theorem CategoryTheory.Limits.imageSubobject_arrow_comp

added theorem CategoryTheory.Limits.imageSubobject_arrow_comp_eq_zero

added theorem CategoryTheory.Limits.imageSubobject_comp_le

added theorem CategoryTheory.Limits.imageSubobject_factors_comp_self

added theorem CategoryTheory.Limits.imageSubobject_iso_comp

added theorem CategoryTheory.Limits.imageSubobject_le

added theorem CategoryTheory.Limits.imageSubobject_le_mk

added theorem CategoryTheory.Limits.imageSubobject_mono

added theorem CategoryTheory.Limits.imageSubobject_zero

added theorem CategoryTheory.Limits.imageSubobject_zero_arrow

added theorem CategoryTheory.Limits.image_map_comp_imageSubobjectIso_inv

added def CategoryTheory.Limits.kernelOrderHom

added def CategoryTheory.Limits.kernelSubobjectIso

added def CategoryTheory.Limits.kernelSubobjectIsoComp

added theorem CategoryTheory.Limits.kernelSubobjectIsoComp_hom_arrow

added theorem CategoryTheory.Limits.kernelSubobjectIsoComp_inv_arrow

added theorem CategoryTheory.Limits.kernelSubobjectIso_comp_kernel_map

added def CategoryTheory.Limits.kernelSubobjectMap

added theorem CategoryTheory.Limits.kernelSubobjectMap_arrow

added theorem CategoryTheory.Limits.kernelSubobjectMap_comp

added theorem CategoryTheory.Limits.kernelSubobjectMap_id

added theorem CategoryTheory.Limits.kernelSubobject_arrow'

added theorem CategoryTheory.Limits.kernelSubobject_arrow

added theorem CategoryTheory.Limits.kernelSubobject_arrow_comp

added theorem CategoryTheory.Limits.kernelSubobject_comp_le

added theorem CategoryTheory.Limits.kernelSubobject_comp_mono

added theorem CategoryTheory.Limits.kernelSubobject_factors

added theorem CategoryTheory.Limits.kernelSubobject_factors_iff

added theorem CategoryTheory.Limits.kernelSubobject_zero

added theorem CategoryTheory.Limits.kernel_map_comp_kernelSubobjectIso_inv

added theorem CategoryTheory.Limits.le_kernelSubobject