Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2020-03-18 03:19 f07a1ebf

View on Github →

feat(category_theory): images in Ab and Type (#2101)

not stacked on top of limits/colimits
comment
add ext to add_monoid_hom.ext
fix
cleanup
suggestions from review
fix
use more existing structure
fix names
oops
linter

Estimated changes

Modified src/algebra/category/Group/adjunctions.lean

modified def AddCommGroup.adj

Modified src/algebra/category/Group/basic.lean

added def AddCommGroup.as_hom

added theorem AddCommGroup.as_hom_apply

added theorem AddCommGroup.as_hom_injective

added theorem AddCommGroup.injective_of_mono

added theorem AddCommGroup.int_hom_ext

Created src/algebra/category/Group/images.lean

added def AddCommGroup.factor_thru_image

added theorem AddCommGroup.image.fac

added theorem AddCommGroup.image.lift_fac

added def AddCommGroup.image.ι

added def AddCommGroup.image

added def AddCommGroup.mono_factorisation

Modified src/algebra/group_power.lean

added theorem gsmul_int_int

added theorem gsmul_int_one

Modified src/category_theory/concrete_category/basic.lean

added theorem category_theory.concrete_category.hom_ext

added theorem category_theory.concrete_category.mono_of_injective

Modified src/category_theory/limits/shapes/images.lean

Modified src/category_theory/limits/types.lean

added theorem category_theory.limits.types.image.lift_fac

added def category_theory.limits.types.image.ι

added def category_theory.limits.types.image

added def category_theory.limits.types.mono_factorisation

Modified src/group_theory/subgroup.lean

added def monoid_hom.range_factorization

added def monoid_hom.range_subtype_val