Mathlib Changelog
v4
Changelog
About
Github
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