Quotients of countably presented ind-objects

RS.CountablyPresented — a countable filtered colimit of embedded objects — is the shape in which "built from countably much data" enters the dimension count of RS.Classical.Deligne.GammaCountable. This file shows the notion stable under quotients: an epimorphic image of a countably presented ind-object is countably presented (RS.CountablyPresented.of_epi), over the same finite length hypothesis that discharges RS.IndImageEmbedded.

The argument. Write Z as the colimit of a countable filtered diagram D of embedded objects and let p : Z ⟶ Q be an epimorphism. The composites of the colimit inclusions with p form a family RS.quotientStage of maps into Q, compatible with the structural maps of D, and the images of its members assemble into a diagram RS.imageDiag — functorially, because such a family is a diagram in the arrow category and the image is a functor on the arrow category (CategoryTheory.Limits.im).

The colimit of that diagram is Q itself (RS.exists_iso_colimit_imageDiag). It maps to Q by the image inclusions; the map is a monomorphism because filtered colimits are exact in the ind-completion, so colim preserves monomorphisms (CategoryTheory.Limits.colim.map_mono' over the AB5 property of Ind C), and an epimorphism because the members of the family are jointly epimorphic (RS.quotientStage_jointly_epi) and each factors through its image.

Finite length makes each of those images embedded (RS.indImageEmbedded_of_lengthLE), and a diagram of ind-objects all of whose values are embedded is the embedding of a diagram in the base category (RS.liftEmbedded), which is what RS.CountablyPresented asks for.

The dimension counts the descent consumes follow: the even component of a countably presented ind-object is of at most countable dimension (RS.rank_hom_unit_le_aleph0_of_presented), and hence so is that of any of its quotients (RS.rank_hom_unit_le_aleph0_of_epi).

Lifting a diagram of embedded objects

A diagram of ind-objects whose values are all embedded is the embedding of a diagram in the base category: the structural maps are transported through the full faithfulness of RS.indOf.

noncomputable def RS.liftEmbedded {C : Type v} [CategoryTheory.SmallCategory C] {I : Type v} [CategoryTheory.SmallCategory I] (F : CategoryTheory.Functor I (CategoryTheory.Ind C)) (W : I → C) (θ : (i : I) → F.obj i ≅ indOf.obj (W i)) : CategoryTheory.Functor I C

A diagram of embedded objects comes from the base category: the chosen isomorphisms transport the structural maps down through the full faithfulness of the embedding.

Equations

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

noncomputable def RS.liftEmbeddedIso {C : Type v} [CategoryTheory.SmallCategory C] {I : Type v} [CategoryTheory.SmallCategory I] (F : CategoryTheory.Functor I (CategoryTheory.Ind C)) (W : I → C) (θ : (i : I) → F.obj i ≅ indOf.obj (W i)) : (liftEmbedded F W θ).comp indOf ≅ F

The lifted diagram embeds back to the diagram it was lifted from.

Equations

• RS.liftEmbeddedIso F W θ = CategoryTheory.NatIso.ofComponents (fun (i : I) => (θ i).symm) ⋯

The diagram of images

A compatible family of maps into a fixed object is a diagram in the arrow category, and the image is a functor on the arrow category (CategoryTheory.Limits.im), so the images of the members of the family form a diagram again.

noncomputable def RS.arrowDiagram {C : Type v} [CategoryTheory.SmallCategory C] {I : Type v} [CategoryTheory.SmallCategory I] {D : CategoryTheory.Functor I (CategoryTheory.Ind C)} {Q : CategoryTheory.Ind C} (f : (i : I) → D.obj i ⟶ Q) (hf : ∀ (i j : I) (α : i ⟶ j), CategoryTheory.CategoryStruct.comp (D.map α) (f j) = f i) : CategoryTheory.Functor I (CategoryTheory.Arrow (CategoryTheory.Ind C))

A compatible family of maps into a fixed object, read as a diagram in the arrow category.

Equations

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

noncomputable def RS.imageDiag {C : Type v} [CategoryTheory.SmallCategory C] [CategoryTheory.Abelian C] {I : Type v} [CategoryTheory.SmallCategory I] {D : CategoryTheory.Functor I (CategoryTheory.Ind C)} {Q : CategoryTheory.Ind C} (f : (i : I) → D.obj i ⟶ Q) (hf : ∀ (i j : I) (α : i ⟶ j), CategoryTheory.CategoryStruct.comp (D.map α) (f j) = f i) : CategoryTheory.Functor I (CategoryTheory.Ind C)

The diagram of images of a compatible family of maps into a fixed object.

Equations

• RS.imageDiag f hf = (RS.arrowDiagram f hf).comp CategoryTheory.Limits.im

noncomputable def RS.imageDiagHom {C : Type v} [CategoryTheory.SmallCategory C] [CategoryTheory.Abelian C] {I : Type v} [CategoryTheory.SmallCategory I] {D : CategoryTheory.Functor I (CategoryTheory.Ind C)} {Q : CategoryTheory.Ind C} (f : (i : I) → D.obj i ⟶ Q) (hf : ∀ (i j : I) (α : i ⟶ j), CategoryTheory.CategoryStruct.comp (D.map α) (f j) = f i) : imageDiag f hf ⟶ (CategoryTheory.Functor.const I).obj Q

The image inclusions, as a map into the constant diagram.

Equations

• RS.imageDiagHom f hf = { app := fun (i : I) => CategoryTheory.Limits.image.ι (f i), naturality := ⋯ }

noncomputable def RS.imageColimitDesc {C : Type v} [CategoryTheory.SmallCategory C] [CategoryTheory.Abelian C] {I : Type v} [CategoryTheory.SmallCategory I] {D : CategoryTheory.Functor I (CategoryTheory.Ind C)} {Q : CategoryTheory.Ind C} [CategoryTheory.IsFiltered I] (f : (i : I) → D.obj i ⟶ Q) (hf : ∀ (i j : I) (α : i ⟶ j), CategoryTheory.CategoryStruct.comp (D.map α) (f j) = f i) : CategoryTheory.Limits.colimit (imageDiag f hf) ⟶ Q

The map from the colimit of the images to the common target.

Equations

• RS.imageColimitDesc f hf = CategoryTheory.Limits.colimit.desc (RS.imageDiag f hf) { pt := Q, ι := RS.imageDiagHom f hf }

theorem RS.ι_imageColimitDesc {C : Type v} [CategoryTheory.SmallCategory C] [CategoryTheory.Abelian C] {I : Type v} [CategoryTheory.SmallCategory I] {D : CategoryTheory.Functor I (CategoryTheory.Ind C)} {Q : CategoryTheory.Ind C} [CategoryTheory.IsFiltered I] (f : (i : I) → D.obj i ⟶ Q) (hf : ∀ (i j : I) (α : i ⟶ j), CategoryTheory.CategoryStruct.comp (D.map α) (f j) = f i) (i : I) : CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.colimit.ι (imageDiag f hf) i) (imageColimitDesc f hf) = CategoryTheory.Limits.image.ι (f i)

