Stage detection for maps out of the unit #
The monoidal unit of the ind-category is the embedded unit, so maps out of it into filtered colimits factor through stages — the form in which the Key Lemma's colimit algebra is probed.
theorem
RS.exists_factor_of_unit_hom_colimit
{C : Type v}
[CategoryTheory.SmallCategory C]
[CategoryTheory.MonoidalCategory C]
{I : Type v}
[CategoryTheory.SmallCategory I]
[CategoryTheory.IsFiltered I]
(D : CategoryTheory.Functor I (CategoryTheory.Ind C))
(f : CategoryTheory.MonoidalCategoryStruct.tensorUnit (CategoryTheory.Ind C) ⟶ CategoryTheory.Limits.colimit D)
:
∃ (i : I) (g : CategoryTheory.MonoidalCategoryStruct.tensorUnit (CategoryTheory.Ind C) ⟶ D.obj i),
CategoryTheory.CategoryStruct.comp g (CategoryTheory.Limits.colimit.ι D i) = f
A map from the monoidal unit of the ind-category into a filtered colimit factors through a stage.
theorem
RS.unit_factor_eq_of_hom_colimit
{C : Type v}
[CategoryTheory.SmallCategory C]
[CategoryTheory.MonoidalCategory C]
{I : Type v}
[CategoryTheory.SmallCategory I]
[CategoryTheory.IsFiltered I]
(D : CategoryTheory.Functor I (CategoryTheory.Ind C))
{i j : I}
(g₁ : CategoryTheory.MonoidalCategoryStruct.tensorUnit (CategoryTheory.Ind C) ⟶ D.obj i)
(g₂ : CategoryTheory.MonoidalCategoryStruct.tensorUnit (CategoryTheory.Ind C) ⟶ D.obj j)
(h :
CategoryTheory.CategoryStruct.comp g₁ (CategoryTheory.Limits.colimit.ι D i) = CategoryTheory.CategoryStruct.comp g₂ (CategoryTheory.Limits.colimit.ι D j))
:
∃ (k : I) (α : i ⟶ k) (β : j ⟶ k),
CategoryTheory.CategoryStruct.comp g₁ (D.map α) = CategoryTheory.CategoryStruct.comp g₂ (D.map β)
Two maps from the unit merged in a filtered colimit merge at a stage.
theorem
RS.unit_colimit_eq_zero_iff
{C : Type v}
[CategoryTheory.SmallCategory C]
[CategoryTheory.MonoidalCategory C]
[CategoryTheory.Preadditive C]
[CategoryTheory.Limits.HasFiniteColimits C]
{I : Type v}
[CategoryTheory.SmallCategory I]
[CategoryTheory.IsFiltered I]
(D : CategoryTheory.Functor I (CategoryTheory.Ind C))
{i : I}
(u : CategoryTheory.MonoidalCategoryStruct.tensorUnit (CategoryTheory.Ind C) ⟶ D.obj i)
:
CategoryTheory.CategoryStruct.comp u (CategoryTheory.Limits.colimit.ι D i) = 0 ↔ ∃ (k : I) (α : i ⟶ k), CategoryTheory.CategoryStruct.comp u (D.map α) = 0
Vanishing at a stage: a unit-map's image in the colimit is zero exactly when a transition map kills it.