Strict morphisms detected by adjacent slicing hearts

For a thin slicing interval, monicity in the right adjacent heart detects a strict monomorphism, while epicity in the left adjacent heart detects a strict epimorphism. The proof transports the abelian kernel/cokernel universal property across the owner comparison isomorphisms and reflects it through the fully faithful interval embedding.

instance CategoryTheory.Triangulated.Slicing.intervalProp_isClosedUnderIsomorphisms (C : Type u) [Category.{v, u} C] [Limits.HasZeroObject C] [HasShift C ℤ] [Preadditive C] [∀ (n : ℤ), (shiftFunctor C n).Additive] [Pretriangulated C] {a b : ℝ} (s : Slicing C) : (intervalProp C s a b).IsClosedUnderIsomorphisms

Open slicing intervals are invariant under isomorphism.

theorem CategoryTheory.Triangulated.Slicing.IntervalCat.mono_toRightHeart_of_strictMono (C : Type u) [Category.{v, u} C] [Limits.HasZeroObject C] [HasShift C ℤ] [Preadditive C] [∀ (n : ℤ), (shiftFunctor C n).Additive] [Pretriangulated C] [IsTriangulated C] {a b : ℝ} [Fact (a < b)] [Fact (b - a ≤ 1)] (s : Slicing C) {X Y : IntervalCat C s a b} (f : X ⟶ Y) (hf : IsStrictMono f) : Mono ((toRightHeart C s a b ⋯).map f)

A strict monomorphism in a thin interval becomes monic in the right adjacent heart.

theorem CategoryTheory.Triangulated.Slicing.IntervalCat.strictMono_of_mono_toRightHeart (C : Type u) [Category.{v, u} C] [Limits.HasZeroObject C] [HasShift C ℤ] [Preadditive C] [∀ (n : ℤ), (shiftFunctor C n).Additive] [Pretriangulated C] [IsTriangulated C] {a b : ℝ} [Fact (a < b)] [Fact (b - a ≤ 1)] (s : Slicing C) {X Y : IntervalCat C s a b} (f : X ⟶ Y) [Mono ((toRightHeart C s a b ⋯).map f)] : IsStrictMono f

A map in a thin interval which becomes monic in the right adjacent heart is a strict monomorphism.

theorem CategoryTheory.Triangulated.Slicing.IntervalCat.epi_toLeftHeart_of_strictEpi (C : Type u) [Category.{v, u} C] [Limits.HasZeroObject C] [HasShift C ℤ] [Preadditive C] [∀ (n : ℤ), (shiftFunctor C n).Additive] [Pretriangulated C] [IsTriangulated C] {a b : ℝ} [Fact (a < b)] [Fact (b - a ≤ 1)] (s : Slicing C) {X Y : IntervalCat C s a b} (f : X ⟶ Y) (hf : IsStrictEpi f) : Epi ((toLeftHeart C s a b ⋯).map f)

A strict epimorphism in a thin interval becomes epic in the left adjacent heart.

theorem CategoryTheory.Triangulated.Slicing.IntervalCat.strictEpi_of_epi_toLeftHeart (C : Type u) [Category.{v, u} C] [Limits.HasZeroObject C] [HasShift C ℤ] [Preadditive C] [∀ (n : ℤ), (shiftFunctor C n).Additive] [Pretriangulated C] [IsTriangulated C] {a b : ℝ} [Fact (a < b)] [Fact (b - a ≤ 1)] (s : Slicing C) {X Y : IntervalCat C s a b} (f : X ⟶ Y) [Epi ((toLeftHeart C s a b ⋯).map f)] : IsStrictEpi f

A map in a thin interval which becomes epic in the left adjacent heart is a strict epimorphism.

theorem CategoryTheory.Triangulated.Slicing.IntervalCat.comp_strictEpi (C : Type u) [Category.{v, u} C] [Limits.HasZeroObject C] [HasShift C ℤ] [Preadditive C] [∀ (n : ℤ), (shiftFunctor C n).Additive] [Pretriangulated C] [IsTriangulated C] {a b : ℝ} [Fact (a < b)] [Fact (b - a ≤ 1)] (s : Slicing C) {X Y Z : IntervalCat C s a b} (f : X ⟶ Y) (g : Y ⟶ Z) (hf : IsStrictEpi f) (hg : IsStrictEpi g) : IsStrictEpi (CategoryStruct.comp f g)

