Documentation

DerivedAlgGeo.CategoryTheory.Abelian.Stability.Subobject

Subobject lemmas for owner stability functions #

These are the categorical primitives needed by the owner HN existence and uniqueness arguments in the repository-owned stability-function API.

source
theorem CategoryTheory.Triangulated.StabilityFunction.shortExact_of_mono {A : Type u} [Category.{v, u} A] [Abelian A] {X Y : A} (f : X ⟶ Y) [Mono f] :
{ X₁ := X, X₂ := Y, X₃ := Limits.cokernel f, f := f, g := Limits.cokernel.π f, zero := ⋯ }.ShortExact

The canonical cokernel sequence of a monomorphism is short exact.

source
@[simp]
theorem CategoryTheory.Triangulated.StabilityFunction.subobject_isZero_iff_eq_bot {A : Type u} [Category.{v, u} A] [Abelian A] {E : A} (B : Subobject E) :
Limits.IsZero (Subobject.underlying.obj B) ↔ B = ⊥

A subobject has zero underlying object exactly when it is bottom.

source
theorem CategoryTheory.Triangulated.StabilityFunction.subobject_ne_bot_of_not_isZero {A : Type u} [Category.{v, u} A] [Abelian A] {E : A} {B : Subobject E} (hB : ¬Limits.IsZero (Subobject.underlying.obj B)) :
B ≠ ⊥

A nonzero subobject is not bottom.

source
theorem CategoryTheory.Triangulated.StabilityFunction.subobject_not_isZero_of_ne_bot {A : Type u} [Category.{v, u} A] [Abelian A] {E : A} {B : Subobject E} (hB : B ≠ ⊥) :
¬Limits.IsZero (Subobject.underlying.obj B)

A subobject distinct from bottom has nonzero underlying object.

source
theorem CategoryTheory.Triangulated.StabilityFunction.subobject_top_ne_bot_of_not_isZero {A : Type u} [Category.{v, u} A] [Abelian A] {E : A} (hE : ¬Limits.IsZero E) :
⊤ ≠ ⊥

The top and bottom subobjects of a nonzero object differ.

source
@[simp]
theorem CategoryTheory.Triangulated.StabilityFunction.subobject_ofLE_bot {A : Type u} [Category.{v, u} A] [Abelian A] {E : A} (S : Subobject E) (h : ⊥ ≤ S) :
⊥.ofLE S h = 0

The inclusion from the bottom subobject is the zero morphism.

source
noncomputable def CategoryTheory.Triangulated.StabilityFunction.subobjectCokernelBotIso {A : Type u} [Category.{v, u} A] [Abelian A] {E : A} (S : Subobject E) (h : ⊥ ≤ S) :
Limits.cokernel (⊥.ofLE S h) ≅ Subobject.underlying.obj S

The cokernel of the inclusion from bottom is the target subobject.

Equations
Instances For
    source
    theorem CategoryTheory.Triangulated.StabilityFunction.cokernel_not_isZero_of_ne_top {A : Type u} [Category.{v, u} A] [Abelian A] {E : A} {B : Subobject E} (hB : B ≠ ⊤) :
    ¬Limits.IsZero (Limits.cokernel B.arrow)

    A proper subobject of an abelian object has nonzero cokernel.

    source
    theorem CategoryTheory.Triangulated.StabilityFunction.imageSubobject_epi_comp {A : Type u} [Category.{v, u} A] [Abelian A] {X Y Z : A} (e : X ⟶ Y) [Epi e] (f : Y ⟶ Z) :
    Limits.imageSubobject (CategoryStruct.comp e f) = Limits.imageSubobject f

    Precomposing a morphism by an epimorphism does not change its image subobject in an abelian category.

    source
    theorem CategoryTheory.Triangulated.StabilityFunction.imageSubobject_eq_top_of_epi {A : Type u} [Category.{v, u} A] [Abelian A] {X Y : A} (f : X ⟶ Y) [Epi f] :
    Limits.imageSubobject f = ⊤

    The image subobject of an epimorphism is top.

    source
    theorem CategoryTheory.Triangulated.StabilityFunction.pullback_obj_injective_of_epi {A : Type u} [Category.{v, u} A] [Abelian A] {X Y : A} (p : X ⟶ Y) [Epi p] :
    Function.Injective (Subobject.pullback p).obj

    Pullback along an epimorphism is injective on subobjects.