Condensed abelian groups form an abelian category.

@[inline, reducible]

abbrev CondensedAb : Type (u + 2)

The category of condensed abelian groups, defined as sheaves of abelian groups over CompHaus with respect to the coherent Grothendieck topology.

Equations

• CondensedAb = Condensed AddCommGroupCat

noncomputable instance CondensedAb.abelian : CategoryTheory.Abelian CondensedAb

Equations

• CondensedAb.abelian = CategoryTheory.sheafIsAbelian