Strict epimorphisms in a thin interval are closed under composition.

theorem CategoryTheory.Triangulated.Slicing.IntervalCat.strictEpi_of_comp_strictEpi (C : Type u) [Category.{v, u} C] [Limits.HasZeroObject C] [HasShift C ℤ] [Preadditive C] [∀ (n : ℤ), (shiftFunctor C n).Additive] [Pretriangulated C] [IsTriangulated C] {a b : ℝ} [Fact (a < b)] [Fact (b - a ≤ 1)] (s : Slicing C) {X Y Z : IntervalCat C s a b} (f : X ⟶ Y) (g : Y ⟶ Z) (hfg : IsStrictEpi (CategoryStruct.comp f g)) : IsStrictEpi g

If a composite is a strict epimorphism in a thin interval, then its second factor is a strict epimorphism.

theorem CategoryTheory.Triangulated.Slicing.IntervalCat.comp_strictMono (C : Type u) [Category.{v, u} C] [Limits.HasZeroObject C] [HasShift C ℤ] [Preadditive C] [∀ (n : ℤ), (shiftFunctor C n).Additive] [Pretriangulated C] [IsTriangulated C] {a b : ℝ} [Fact (a < b)] [Fact (b - a ≤ 1)] (s : Slicing C) {X Y Z : IntervalCat C s a b} (f : X ⟶ Y) (g : Y ⟶ Z) (hf : IsStrictMono f) (hg : IsStrictMono g) : IsStrictMono (CategoryStruct.comp f g)

Strict monomorphisms in a thin interval are closed under composition.

theorem CategoryTheory.Triangulated.Slicing.IntervalCat.isStrictSubobject_of_isAdmissible (C : Type u) [Category.{v, u} C] [Limits.HasZeroObject C] [HasShift C ℤ] [Preadditive C] [∀ (n : ℤ), (shiftFunctor C n).Additive] [Pretriangulated C] [IsTriangulated C] {a b : ℝ} [Fact (a < b)] [Fact (b - a ≤ 1)] (s : Slicing C) {E : IntervalCat C s a b} (A : Subobject E) (hA : IsAdmissibleSubobject C s A) : IsStrictSubobject A

The canonical arrow of an intrinsic admissible interval subobject is an owner strict monomorphism.

def CategoryTheory.Triangulated.Slicing.IntervalCat.admissibleToStrictSubobject (C : Type u) [Category.{v, u} C] [Limits.HasZeroObject C] [HasShift C ℤ] [Preadditive C] [∀ (n : ℤ), (shiftFunctor C n).Additive] [Pretriangulated C] [IsTriangulated C] {a b : ℝ} [Fact (a < b)] [Fact (b - a ≤ 1)] (s : Slicing C) (E : IntervalCat C s a b) : AdmissibleSubobject C s E ↪o StrictSubobject E

Intrinsic admissible subobjects order-embed into owner strict subobjects.

Equations

• One or more equations did not get rendered due to their size.

theorem CategoryTheory.Triangulated.Slicing.IntervalCat.isAdmissiblyArtinian_of_isStrictArtinian (C : Type u) [Category.{v, u} C] [Limits.HasZeroObject C] [HasShift C ℤ] [Preadditive C] [∀ (n : ℤ), (shiftFunctor C n).Additive] [Pretriangulated C] [IsTriangulated C] {a b : ℝ} [Fact (a < b)] [Fact (b - a ≤ 1)] (s : Slicing C) {E : IntervalCat C s a b} [IsStrictArtinianObject E] : IsAdmissiblyArtinian C s E

A strict-Artinian interval object is intrinsically admissibly Artinian.

