A grothendieck category is an Ab5 category, such that there exists a single separator
Date: nil
Author: Anton Zakrewski
Created: 2024-10-14 Mo 08:55