theorem RS.exists_iso_colimit_imageDiag {C : Type v} [CategoryTheory.SmallCategory C] [CategoryTheory.Abelian C] {I : Type v} [CategoryTheory.SmallCategory I] {D : CategoryTheory.Functor I (CategoryTheory.Ind C)} {Q : CategoryTheory.Ind C} [CategoryTheory.IsFiltered I] (f : (i : I) → D.obj i ⟶ Q) (hf : ∀ (i j : I) (α : i ⟶ j), CategoryTheory.CategoryStruct.comp (D.map α) (f j) = f i) (hepi : ∀ {T : CategoryTheory.Ind C} (a b : Q ⟶ T), (∀ (i : I), CategoryTheory.CategoryStruct.comp (f i) a = CategoryTheory.CategoryStruct.comp (f i) b) → a = b) : Nonempty (Q ≅ CategoryTheory.Limits.colimit (imageDiag f hf))

The images of a jointly epimorphic filtered family exhaust their target. The map from the colimit of the images is a monomorphism because filtered colimits are exact in the ind-completion, and an epimorphism because every member of the family factors through its image.

The quotient of a countably presented ind-object

noncomputable def RS.quotientStage {C : Type v} [CategoryTheory.SmallCategory C] {I : Type v} [CategoryTheory.SmallCategory I] [CategoryTheory.IsFiltered I] {D : CategoryTheory.Functor I (CategoryTheory.Ind C)} {Z Q : CategoryTheory.Ind C} (e : Z ≅ CategoryTheory.Limits.colimit D) (p : Z ⟶ Q) (i : I) : D.obj i ⟶ Q

