Strict finite length along inclusions of owner slicing intervals

This is the foundation-level transfer needed by deformation local finiteness. It embeds strict-subobject orders along a full faithful interval inclusion and pulls both well-foundedness conditions back.

noncomputable def CategoryTheory.Triangulated.strictImage {A : Type u} [Category.{v, u} A] [Preadditive A] [Limits.HasKernels A] [Limits.HasCokernels A] {D : Type u'} [Category.{v', u'} D] [Preadditive D] [Limits.HasKernels D] [Limits.HasCokernels D] (F : Functor A D) (hF : ∀ {X Y : A} (f : X ⟶ Y), IsStrictMono f → IsStrictMono (F.map f)) (harr : ∀ {Y Z : D} (f : Y ⟶ Z) [inst : Mono f], IsStrictMono f → IsStrictMono (Subobject.mk f).arrow) {E : A} : StrictSubobject E → StrictSubobject (F.obj E)

The image of a strict subobject, landing in strict subobjects — which is what lets the hypothesis be strict rather than ordinary.

Fullness and faithfulness are omitted: the construction and its monotonicity need only that F preserves strict monos. They enter only through strictImage_injective, and a functor that is not full can still obtain strict monotonicity of the image map by other means — see Slicing.PreimageData.strictImage_strictMono in Phase/Transfer/LocallyFinite.lean, which uses reflection of isomorphisms.

Equations

• CategoryTheory.Triangulated.strictImage F hF harr B = ⟨CategoryTheory.Subobject.mk (F.map (↑B).arrow), ⋯⟩

theorem CategoryTheory.Triangulated.strictImage_monotone {A : Type u} [Category.{v, u} A] [Preadditive A] [Limits.HasKernels A] [Limits.HasCokernels A] {D : Type u'} [Category.{v', u'} D] [Preadditive D] [Limits.HasKernels D] [Limits.HasCokernels D] (F : Functor A D) (hF : ∀ {X Y : A} (f : X ⟶ Y), IsStrictMono f → IsStrictMono (F.map f)) (harr : ∀ {Y Z : D} (f : Y ⟶ Z) [inst : Mono f], IsStrictMono f → IsStrictMono (Subobject.mk f).arrow) {E : A} : Monotone (strictImage F ⋯ ⋯)

theorem CategoryTheory.Triangulated.strictImage_injective {A : Type u} [Category.{v, u} A] [Preadditive A] [Limits.HasKernels A] [Limits.HasCokernels A] {D : Type u'} [Category.{v', u'} D] [Preadditive D] [Limits.HasKernels D] [Limits.HasCokernels D] (F : Functor A D) [F.Full] [F.Faithful] (hF : ∀ {X Y : A} (f : X ⟶ Y), IsStrictMono f → IsStrictMono (F.map f)) (harr : ∀ {Y Z : D} (f : Y ⟶ Z) [inst : Mono f], IsStrictMono f → IsStrictMono (Subobject.mk f).arrow) {E : A} : Function.Injective (strictImage F ⋯ ⋯)

theorem CategoryTheory.Triangulated.strictImage_strictMono {A : Type u} [Category.{v, u} A] [Preadditive A] [Limits.HasKernels A] [Limits.HasCokernels A] {D : Type u'} [Category.{v', u'} D] [Preadditive D] [Limits.HasKernels D] [Limits.HasCokernels D] (F : Functor A D) [F.Full] [F.Faithful] (hF : ∀ {X Y : A} (f : X ⟶ Y), IsStrictMono f → IsStrictMono (F.map f)) (harr : ∀ {Y Z : D} (f : Y ⟶ Z) [inst : Mono f], IsStrictMono f → IsStrictMono (Subobject.mk f).arrow) {E : A} {a b : StrictSubobject E} (hab : a < b) : strictImage F ⋯ ⋯ a < strictImage F ⋯ ⋯ b

Monotone + injective on a partial order is strictly monotone, which is what pulls well-foundedness back.

theorem CategoryTheory.Triangulated.isStrictArtinianObject_of_strictMono {A : Type u} [Category.{v, u} A] [Preadditive A] [Limits.HasKernels A] [Limits.HasCokernels A] {D : Type u'} [Category.{v', u'} D] [Preadditive D] [Limits.HasKernels D] [Limits.HasCokernels D] {X : A} {Y : D} (G : StrictSubobject X → StrictSubobject Y) (hG : StrictMono G) [IsStrictArtinianObject Y] : IsStrictArtinianObject X

The strict-Artinian condition descends along any strictly monotone map of strict subobjects. This is the whole content of the well-foundedness transfer: the descending chain condition on StrictSubobject Y pulls back through G by InvImage.wf, whatever produced G. Stated for a bare map so that a functor which is not full, and so cannot use strictImage_injective, can still discharge it once it has strict monotonicity by another route.

theorem CategoryTheory.Triangulated.isStrictNoetherianObject_of_strictMono {A : Type u} [Category.{v, u} A] [Preadditive A] [Limits.HasKernels A] [Limits.HasCokernels A] {D : Type u'} [Category.{v', u'} D] [Preadditive D] [Limits.HasKernels D] [Limits.HasCokernels D] {X : A} {Y : D} (G : StrictSubobject X → StrictSubobject Y) (hG : StrictMono G) [IsStrictNoetherianObject Y] : IsStrictNoetherianObject X

The strict-Noetherian condition descends along any strictly monotone map of strict subobjects, by the same argument with the order reversed.

theorem CategoryTheory.Triangulated.intervalInclusion_map_strictMono (C : Type u) [Category.{v, u} C] [Limits.HasZeroObject C] [HasShift C ℤ] [Preadditive C] [∀ (n : ℤ), (shiftFunctor C n).Additive] [Pretriangulated C] [IsTriangulated C] {s₁ s₂ : Slicing C} {a₁ b₁ a₂ b₂ : ℝ} [Fact (a₁ < b₁)] [Fact (b₁ - a₁ ≤ 1)] [Fact (a₂ < b₂)] [Fact (b₂ - a₂ ≤ 1)] (h : Slicing.intervalProp C s₁ a₁ b₁ ≤ Slicing.intervalProp C s₂ a₂ b₂) {X Y : Slicing.IntervalCat C s₁ a₁ b₁} (f : X ⟶ Y) (hf : IsStrictMono f) : IsStrictMono ((ObjectProperty.ιOfLE h).map f)

Inclusion of one thin owner interval in another preserves strict monomorphisms.

theorem CategoryTheory.Triangulated.intervalSubobject_arrow_strictMono (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} {a b : ℝ} [Fact (a < b)] [Fact (b - a ≤ 1)] {X Y : Slicing.IntervalCat C s a b} (f : X ⟶ Y) [Mono f] (hf : IsStrictMono f) : IsStrictMono (Subobject.mk f).arrow

The canonical representative arrow of a strict interval subobject is strict.

theorem CategoryTheory.Triangulated.interval_strictFiniteLength_of_inclusion (C : Type u) [Category.{v, u} C] [Limits.HasZeroObject C] [HasShift C ℤ] [Preadditive C] [∀ (n : ℤ), (shiftFunctor C n).Additive] [Pretriangulated C] [IsTriangulated C] {s₁ s₂ : Slicing C} {a₁ b₁ a₂ b₂ : ℝ} [Fact (a₁ < b₁)] [Fact (b₁ - a₁ ≤ 1)] [Fact (a₂ < b₂)] [Fact (b₂ - a₂ ≤ 1)] (h : Slicing.intervalProp C s₁ a₁ b₁ ≤ Slicing.intervalProp C s₂ a₂ b₂) (hFinite : ∀ (Y : Slicing.IntervalCat C s₂ a₂ b₂), IsStrictArtinianObject Y ∧ IsStrictNoetherianObject Y) (X : Slicing.IntervalCat C s₁ a₁ b₁) : IsStrictArtinianObject X ∧ IsStrictNoetherianObject X

Strict finite length pulls back along an inclusion of thin owner slicing intervals.