Commit 2023-07-31 08:59 4773f928

View on Github →

feat(Algebra/Category/GroupCat/Abelian): prove AddCommGroupCat is AB5 (#5597) This work was done during the 2023 Copenhagen masterclass on formalisation of condensed mathematics. Numerous participants contributed.

Estimated changes

Modified Mathlib.lean

Modified Mathlib/Algebra/Category/GroupCat/Abelian.lean

added theorem AddCommGroupCat.exact_iff

Modified Mathlib/Algebra/Category/GroupCat/Basic.lean

added theorem CommGroupCat.comp_def

added theorem GroupCat.comp_def

Created Mathlib/Algebra/Category/GroupCat/Kernels.lean

added def AddCommGroupCat.cokernelCocone

added def AddCommGroupCat.cokernelIsColimit

added def AddCommGroupCat.kernelCone

added def AddCommGroupCat.kernelIsLimit

Modified Mathlib/GroupTheory/QuotientGroup.lean

added theorem QuotientGroup.ker_le_range_iff

Modified Mathlib/GroupTheory/Subgroup/Basic.lean

added theorem MonoidHom.range_le_ker_iff