Magnitude conjecture

QuotientSubmoduleEquidistribution.CategoryTheory.CategoricalRadicalIdeal

The categorical radical as an additive Hom ideal #

The Jacobson condition IsRadicalMorphism f is closed under addition, negation, and arbitrary composition. Consequently it defines a canonical two-sided additive Hom ideal in every preadditive category.

source
theorem QuotientSubmoduleEquidistribution.CategoricalRadical.isRadicalMorphism_zero {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Preadditive C] {X Y : C} :
IsRadicalMorphism 0

The zero morphism is radical.

source
theorem QuotientSubmoduleEquidistribution.CategoricalRadical.isRadicalMorphism_neg {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Preadditive C] {X Y : C} {f : X ⟶ Y} (hf : IsRadicalMorphism f) :
IsRadicalMorphism (-f)

The negative of a radical morphism is radical.

source
theorem QuotientSubmoduleEquidistribution.CategoricalRadical.isRadicalMorphism_add {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Preadditive C] {X Y : C} {f r : X ⟶ Y} (hf : IsRadicalMorphism f) (hr : IsRadicalMorphism r) :
IsRadicalMorphism (f + r)

The sum of two radical morphisms is radical.

source
def QuotientSubmoduleEquidistribution.CategoricalRadical.homIdeal {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Preadditive C] :
CategoricalIdeal.HomIdeal C

The canonical categorical Jacobson radical Hom ideal.

Instances For
    source
    @[simp]
    theorem QuotientSubmoduleEquidistribution.CategoricalRadical.mem_homIdeal_iff {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Preadditive C] {X Y : C} (f : X ⟶ Y) :
    f ∈ homIdeal.hom X Y ↔ IsRadicalMorphism f