Finite support for maps out of compact objects

This file turns the additive-group formulation of compactness into the finite-support statement used by Brown's mapping-telescope construction. A morphism from a compact object into a coproduct is a finite sum of component morphisms followed by the coproduct injections.

The proof identifies a coproduct of additive commutative groups with the concrete direct sum. This bridge is kept private: the exported theorem is stated entirely in the ambient preadditive category.

noncomputable def CategoryTheory.directSumToHom {C : Type u} [Category.{v, u} C] [Preadditive C] (K : C) {ι : Type} [DecidableEq ι] (X : ι → C) [Limits.HasCoproduct X] : (DirectSum ι fun (i : ι) => K ⟶ X i) →+ (K ⟶ ∐ X)

The comparison map from the direct sum of the Hom groups into the summands to the Hom group into the coproduct: (aᵢ) ↦ ∑ aᵢ ≫ ιᵢ. Compactness of K in the indexing universe Type is bijectivity of this map for every coproduct, see isCompactObject_iff_bijective_directSumToHom.

Equations

• CategoryTheory.directSumToHom K X = DirectSum.toAddMonoid fun (i : ι) => CategoryTheory.Preadditive.rightComp K (CategoryTheory.Limits.Sigma.ι X i)

@[simp]

theorem CategoryTheory.directSumToHom_of {C : Type u} [Category.{v, u} C] [Preadditive C] (K : C) {ι : Type} [DecidableEq ι] (X : ι → C) [Limits.HasCoproduct X] (i : ι) (a : K ⟶ X i) : (directSumToHom K X) ((DirectSum.of (fun (i : ι) => K ⟶ X i) i) a) = CategoryStruct.comp a (Limits.Sigma.ι X i)

noncomputable def CategoryTheory.directSumPrecomp {C : Type u} [Category.{v, u} C] [Preadditive C] {K : C} {ι : Type} (X : ι → C) {L : C} (f : K ⟶ L) : (DirectSum ι fun (i : ι) => L ⟶ X i) →+ DirectSum ι fun (i : ι) => K ⟶ X i

Precomposition with f on every summand of the direct sum of Hom groups.

Equations

• CategoryTheory.directSumPrecomp X f = DirectSum.map fun (i : ι) => CategoryTheory.Preadditive.leftComp (X i) f

@[simp]

theorem CategoryTheory.directSumPrecomp_apply {C : Type u} [Category.{v, u} C] [Preadditive C] {K : C} {ι : Type} (X : ι → C) {L : C} (f : K ⟶ L) (x : DirectSum ι fun (i : ι) => L ⟶ X i) (i : ι) : ((directSumPrecomp X f) x) i = CategoryStruct.comp f (x i)

theorem CategoryTheory.directSumPrecomp_comp {C : Type u} [Category.{v, u} C] [Preadditive C] {K : C} {ι : Type} (X : ι → C) {L M : C} (f : K ⟶ L) (g : L ⟶ M) (x : DirectSum ι fun (i : ι) => M ⟶ X i) : (directSumPrecomp X f) ((directSumPrecomp X g) x) = (directSumPrecomp X (CategoryStruct.comp f g)) x

theorem CategoryTheory.directSumPrecomp_id {C : Type u} [Category.{v, u} C] [Preadditive C] {K : C} {ι : Type} (X : ι → C) (x : DirectSum ι fun (i : ι) => K ⟶ X i) : (directSumPrecomp X (CategoryStruct.id K)) x = x

theorem CategoryTheory.directSumToHom_precomp {C : Type u} [Category.{v, u} C] [Preadditive C] {K : C} {ι : Type} [DecidableEq ι] (X : ι → C) [Limits.HasCoproduct X] {L : C} (f : K ⟶ L) (x : DirectSum ι fun (i : ι) => L ⟶ X i) : (directSumToHom K X) ((directSumPrecomp X f) x) = CategoryStruct.comp f ((directSumToHom L X) x)

The comparison map is natural in the source object.

theorem CategoryTheory.IsCompactObject.bijective_directSumToHom {C : Type u} [Category.{v, u} C] [Preadditive C] {K : C} {ι : Type} [DecidableEq ι] (X : ι → C) [Limits.HasCoproduct X] (hK : IsCompactObject K) : Function.Bijective ⇑(directSumToHom K X)

Compact objects have bijective comparison maps.

theorem CategoryTheory.isCompactObject_of_bijective_directSumToHom {C : Type u} [Category.{v, u} C] [Preadditive C] {K : C} (h : ∀ (ι : Type) [inst : DecidableEq ι] (X : ι → C) [inst_1 : Limits.HasCoproduct X], Function.Bijective ⇑(directSumToHom K X)) : IsCompactObject K

Bijective comparison maps give compactness.

theorem CategoryTheory.isCompactObject_iff_bijective_directSumToHom {C : Type u} [Category.{v, u} C] [Preadditive C] {K : C} : IsCompactObject K ↔ ∀ (ι : Type) [inst : DecidableEq ι] (X : ι → C) [inst_1 : Limits.HasCoproduct X], Function.Bijective ⇑(directSumToHom K X)

Compactness in the indexing universe Type is bijectivity of the direct-sum comparison map for every Type-indexed coproduct.

theorem CategoryTheory.IsCompactObject.exists_finite_sum {C : Type u} [Category.{v, u} C] [Preadditive C] {K : C} (hK : IsCompactObject K) {ι : Type} (X : ι → C) [Limits.HasCoproduct X] (f : K ⟶ ∐ X) : ∃ (s : Finset ι) (g : (i : ι) → K ⟶ X i), f = ∑ i ∈ s, CategoryStruct.comp (g i) (Limits.Sigma.ι X i)

A morphism from a compact object into a coproduct is a finite sum of morphisms into individual summands followed by the coproduct injections.