Documentation

Mathlib.Algebra.Category.GroupCat.Abelian

The category of abelian groups is abelian #

In the category of abelian groups, every monomorphism is normal.

Equations
  • One or more equations did not get rendered due to their size.
Instances For

    In the category of abelian groups, every epimorphism is normal.

    Equations
    • One or more equations did not get rendered due to their size.
    Instances For

      The category of abelian groups is abelian.

      Equations

      The category of abelian groups satisfies Grothedieck's Axiom AB5.

      Equations
      • AddCommGroupCat.instPreservesFiniteLimitsFunctorColimOfIsFiltered = CategoryTheory.Limits.colim.preservesFiniteLimitsOfMapExact