Additive ideals in preadditive categories

This file contains the lightweight two-sided Hom-ideal structure shared by categorical quotients and radical-power arguments.

structure QuotientSubmoduleEquidistribution.CategoricalIdeal.HomIdeal (C : Type u) [CategoryTheory.Category.{v, u} C] [CategoryTheory.Preadditive C] : Type (max u v)

A two-sided additive ideal in a preadditive category.

• hom (X Y : C) : AddSubgroup (X ⟶ Y)
• precomp {X Y Z : C} (f : X ⟶ Y) {g : Y ⟶ Z} : g ∈ self.hom Y Z → CategoryTheory.CategoryStruct.comp f g ∈ self.hom X Z
• postcomp {X Y Z : C} {f : X ⟶ Y} (g : Y ⟶ Z) : f ∈ self.hom X Y → CategoryTheory.CategoryStruct.comp f g ∈ self.hom X Z