theorem CategoryTheory.Triangulated.Slicing.IntervalCat.isAdmissiblyNoetherian_of_isStrictNoetherian (C : Type u) [Category.{v, u} C] [Limits.HasZeroObject C] [HasShift C ℤ] [Preadditive C] [∀ (n : ℤ), (shiftFunctor C n).Additive] [Pretriangulated C] [IsTriangulated C] {a b : ℝ} [Fact (a < b)] [Fact (b - a ≤ 1)] (s : Slicing C) {E : IntervalCat C s a b} [IsStrictNoetherianObject E] : IsAdmissiblyNoetherian C s E

A strict-Noetherian interval object is intrinsically admissibly Noetherian.

theorem CategoryTheory.Triangulated.Slicing.IntervalCat.isFiniteLength_of_isStrictFiniteLength (C : Type u) [Category.{v, u} C] [Limits.HasZeroObject C] [HasShift C ℤ] [Preadditive C] [∀ (n : ℤ), (shiftFunctor C n).Additive] [Pretriangulated C] [IsTriangulated C] {a b : ℝ} [Fact (a < b)] [Fact (b - a ≤ 1)] (s : Slicing C) {E : IntervalCat C s a b} (hE : IsStrictFiniteLengthObject E) : IsFiniteLength C s E

Owner strict finite length implies the intrinsic finite-length condition used by owner local finiteness.

