Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2020-08-03 05:29 60ba4782

View on Github →

feat(algebra/category/Module): the category of R-modules is abelian (#3606)

Estimated changes

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

added def Module.normal_epi

added def Module.normal_mono

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

added def Module.as_hom

added theorem Module.epi_of_range_eq_top

added theorem Module.ker_eq_bot_of_mono

deleted def Module.kernel_cone

deleted def Module.kernel_is_limit

added theorem Module.mono_of_ker_eq_bot

added theorem Module.range_eq_top_of_epi

added def linear_equiv.to_Module_iso'

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

added def Module.cokernel_cocone

added def Module.cokernel_is_colimit

added def Module.has_cokernels_Module

added def Module.has_kernels_Module

added def Module.kernel_cone

added def Module.kernel_is_limit

Modified src/linear_algebra/basic.lean

added theorem linear_map.comp_ker_subtype

added theorem linear_map.ker_eq_bot_of_cancel

added theorem linear_map.range_eq_top_of_cancel

added theorem linear_map.range_mkq_comp

added def submodule.quot_equiv_of_eq