Embedded images from finite length

RS.IndImageEmbedded — the image in Ind C of a map out of an embedded object is again embedded — is carried as a hypothesis by RS.Classical.Deligne.CountableDescent and discharged here from finite length: if every object of C carries a bound on the length of the chains in its subobject order, then every such image is embedded.

The argument. A map f : indOf.obj Y ⟶ Z factors through a stage of the chosen presentation of Z (RS.exists_presStage_factor), say as indOf.map g ≫ presStage Z i. The stage may be advanced along any α : i ⟶ j, and advancing it only enlarges the kernel of the composite g ≫ F.map α in the subobject order of Y. Finite length makes that order satisfy the ascending chain condition (RS.exists_maximal_of_lengthLE), so the kernel may be taken maximal, at a stage j₀; write g₀ for the map to that stage.

Maximality says that no further advance of the stage enlarges the kernel, and that is exactly what makes the image of g₀ embed into Z: the map indOf.map (image.ι g₀) ≫ presStage Z j₀ is a monomorphism. Monomorphisms of ind-objects are detected on the embedded objects (RS.mono_of_hom_indOf_injective), the detection brings the question back to a single stage of the presentation, and there RS.mono_of_kernelSubobject_comp_le settles it inside C. The embedding preserves finite colimits, so the other half of the factorisation of g₀ stays an epimorphism, and f acquires a strong epi–mono factorisation through indOf.obj (image g₀); uniqueness of such factorisations identifies the image of f with it.

Finite length is the ascending chain condition

RS.LengthLE Y N forbids strictly increasing chains of N + 2 subobjects of Y. A family of subobjects without a maximal member would generate an infinite strictly increasing chain, so it forbids that too.

theorem RS.exists_maximal_of_lengthLE {C : Type u} [CategoryTheory.Category.{w, u} C] {Y : C} {N : ℕ} (hY : LengthLE Y N) {S : Set (CategoryTheory.Subobject Y)} (hS : S.Nonempty) : ∃ P ∈ S, ∀ Q ∈ S, P ≤ Q → Q ≤ P

Finite length gives maximal members: if the subobject order of Y carries no strictly increasing chain of N + 2 terms, then every nonempty family of subobjects of Y has a maximal member.

The stable-kernel criterion for a monomorphism

A map f followed by g has a kernel at least that of f. When the two kernels agree, the mono half of the image factorisation of f survives postcomposition with g: the kernel of image.ι f ≫ g is pulled back along the epi half to the common kernel, and an epimorphism cancels.

theorem RS.kernelSubobject_le_comp {C : Type u} [CategoryTheory.Category.{w, u} C] [CategoryTheory.Abelian C] {X Y Z : C} (f : X ⟶ Y) (g : Y ⟶ Z) : CategoryTheory.Limits.kernelSubobject f ≤ CategoryTheory.Limits.kernelSubobject (CategoryTheory.CategoryStruct.comp f g)

Postcomposition only enlarges the kernel.

theorem RS.mono_of_kernelSubobject_comp_le {C : Type u} [CategoryTheory.Category.{w, u} C] [CategoryTheory.Abelian C] {X Y Z : C} (f : X ⟶ Y) (g : Y ⟶ Z) (h : CategoryTheory.Limits.kernelSubobject (CategoryTheory.CategoryStruct.comp f g) ≤ CategoryTheory.Limits.kernelSubobject f) : CategoryTheory.Mono (CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.image.ι f) g)

The stable-kernel criterion: if postcomposing f with g does not enlarge the kernel of f, then the mono half of the image factorisation of f remains a monomorphism after postcomposition with g.

Embedded images

The main theorem: finite length discharges RS.IndImageEmbedded.

theorem RS.exists_stage_comp_eq_of_presStage {C : Type v} [CategoryTheory.SmallCategory C] {Z : CategoryTheory.Ind C} {W : C} {j : Z.presentation.I} (a b : indOf.obj W ⟶ indOf.obj (Z.presentation.F.obj j)) (hab : CategoryTheory.CategoryStruct.comp a (presStage Z j) = CategoryTheory.CategoryStruct.comp b (presStage Z j)) : ∃ (k : Z.presentation.I) (β : j ⟶ k), CategoryTheory.CategoryStruct.comp a (indOf.map (Z.presentation.F.map β)) = CategoryTheory.CategoryStruct.comp b (indOf.map (Z.presentation.F.map β))

Two maps out of an embedded object into a stage of the presentation of an ind-object which agree in the ind-object already agree at a later stage — the merging half of compactness, read at the structural maps of the presentation.

theorem RS.indImageEmbedded_of_lengthLE {C : Type v} [CategoryTheory.SmallCategory C] [CategoryTheory.Abelian C] (hlen : ∀ (Z : C), ∃ (N : ℕ), LengthLE Z N) : IndImageEmbedded C

Embedded images from finite length. If every object of C has a bound on the length of the chains in its subobject order, then the image in Ind C of a map out of an embedded object is again embedded.