theorem CategoryTheory.Triangulated.Slicing.IsLocallyFinite.of_strictFiniteLength (C : Type u) [Category.{v, u} C] [Limits.HasZeroObject C] [HasShift C ℤ] [Preadditive C] [∀ (n : ℤ), (shiftFunctor C n).Additive] [Pretriangulated C] [IsTriangulated C] (s : Slicing C) {η : ℝ} (hη : 0 < η) (hη' : η < 1 / 2) (hfinite : ∀ (t : ℝ) (E : IntervalCat C s (t - η) (t + η)), IsStrictFiniteLengthObject E) : IsLocallyFinite C s

A uniform strict finite-length bound on normalized thin intervals gives owner local finiteness.

theorem CategoryTheory.Triangulated.Slicing.IsLocallyFinite.of_finiteSubobjects (C : Type u) [Category.{v, u} C] [Limits.HasZeroObject C] [HasShift C ℤ] [Preadditive C] [∀ (n : ℤ), (shiftFunctor C n).Additive] [Pretriangulated C] [IsTriangulated C] (s : Slicing C) {η : ℝ} (hη : 0 < η) (hη' : η < 1 / 2) (hfinite : ∀ (t : ℝ) (E : IntervalCat C s (t - η) (t + η)), Finite (Subobject E)) : IsLocallyFinite C s

Uniform finiteness of subobject lattices on normalized thin intervals gives owner local finiteness.

theorem CategoryTheory.Triangulated.Slicing.IntervalCat.strictShortExact_of_distinguished (C : Type u) [Category.{v, u} C] [Limits.HasZeroObject C] [HasShift C ℤ] [Preadditive C] [∀ (n : ℤ), (shiftFunctor C n).Additive] [Pretriangulated C] [IsTriangulated C] {a b : ℝ} [Fact (a < b)] [Fact (b - a ≤ 1)] (s : Slicing C) {S : ShortComplex (IntervalCat C s a b)} {δ : S.X₃.obj ⟶ (shiftFunctor C 1).obj S.X₁.obj} (hT : Pretriangulated.Triangle.mk S.f.hom S.g.hom δ ∈ Pretriangulated.distinguishedTriangles) : StrictShortExact S

A distinguished ambient triangle on three thin-interval objects defines an owner strict short exact sequence in the interval category.

theorem CategoryTheory.Triangulated.Slicing.IntervalCat.exists_distinguished_of_shortExact_toLeftHeart (C : Type u) [Category.{v, u} C] [Limits.HasZeroObject C] [HasShift C ℤ] [Preadditive C] [∀ (n : ℤ), (shiftFunctor C n).Additive] [Pretriangulated C] [IsTriangulated C] {a b : ℝ} [Fact (b - a ≤ 1)] (s : Slicing C) {S : ShortComplex (IntervalCat C s a b)} (hL : (S.map (toLeftHeart C s a b ⋯)).ShortExact) : ∃ (δ : S.X₃.obj ⟶ (shiftFunctor C 1).obj S.X₁.obj), Pretriangulated.Triangle.mk S.f.hom S.g.hom δ ∈ Pretriangulated.distinguishedTriangles

A short exact sequence obtained in the left adjacent heart extends to an ambient distinguished triangle with the original interval objects.

instance CategoryTheory.Triangulated.Slicing.IntervalCat.toLeftHeart_preservesKernel (C : Type u) [Category.{v, u} C] [Limits.HasZeroObject C] [HasShift C ℤ] [Preadditive C] [∀ (n : ℤ), (shiftFunctor C n).Additive] [Pretriangulated C] [IsTriangulated C] {a b : ℝ} [Fact (a < b)] [Fact (b - a ≤ 1)] (s : Slicing C) {X Y : IntervalCat C s a b} (f : X ⟶ Y) : Limits.PreservesLimit (Limits.parallelPair f 0) (toLeftHeart C s a b ⋯)

The left adjacent-heart embedding preserves the canonical interval kernel.

instance CategoryTheory.Triangulated.Slicing.IntervalCat.toRightHeart_preservesCokernel (C : Type u) [Category.{v, u} C] [Limits.HasZeroObject C] [HasShift C ℤ] [Preadditive C] [∀ (n : ℤ), (shiftFunctor C n).Additive] [Pretriangulated C] [IsTriangulated C] {a b : ℝ} [Fact (a < b)] [Fact (b - a ≤ 1)] (s : Slicing C) {X Y : IntervalCat C s a b} (f : X ⟶ Y) : Limits.PreservesColimit (Limits.parallelPair f 0) (toRightHeart C s a b ⋯)

The right adjacent-heart embedding preserves the canonical interval cokernel.

theorem CategoryTheory.Triangulated.Slicing.IntervalCat.exists_distinguished_of_strictShortExact (C : Type u) [Category.{v, u} C] [Limits.HasZeroObject C] [HasShift C ℤ] [Preadditive C] [∀ (n : ℤ), (shiftFunctor C n).Additive] [Pretriangulated C] [IsTriangulated C] {a b : ℝ} [Fact (a < b)] [Fact (b - a ≤ 1)] (s : Slicing C) {S : ShortComplex (IntervalCat C s a b)} (hS : StrictShortExact S) : ∃ (δ : S.X₃.obj ⟶ (shiftFunctor C 1).obj S.X₁.obj), Pretriangulated.Triangle.mk S.f.hom S.g.hom δ ∈ Pretriangulated.distinguishedTriangles

An owner strict short exact sequence in a thin interval extends to an ambient distinguished triangle.

theorem CategoryTheory.Triangulated.Slicing.IntervalCat.strictShortExact_iff_exists_distinguished (C : Type u) [Category.{v, u} C] [Limits.HasZeroObject C] [HasShift C ℤ] [Preadditive C] [∀ (n : ℤ), (shiftFunctor C n).Additive] [Pretriangulated C] [IsTriangulated C] {a b : ℝ} [Fact (a < b)] [Fact (b - a ≤ 1)] (s : Slicing C) {S : ShortComplex (IntervalCat C s a b)} : StrictShortExact S ↔ ∃ (δ : S.X₃.obj ⟶ (shiftFunctor C 1).obj S.X₁.obj), Pretriangulated.Triangle.mk S.f.hom S.g.hom δ ∈ Pretriangulated.distinguishedTriangles

Owner strict short exact sequences in a thin interval are exactly the short complexes whose ambient maps extend to a distinguished triangle.

theorem CategoryTheory.Triangulated.Slicing.IntervalCat.K₀_of_strictShortExact (C : Type u) [Category.{v, u} C] [Limits.HasZeroObject C] [HasShift C ℤ] [Preadditive C] [∀ (n : ℤ), (shiftFunctor C n).Additive] [Pretriangulated C] [IsTriangulated C] {a b : ℝ} [Fact (a < b)] [Fact (b - a ≤ 1)] (s : Slicing C) {S : ShortComplex (IntervalCat C s a b)} (hS : StrictShortExact S) : K₀.of C S.X₂.obj = K₀.of C S.X₁.obj + K₀.of C S.X₃.obj

A strict short exact sequence in a thin interval supplies the expected ambient owner Grothendieck-group relation.

@[reducible, inline]

abbrev CategoryTheory.Triangulated.Slicing.IntervalCat.inclusion (C : Type u) [Category.{v, u} C] [Limits.HasZeroObject C] [HasShift C ℤ] [Preadditive C] [∀ (n : ℤ), (shiftFunctor C n).Additive] [Pretriangulated C] {a b : ℝ} (s : Slicing C) {a₂ b₂ : ℝ} (ha : a₂ ≤ a) (hb : b ≤ b₂) : Functor (IntervalCat C s a b) (IntervalCat C s a₂ b₂)

The fully faithful inclusion from a thin interval into a wider interval.

Equations

• CategoryTheory.Triangulated.Slicing.IntervalCat.inclusion C s ha hb = CategoryTheory.ObjectProperty.ιOfLE ⋯

theorem CategoryTheory.Triangulated.Slicing.IntervalCat.strictShortExact_inclusion (C : Type u) [Category.{v, u} C] [Limits.HasZeroObject C] [HasShift C ℤ] [Preadditive C] [∀ (n : ℤ), (shiftFunctor C n).Additive] [Pretriangulated C] [IsTriangulated C] {a b : ℝ} [Fact (a < b)] [Fact (b - a ≤ 1)] (s : Slicing C) {a₂ b₂ : ℝ} [Fact (a₂ < b₂)] [Fact (b₂ - a₂ ≤ 1)] (ha : a₂ ≤ a) (hb : b ≤ b₂) {S : ShortComplex (IntervalCat C s a b)} (hS : StrictShortExact S) : StrictShortExact (S.map (inclusion C s ha hb))

A strict short exact sequence remains strict short exact after widening the ambient thin interval.

noncomputable def CategoryTheory.Triangulated.HNFiltration.appendStrictFactor (C : Type u) [Category.{v, u} C] [Limits.HasZeroObject C] [HasShift C ℤ] [Preadditive C] [∀ (n : ℤ), (shiftFunctor C n).Additive] [Pretriangulated C] [IsTriangulated C] {a b : ℝ} [Fact (a < b)] [Fact (b - a ≤ 1)] {P : ℝ → ObjectProperty C} {s : Slicing C} {S : ShortComplex (Slicing.IntervalCat C s a b)} (G : HNFiltration C P S.X₁.obj) (hS : StrictShortExact S) (ψ : ℝ) (hψ : P ψ S.X₃.obj) (hψ_lt : ∀ (j : Fin G.n), ψ < G.φ j) : HNFiltration C P S.X₂.obj

Append a semistable strict quotient to an owner HN filtration of the kernel object in a thin interval.

Equations

• One or more equations did not get rendered due to their size.

instance CategoryTheory.Triangulated.Slicing.intervalProp_isClosedUnderBinaryProducts (C : Type u) [Category.{v, u} C] [Limits.HasZeroObject C] [HasShift C ℤ] [Preadditive C] [∀ (n : ℤ), (shiftFunctor C n).Additive] [Pretriangulated C] {a b : ℝ} (s : Slicing C) : (intervalProp C s a b).IsClosedUnderBinaryProducts

Open slicing intervals are closed under binary products.

instance CategoryTheory.Triangulated.Slicing.intervalProp_isClosedUnderFiniteProducts (C : Type u) [Category.{v, u} C] [Limits.HasZeroObject C] [HasShift C ℤ] [Preadditive C] [∀ (n : ℤ), (shiftFunctor C n).Additive] [Pretriangulated C] {a b : ℝ} (s : Slicing C) : (intervalProp C s a b).IsClosedUnderFiniteProducts

Open slicing intervals are closed under finite products.

instance CategoryTheory.Triangulated.Slicing.intervalCat_hasFiniteProducts (C : Type u) [Category.{v, u} C] [Limits.HasZeroObject C] [HasShift C ℤ] [Preadditive C] [∀ (n : ℤ), (shiftFunctor C n).Additive] [Pretriangulated C] {a b : ℝ} (s : Slicing C) : Limits.HasFiniteProducts (IntervalCat C s a b)

Thin interval categories have finite products.

instance CategoryTheory.Triangulated.Slicing.intervalCat_hasBinaryBiproducts (C : Type u) [Category.{v, u} C] [Limits.HasZeroObject C] [HasShift C ℤ] [Preadditive C] [∀ (n : ℤ), (shiftFunctor C n).Additive] [Pretriangulated C] {a b : ℝ} (s : Slicing C) : Limits.HasBinaryBiproducts (IntervalCat C s a b)

Thin interval categories have binary biproducts.

instance CategoryTheory.Triangulated.Slicing.intervalCat_hasFiniteBiproducts (C : Type u) [Category.{v, u} C] [Limits.HasZeroObject C] [HasShift C ℤ] [Preadditive C] [∀ (n : ℤ), (shiftFunctor C n).Additive] [Pretriangulated C] {a b : ℝ} (s : Slicing C) : Limits.HasFiniteBiproducts (IntervalCat C s a b)

Thin interval categories have finite biproducts.

instance CategoryTheory.Triangulated.Slicing.intervalCat_hasEqualizers (C : Type u) [Category.{v, u} C] [Limits.HasZeroObject C] [HasShift C ℤ] [Preadditive C] [∀ (n : ℤ), (shiftFunctor C n).Additive] [Pretriangulated C] [IsTriangulated C] {a b : ℝ} [Fact (a < b)] [Fact (b - a ≤ 1)] (s : Slicing C) : Limits.HasEqualizers (IntervalCat C s a b)

Thin interval categories have equalizers.

instance CategoryTheory.Triangulated.Slicing.intervalCat_hasCoequalizers (C : Type u) [Category.{v, u} C] [Limits.HasZeroObject C] [HasShift C ℤ] [Preadditive C] [∀ (n : ℤ), (shiftFunctor C n).Additive] [Pretriangulated C] [IsTriangulated C] {a b : ℝ} [Fact (a < b)] [Fact (b - a ≤ 1)] (s : Slicing C) : Limits.HasCoequalizers (IntervalCat C s a b)

Thin interval categories have coequalizers.

instance CategoryTheory.Triangulated.Slicing.intervalCat_hasPullbacks (C : Type u) [Category.{v, u} C] [Limits.HasZeroObject C] [HasShift C ℤ] [Preadditive C] [∀ (n : ℤ), (shiftFunctor C n).Additive] [Pretriangulated C] [IsTriangulated C] {a b : ℝ} [Fact (a < b)] [Fact (b - a ≤ 1)] (s : Slicing C) : Limits.HasPullbacks (IntervalCat C s a b)

Thin interval categories have pullbacks.

instance CategoryTheory.Triangulated.Slicing.intervalCat_hasPushouts (C : Type u) [Category.{v, u} C] [Limits.HasZeroObject C] [HasShift C ℤ] [Preadditive C] [∀ (n : ℤ), (shiftFunctor C n).Additive] [Pretriangulated C] [IsTriangulated C] {a b : ℝ} [Fact (a < b)] [Fact (b - a ≤ 1)] (s : Slicing C) : Limits.HasPushouts (IntervalCat C s a b)

Thin interval categories have pushouts.

instance CategoryTheory.Triangulated.Slicing.IntervalCat.toLeftHeart_preservesFiniteLimits (C : Type u) [Category.{v, u} C] [Limits.HasZeroObject C] [HasShift C ℤ] [Preadditive C] [∀ (n : ℤ), (shiftFunctor C n).Additive] [Pretriangulated C] [IsTriangulated C] {a b : ℝ} [Fact (a < b)] [Fact (b - a ≤ 1)] (s : Slicing C) : Limits.PreservesFiniteLimits (toLeftHeart C s a b ⋯)

The left adjacent-heart embedding preserves finite limits.

instance CategoryTheory.Triangulated.Slicing.IntervalCat.toRightHeart_preservesFiniteColimits (C : Type u) [Category.{v, u} C] [Limits.HasZeroObject C] [HasShift C ℤ] [Preadditive C] [∀ (n : ℤ), (shiftFunctor C n).Additive] [Pretriangulated C] [IsTriangulated C] {a b : ℝ} [Fact (a < b)] [Fact (b - a ≤ 1)] (s : Slicing C) : Limits.PreservesFiniteColimits (toRightHeart C s a b ⋯)

The right adjacent-heart embedding preserves finite colimits.

theorem CategoryTheory.Triangulated.Slicing.IntervalCat.finite_subobject_of_leftHeart (C : Type u) [Category.{v, u} C] [Limits.HasZeroObject C] [HasShift C ℤ] [Preadditive C] [∀ (n : ℤ), (shiftFunctor C n).Additive] [Pretriangulated C] [IsTriangulated C] {a b : ℝ} [Fact (a < b)] [Fact (b - a ≤ 1)] (s : Slicing C) {X : IntervalCat C s a b} (hX : Finite (Subobject ((toLeftHeart C s a b ⋯).obj X))) : Finite (Subobject X)

Finiteness of the subobject lattice in the left adjacent heart descends to the thin interval category.

theorem CategoryTheory.Triangulated.Slicing.IntervalCat.isArtinianObject_of_leftHeart (C : Type u) [Category.{v, u} C] [Limits.HasZeroObject C] [HasShift C ℤ] [Preadditive C] [∀ (n : ℤ), (shiftFunctor C n).Additive] [Pretriangulated C] [IsTriangulated C] {a b : ℝ} [Fact (a < b)] [Fact (b - a ≤ 1)] (s : Slicing C) {X : IntervalCat C s a b} [IsArtinianObject ((toLeftHeart C s a b ⋯).obj X)] : IsArtinianObject X

An Artinian object in the left adjacent heart is Artinian in the thin interval category.

theorem CategoryTheory.Triangulated.Slicing.IntervalCat.isNoetherianObject_of_leftHeart (C : Type u) [Category.{v, u} C] [Limits.HasZeroObject C] [HasShift C ℤ] [Preadditive C] [∀ (n : ℤ), (shiftFunctor C n).Additive] [Pretriangulated C] [IsTriangulated C] {a b : ℝ} [Fact (a < b)] [Fact (b - a ≤ 1)] (s : Slicing C) {X : IntervalCat C s a b} [IsNoetherianObject ((toLeftHeart C s a b ⋯).obj X)] : IsNoetherianObject X

A Noetherian object in the left adjacent heart is Noetherian in the thin interval category.

theorem CategoryTheory.Triangulated.Slicing.IntervalCat.isStrictArtinianObject_of_rightHeart (C : Type u) [Category.{v, u} C] [Limits.HasZeroObject C] [HasShift C ℤ] [Preadditive C] [∀ (n : ℤ), (shiftFunctor C n).Additive] [Pretriangulated C] [IsTriangulated C] {a b : ℝ} [Fact (a < b)] [Fact (b - a ≤ 1)] (s : Slicing C) {X : IntervalCat C s a b} [IsArtinianObject ((toRightHeart C s a b ⋯).obj X)] : IsStrictArtinianObject X

An Artinian object in the right adjacent heart is strict-Artinian in the thin interval category.

theorem CategoryTheory.Triangulated.Slicing.IntervalCat.isStrictNoetherianObject_of_rightHeart (C : Type u) [Category.{v, u} C] [Limits.HasZeroObject C] [HasShift C ℤ] [Preadditive C] [∀ (n : ℤ), (shiftFunctor C n).Additive] [Pretriangulated C] [IsTriangulated C] {a b : ℝ} [Fact (a < b)] [Fact (b - a ≤ 1)] (s : Slicing C) {X : IntervalCat C s a b} [IsNoetherianObject ((toRightHeart C s a b ⋯).obj X)] : IsStrictNoetherianObject X

A Noetherian object in the right adjacent heart is strict-Noetherian in the thin interval category.

instance CategoryTheory.Triangulated.Slicing.intervalCat_quasiAbelian (C : Type u) [Category.{v, u} C] [Limits.HasZeroObject C] [HasShift C ℤ] [Preadditive C] [∀ (n : ℤ), (shiftFunctor C n).Additive] [Pretriangulated C] [IsTriangulated C] {a b : ℝ} [Fact (a < b)] [Fact (b - a ≤ 1)] (s : Slicing C) : QuasiAbelian (IntervalCat C s a b)

A thin owner slicing interval is quasi-abelian.