Nonvanishing of the unit along a chain colimit

For a chain of objects of the ind-category with compatible maps from the monoidal unit, the image of the unit in the colimit vanishes exactly when it dies at a finite stage. This is the form in which the Key Lemma's colimit algebra is shown nonzero: the δ-transitions carry the unit forward, and stage detection reduces vanishing in the colimit to vanishing at a stage. The chain is indexed by a universe-lifted copy of ℕ, the shape at which the ind-category is known to have filtered colimits.

@[reducible, inline]

abbrev RS.SmallNat : Type v

A v-small copy of the natural numbers.

Equations

• RS.SmallNat = CategoryTheory.ULiftHom (ULift.{?u.1, 0} ℕ)

noncomputable def RS.smallNatEquiv : ℕ ≌ SmallNat

The equivalence between ℕ and its v-small copy.

Equations

• RS.smallNatEquiv = CategoryTheory.ULiftHomULiftCategory.equiv ℕ

instance RS.instIsFilteredSmallNat : CategoryTheory.IsFiltered SmallNat

theorem RS.unit_chainMap {C : Type v} [CategoryTheory.SmallCategory C] [CategoryTheory.MonoidalCategory C] (B : ℕ → CategoryTheory.Ind C) (δ : (n : ℕ) → B n ⟶ B (n + 1)) (u : (n : ℕ) → CategoryTheory.MonoidalCategoryStruct.tensorUnit (CategoryTheory.Ind C) ⟶ B n) (hu : ∀ (n : ℕ), CategoryTheory.CategoryStruct.comp (u n) (δ n) = u (n + 1)) {m n : ℕ} (h : m ≤ n) : CategoryTheory.CategoryStruct.comp (u m) (chainMap B δ h) = u n

Compatible unit maps ride along the chain morphisms.

noncomputable def RS.chainFunctorSmall {C : Type v} [CategoryTheory.SmallCategory C] (B : ℕ → CategoryTheory.Ind C) (δ : (n : ℕ) → B n ⟶ B (n + 1)) : CategoryTheory.Functor SmallNat (CategoryTheory.Ind C)

The chain functor over the v-small copy of ℕ.

Equations

• RS.chainFunctorSmall B δ = RS.smallNatEquiv.inverse.comp (RS.chainFunctor B δ)

theorem RS.unit_chain_colimit_eq_zero_iff {C : Type v} [CategoryTheory.SmallCategory C] [CategoryTheory.MonoidalCategory C] [CategoryTheory.Preadditive C] [CategoryTheory.Limits.HasFiniteColimits C] (B : ℕ → CategoryTheory.Ind C) (δ : (n : ℕ) → B n ⟶ B (n + 1)) (u : (n : ℕ) → CategoryTheory.MonoidalCategoryStruct.tensorUnit (CategoryTheory.Ind C) ⟶ B n) (hu : ∀ (n : ℕ), CategoryTheory.CategoryStruct.comp (u n) (δ n) = u (n + 1)) (m : ℕ) : CategoryTheory.CategoryStruct.comp (u m) (CategoryTheory.Limits.colimit.ι (chainFunctorSmall B δ) (smallNatEquiv.functor.obj m)) = 0 ↔ ∃ (n : ℕ), u n = 0

Nonvanishing of the unit in a chain colimit: with compatible unit maps along the chain, the image of the unit in the colimit is zero exactly when the unit dies at some stage.