Magnitude conjecture

QuotientSubmoduleEquidistribution.CategoryTheory.IdealQuotient

Ideal quotients of preadditive categories #

Mathlib supplies quotients by a categorical congruence. This file packages a two-sided additive Hom ideal as such a congruence, equips the quotient with its induced preadditive structure, and proves that the quotient functor kills exactly the ideal.

source
def QuotientSubmoduleEquidistribution.CategoricalIdeal.HomIdeal.rel {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Preadditive C] (I : HomIdeal C) :
HomRel C

Congruence modulo the given Hom ideal.

Instances For
    source
    instance QuotientSubmoduleEquidistribution.CategoricalIdeal.HomIdeal.instCongruenceRel {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Preadditive C] (I : HomIdeal C) :
    CategoryTheory.Congruence I.rel
    source
    theorem QuotientSubmoduleEquidistribution.CategoricalIdeal.HomIdeal.add_compatible {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Preadditive C] (I : HomIdeal C) {X Y : C} (f₁ f₂ g₁ g₂ : X ⟶ Y) (hf : I.rel f₁ f₂) (hg : I.rel g₁ g₂) :
    I.rel (f₁ + g₁) (f₂ + g₂)
    source
    @[reducible, inline]
    abbrev QuotientSubmoduleEquidistribution.CategoricalIdeal.HomIdeal.quotientPreadditive {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Preadditive C] (I : HomIdeal C) :
    CategoryTheory.Preadditive (CategoryTheory.Quotient I.rel)

    The induced preadditive structure on the category quotient.

    Instances For
      source
      theorem QuotientSubmoduleEquidistribution.CategoricalIdeal.HomIdeal.map_eq_zero_iff {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Preadditive C] (I : HomIdeal C) {X Y : C} (f : X ⟶ Y) :
      (CategoryTheory.Quotient.functor I.rel).map f = 0 ↔ f ∈ I.hom X Y

      The quotient functor kills exactly the given Hom ideal.

      source
      theorem QuotientSubmoduleEquidistribution.CategoricalIdeal.HomIdeal.map_isRadicalMorphism {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Preadditive C] (I : HomIdeal C) {X Y : C} (f : X ⟶ Y) (hf : CategoricalRadical.IsRadicalMorphism f) :
      CategoricalRadical.IsRadicalMorphism ((CategoryTheory.Quotient.functor I.rel).map f)

      The quotient functor sends categorical radical morphisms to categorical radical morphisms.

      source
      theorem QuotientSubmoduleEquidistribution.CategoricalIdeal.HomIdeal.mem_of_isRadicalMorphism_of_quotient_hasZeroRadical {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Preadditive C] (I : HomIdeal C) {X Y : C} (f : X ⟶ Y) (hzero : CategoricalRadical.HasZeroRadical (CategoryTheory.Quotient I.rel)) (hf : CategoricalRadical.IsRadicalMorphism f) :
      f ∈ I.hom X Y

      If the quotient has zero categorical radical, every radical morphism upstairs belongs to the defining Hom ideal.