The stages of a presentation of Z, followed by a map out of Z.

Equations

• RS.quotientStage e p i = CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.colimit.ι D i) (CategoryTheory.CategoryStruct.comp e.inv p)

theorem RS.quotientStage_comp {C : Type v} [CategoryTheory.SmallCategory C] {I : Type v} [CategoryTheory.SmallCategory I] [CategoryTheory.IsFiltered I] {D : CategoryTheory.Functor I (CategoryTheory.Ind C)} {Z Q : CategoryTheory.Ind C} (e : Z ≅ CategoryTheory.Limits.colimit D) (p : Z ⟶ Q) (i j : I) (α : i ⟶ j) : CategoryTheory.CategoryStruct.comp (D.map α) (quotientStage e p j) = quotientStage e p i

The stages are compatible with the structural maps of the presentation.

theorem RS.quotientStage_jointly_epi {C : Type v} [CategoryTheory.SmallCategory C] {I : Type v} [CategoryTheory.SmallCategory I] [CategoryTheory.IsFiltered I] {D : CategoryTheory.Functor I (CategoryTheory.Ind C)} {Z Q : CategoryTheory.Ind C} (e : Z ≅ CategoryTheory.Limits.colimit D) (p : Z ⟶ Q) [CategoryTheory.Epi p] {T : CategoryTheory.Ind C} (a b : Q ⟶ T) (h : ∀ (i : I), CategoryTheory.CategoryStruct.comp (quotientStage e p i) a = CategoryTheory.CategoryStruct.comp (quotientStage e p i) b) : a = b

The stages of a presentation, followed by an epimorphism, are jointly epimorphic.

theorem RS.CountablyPresented.of_epi {C : Type v} [CategoryTheory.SmallCategory C] [CategoryTheory.Abelian C] (hlen : ∀ (Z : C), ∃ (N : ℕ), LengthLE Z N) {Z Q : CategoryTheory.Ind C} (p : Z ⟶ Q) [CategoryTheory.Epi p] (h : CountablyPresented Z) : CountablyPresented Q

A quotient of a countably presented ind-object is countably presented. Finite length makes the images of the stages embedded, and those images exhaust the quotient.

The dimension counts

The even component of a countably presented ind-object is a countable union of even components of embedded objects, hence of at most countable dimension; the same then holds for every quotient.

theorem RS.rank_hom_unit_le_aleph0_of_presented {C : Type v} [CategoryTheory.SmallCategory C] [CategoryTheory.MonoidalCategory C] [CategoryTheory.Abelian C] [CategoryTheory.Linear ℂ C] [CategoryTheory.MonoidalPreadditive C] [CategoryTheory.RigidCategory C] [CategoryTheory.Linear ℂ (CategoryTheory.Ind C)] (hu : HasScalarUnit C) (hsmul : IndOfLinear C) (hlen : ∀ (Z : C), ∃ (N : ℕ), LengthLE Z N) {Z : CategoryTheory.Ind C} (h : CountablyPresented Z) : Module.rank ℂ (CategoryTheory.MonoidalCategoryStruct.tensorUnit (CategoryTheory.Ind C) ⟶ Z) ≤ Cardinal.aleph0

A countably presented ind-object has countable even component: it is a countable filtered colimit of embedded objects, each of which has finite dimensional even component by finite length.

theorem RS.rank_hom_unit_le_aleph0_of_epi {C : Type v} [CategoryTheory.SmallCategory C] [CategoryTheory.MonoidalCategory C] [CategoryTheory.Abelian C] [CategoryTheory.Linear ℂ C] [CategoryTheory.MonoidalPreadditive C] [CategoryTheory.RigidCategory C] [CategoryTheory.Linear ℂ (CategoryTheory.Ind C)] (hu : HasScalarUnit C) (hsmul : IndOfLinear C) (hlen : ∀ (Z : C), ∃ (N : ℕ), LengthLE Z N) {Z Q : CategoryTheory.Ind C} (p : Z ⟶ Q) [CategoryTheory.Epi p] (h : CountablyPresented Z) : Module.rank ℂ (CategoryTheory.MonoidalCategoryStruct.tensorUnit (CategoryTheory.Ind C) ⟶ Q) ≤ Cardinal.aleph0

A quotient of a countably presented ind-object has countable even component. This is the form in which the countable descent consumes RS.CountablyPresented.of_epi.