Documentation

TauCeti.CategoryTheory.ObjectProperty.KilledBy

Objects killed by a natural number #

In a preadditive category, a natural number e kills an object Z when e • 𝟙 Z = 0. The objects killed by e form an object property, CategoryTheory.ObjectProperty.isKilledBy C e, closed under subobjects and quotients: if e kills W, it kills every subobject and every quotient of W. In a category of modules this is the condition that e annihilates every element.

source
def CategoryTheory.ObjectProperty.isKilledBy (C : Type u_1) [Category.{v_1, u_1} C] [Preadditive C] (e : ℕ) :
ObjectProperty C

The objects Z killed by a natural number e, in the sense that e • 𝟙 Z = 0.

Instances For
    source
    @[simp]
    theorem CategoryTheory.ObjectProperty.prop_isKilledBy_iff {C : Type u_1} [Category.{v_1, u_1} C] [Preadditive C] (e : ℕ) (Z : C) :
    isKilledBy C e Z ↔ e • CategoryStruct.id Z = 0

    An object Z is killed by e exactly when e • 𝟙 Z = 0.

    source
    instance CategoryTheory.ObjectProperty.instIsClosedUnderSubobjectsIsKilledBy {C : Type u_1} [Category.{v_1, u_1} C] [Preadditive C] (e : ℕ) :
    (isKilledBy C e).IsClosedUnderSubobjects

    A subobject of an object killed by e is killed by e.

    source
    instance CategoryTheory.ObjectProperty.instIsClosedUnderQuotientsIsKilledBy {C : Type u_1} [Category.{v_1, u_1} C] [Preadditive C] (e : ℕ) :
    (isKilledBy C e).IsClosedUnderQuotients

    A quotient of an object killed by e is killed by e.