Magnitude conjecture

MagnitudeConjecture.CategoryTheory.HomIdealComap

Pullback of categorical Hom ideals #

An additive functor pulls a two-sided additive Hom ideal back along its Hom maps. Ideal powers in the pullback map into the corresponding powers downstairs. For a fully faithful additive functor, categorical-radical membership is equivalent before and after applying the functor.

source
def QuotientSubmoduleEquidistribution.CategoricalIdeal.HomIdeal.comap {C : Type u} {D : Type v} [CategoryTheory.Category.{w, u} C] [CategoryTheory.Category.{w, v} D] [CategoryTheory.Preadditive C] [CategoryTheory.Preadditive D] (F : CategoryTheory.Functor C D) [F.Additive] (I : HomIdeal D) :
HomIdeal C

Pull a Hom ideal back along an additive functor.

Instances For
    source
    @[simp]
    theorem QuotientSubmoduleEquidistribution.CategoricalIdeal.HomIdeal.mem_comap_iff {C : Type u} {D : Type v} [CategoryTheory.Category.{w, u} C] [CategoryTheory.Category.{w, v} D] [CategoryTheory.Preadditive C] [CategoryTheory.Preadditive D] (F : CategoryTheory.Functor C D) [F.Additive] (I : HomIdeal D) {X Y : C} (f : X ⟶ Y) :
    f ∈ (comap F I).hom X Y ↔ F.map f ∈ I.hom (F.obj X) (F.obj Y)
    source
    theorem QuotientSubmoduleEquidistribution.CategoricalIdeal.HomIdeal.map_mem_pow_of_mem_comap_pow {C : Type u} {D : Type v} [CategoryTheory.Category.{w, u} C] [CategoryTheory.Category.{w, v} D] [CategoryTheory.Preadditive C] [CategoryTheory.Preadditive D] (F : CategoryTheory.Functor C D) [F.Additive] (I : HomIdeal D) (n : ℕ) {X Y : C} {f : X ⟶ Y} :
    f ∈ ((comap F I).pow n).hom X Y → F.map f ∈ (I.pow n).hom (F.obj X) (F.obj Y)

    A morphism in a power of a pulled-back ideal maps into the same power of the original ideal.

    source
    theorem QuotientSubmoduleEquidistribution.CategoricalIdeal.HomIdeal.pow_add {C : Type u} [CategoryTheory.Category.{w, u} C] [CategoryTheory.Preadditive C] (I : HomIdeal C) (m n : ℕ) :
    I.pow (m + n) = I.pow m ⋆ᵢ I.pow n

    Powers of a Hom ideal add their exponents under ideal multiplication.

    source
    def QuotientSubmoduleEquidistribution.CategoricalIdeal.HomIdeal.homSubmodule {C : Type u} [CategoryTheory.Category.{w, u} C] [CategoryTheory.Preadditive C] {k : Type u_1} [Semiring k] [CategoryTheory.Linear k C] (I : HomIdeal C) (X Y : C) :
    Submodule k (X ⟶ Y)

    A Hom ideal in a linear category, regarded pointwise as a linear submodule.

    Instances For
      source
      @[simp]
      theorem QuotientSubmoduleEquidistribution.CategoricalIdeal.HomIdeal.mem_homSubmodule_iff {C : Type u} [CategoryTheory.Category.{w, u} C] [CategoryTheory.Preadditive C] {k : Type u_1} [Semiring k] [CategoryTheory.Linear k C] (I : HomIdeal C) (X Y : C) (f : X ⟶ Y) :
      f ∈ I.homSubmodule X Y ↔ f ∈ I.hom X Y
      source
      theorem MagnitudeConjecture.isRadicalMorphism_iff_map_of_fullyFaithful {C : Type u} {D : Type v} [CategoryTheory.Category.{w, u} C] [CategoryTheory.Category.{w, v} D] [CategoryTheory.Preadditive C] [CategoryTheory.Preadditive D] (F : CategoryTheory.Functor C D) [F.Additive] (hF : F.FullyFaithful) {X Y : C} (f : X ⟶ Y) :
      QuotientSubmoduleEquidistribution.CategoricalRadical.IsRadicalMorphism f ↔ QuotientSubmoduleEquidistribution.CategoricalRadical.IsRadicalMorphism (F.map f)

      A fully faithful additive functor preserves and reflects categorical radical morphisms between objects in its image.