Magnitude conjecture

QuotientSubmoduleEquidistribution.CategoryTheory.CategoricalRadical

The radical of a preadditive category #

This file defines the standard Jacobson-radical condition for a morphism in a preadditive category and proves a one-generator cosemisimplicity criterion. If every object is a finite biproduct of one object P and every nonzero endomorphism of P is invertible, then the categorical radical is zero.

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

The Jacobson-radical condition for a morphism in a preadditive category, using the source-object convention.

Instances For
    source
    theorem QuotientSubmoduleEquidistribution.CategoricalRadical.isIso_one_sub_comp {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Preadditive C] {X Y : C} (a : X ⟶ Y) (b : Y ⟶ X) [CategoryTheory.IsIso (CategoryTheory.CategoryStruct.id X - CategoryTheory.CategoryStruct.comp a b)] :
    CategoryTheory.IsIso (CategoryTheory.CategoryStruct.id Y - CategoryTheory.CategoryStruct.comp b a)

    The categorical Jacobson identity: invertibility of 1 - a b implies invertibility of 1 - b a.

    source
    theorem QuotientSubmoduleEquidistribution.CategoricalRadical.isRadicalMorphism_precomp {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Preadditive C] {W X Y : C} (a : W ⟶ X) {f : X ⟶ Y} (hf : IsRadicalMorphism f) :
    IsRadicalMorphism (CategoryTheory.CategoryStruct.comp a f)

    The categorical radical is closed under precomposition.

    source
    theorem QuotientSubmoduleEquidistribution.CategoricalRadical.isRadicalMorphism_postcomp {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Preadditive C] {X Y Z : C} {f : X ⟶ Y} (b : Y ⟶ Z) (hf : IsRadicalMorphism f) :
    IsRadicalMorphism (CategoryTheory.CategoryStruct.comp f b)

    The categorical radical is closed under postcomposition.

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

    Adding a radical morphism to a split monomorphism preserves split monicity.

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

    Adding a radical morphism to a split epimorphism preserves split epicity.

    source
    def QuotientSubmoduleEquidistribution.CategoricalRadical.HasZeroRadical (C : Type u) [CategoryTheory.Category.{v, u} C] [CategoryTheory.Preadditive C] :
    Prop

    A preadditive category has zero radical if its only radical morphisms are zero.

    Instances For
      source
      theorem QuotientSubmoduleEquidistribution.CategoricalRadical.isRadicalMorphism_of_forall_comp_isNilpotent {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Preadditive C] {X Y : C} (f : X ⟶ Y) (h : ∀ (g : Y ⟶ X), IsNilpotent (CategoryTheory.End.of (CategoryTheory.CategoryStruct.comp f g))) :
      IsRadicalMorphism f

      A morphism is radical if every return composite is nilpotent.

      source
      theorem QuotientSubmoduleEquidistribution.CategoricalRadical.radicalMorphism_eq_zero_between_biproducts {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Preadditive C] [CategoryTheory.Limits.HasFiniteBiproducts C] {P : C} (hP : ∀ (a : CategoryTheory.End P), a ≠ 0 → CategoryTheory.IsIso a) {J K : Type} [Fintype J] [Fintype K] (f : (⨁ fun (x : J) => P) ⟶ ⨁ fun (x : K) => P) (hf : IsRadicalMorphism f) :
      f = 0

      If every nonzero endomorphism of P is invertible, then the categorical radical between any two finite biproducts of P is zero.

      source
      def QuotientSubmoduleEquidistribution.CategoricalRadical.IsAdditivelyGeneratedBy {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Preadditive C] [CategoryTheory.Limits.HasFiniteBiproducts C] (P : C) :
      Prop

      A category is additively generated by one object when every object is isomorphic to a finite biproduct of copies of it.

      Instances For
        source
        theorem QuotientSubmoduleEquidistribution.CategoricalRadical.radicalMorphism_eq_zero_of_isAdditivelyGeneratedBy {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Preadditive C] [CategoryTheory.Limits.HasFiniteBiproducts C] {P : C} (hP : ∀ (a : CategoryTheory.End P), a ≠ 0 → CategoryTheory.IsIso a) (hgen : IsAdditivelyGeneratedBy P) {X Y : C} (f : X ⟶ Y) (hf : IsRadicalMorphism f) :
        f = 0

        Every radical morphism is zero in an additive category generated by one object whose nonzero endomorphisms are all invertible.

        source
        theorem QuotientSubmoduleEquidistribution.CategoricalRadical.hasZeroRadical_of_isAdditivelyGeneratedBy {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Preadditive C] [CategoryTheory.Limits.HasFiniteBiproducts C] {P : C} (hP : ∀ (a : CategoryTheory.End P), a ≠ 0 → CategoryTheory.IsIso a) (hgen : IsAdditivelyGeneratedBy P) :
        HasZeroRadical C

        One-generator Schur data imply that the whole categorical radical is zero.