Commit 2022-03-15 03:05 f3378562

View on Github →

feat(algebra/category): show categorical image in Module agrees with range (#12605) This just follows the existing code for the same fact in AddCommGroup. This PR is preparing for a better API for homological calculations in Module R.

Estimated changes

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

added def Module.factor_thru_image

added theorem Module.image.fac

added theorem Module.image.lift_fac

added def Module.image.ι

added def Module.image

added theorem Module.image_iso_range_hom_subtype

added theorem Module.image_iso_range_inv_image_ι

added def Module.mono_factorisation