Shifting a chain colimit by one stage

Dropping the bottom stage of a chain does not change its colimit. The stage inclusions of the full chain restrict to a cocone on the shifted chain, giving the tail comparison; the transitions followed by the shifted stage inclusions form a cocone on the full chain, giving the comparison back. Both composites are identified with the identities by the stagewise extensionality lemma. The descent-from-legs helper chainDesc is factored out for reuse: any family of legs absorbed by the transitions descends to the chain colimit, with the stage computation exposed as a simp lemma.

theorem RS.chainMap_legs {E : Type u} [CategoryTheory.Category.{v, u} E] (B : ℕ → E) (δ : (n : ℕ) → B n ⟶ B (n + 1)) {Z : E} (legs : (n : ℕ) → B n ⟶ Z) (h : ∀ (n : ℕ), CategoryTheory.CategoryStruct.comp (δ n) (legs (n + 1)) = legs n) {a b : ℕ} (hab : a ≤ b) : CategoryTheory.CategoryStruct.comp (chainMap B δ hab) (legs b) = legs a

Legs absorbed by the transitions absorb all chain morphisms.

noncomputable def RS.chainCocone {E : Type u} [CategoryTheory.Category.{v, u} E] (B : ℕ → E) (δ : (n : ℕ) → B n ⟶ B (n + 1)) {Z : E} (legs : (n : ℕ) → B n ⟶ Z) (h : ∀ (n : ℕ), CategoryTheory.CategoryStruct.comp (δ n) (legs (n + 1)) = legs n) : CategoryTheory.Limits.Cocone (chainDiagram B δ)

The cocone on the chain diagram assembled from legs absorbed by the transitions.

Equations

• RS.chainCocone B δ legs h = { pt := Z, ι := { app := fun (k : RS.SmallNat) => legs (RS.smallNatEquiv.inverse.obj k), naturality := ⋯ } }

noncomputable def RS.chainDesc {E : Type u} [CategoryTheory.Category.{v, u} E] (B : ℕ → E) (δ : (n : ℕ) → B n ⟶ B (n + 1)) [CategoryTheory.Limits.HasColimitsOfShape SmallNat E] {Z : E} (legs : (n : ℕ) → B n ⟶ Z) (h : ∀ (n : ℕ), CategoryTheory.CategoryStruct.comp (δ n) (legs (n + 1)) = legs n) : chainColimit B δ ⟶ Z

The descent out of the chain colimit determined by legs absorbed by the transitions.

Equations

• RS.chainDesc B δ legs h = CategoryTheory.Limits.colimit.desc (RS.chainDiagram B δ) (RS.chainCocone B δ legs h)

@[simp]

theorem RS.ι_chainDesc {E : Type u} [CategoryTheory.Category.{v, u} E] (B : ℕ → E) (δ : (n : ℕ) → B n ⟶ B (n + 1)) [CategoryTheory.Limits.HasColimitsOfShape SmallNat E] {Z : E} (legs : (n : ℕ) → B n ⟶ Z) (h : ∀ (n : ℕ), CategoryTheory.CategoryStruct.comp (δ n) (legs (n + 1)) = legs n) (n : ℕ) : CategoryTheory.CategoryStruct.comp (chainColimitι B δ n) (chainDesc B δ legs h) = legs n

On a stage, the descent is the corresponding leg.

@[simp]

theorem RS.ι_chainDesc_assoc {E : Type u} [CategoryTheory.Category.{v, u} E] (B : ℕ → E) (δ : (n : ℕ) → B n ⟶ B (n + 1)) [CategoryTheory.Limits.HasColimitsOfShape SmallNat E] {Z : E} (legs : (n : ℕ) → B n ⟶ Z) (h : ∀ (n : ℕ), CategoryTheory.CategoryStruct.comp (δ n) (legs (n + 1)) = legs n) (n : ℕ) {Z✝ : E} (h✝ : Z ⟶ Z✝) : CategoryTheory.CategoryStruct.comp (chainColimitι B δ n) (CategoryTheory.CategoryStruct.comp (chainDesc B δ legs h) h✝) = CategoryTheory.CategoryStruct.comp (legs n) h✝

On a stage, the descent is the corresponding leg.

noncomputable def RS.chainColimitTail {E : Type u} [CategoryTheory.Category.{v, u} E] (B : ℕ → E) (δ : (n : ℕ) → B n ⟶ B (n + 1)) [CategoryTheory.Limits.HasColimitsOfShape SmallNat E] : (chainColimit (fun (k : ℕ) => B (k + 1)) fun (k : ℕ) => δ (k + 1)) ⟶ chainColimit B δ

The comparison from the colimit of the shifted chain, whose leg at a stage is the next stage inclusion of the full chain.

Equations

• RS.chainColimitTail B δ = RS.chainDesc (fun (k : ℕ) => B (k + 1)) (fun (k : ℕ) => δ (k + 1)) (fun (k : ℕ) => RS.chainColimitι B δ (k + 1)) ⋯

@[simp]

theorem RS.ι_chainColimitTail {E : Type u} [CategoryTheory.Category.{v, u} E] (B : ℕ → E) (δ : (n : ℕ) → B n ⟶ B (n + 1)) [CategoryTheory.Limits.HasColimitsOfShape SmallNat E] (k : ℕ) : CategoryTheory.CategoryStruct.comp (chainColimitι (fun (k : ℕ) => B (k + 1)) (fun (k : ℕ) => δ (k + 1)) k) (chainColimitTail B δ) = chainColimitι B δ (k + 1)

On a stage, the tail comparison is the next stage inclusion.

@[simp]

theorem RS.ι_chainColimitTail_assoc {E : Type u} [CategoryTheory.Category.{v, u} E] (B : ℕ → E) (δ : (n : ℕ) → B n ⟶ B (n + 1)) [CategoryTheory.Limits.HasColimitsOfShape SmallNat E] (k : ℕ) {Z : E} (h : chainColimit B δ ⟶ Z) : CategoryTheory.CategoryStruct.comp (chainColimitι (fun (k : ℕ) => B (k + 1)) (fun (k : ℕ) => δ (k + 1)) k) (CategoryTheory.CategoryStruct.comp (chainColimitTail B δ) h) = CategoryTheory.CategoryStruct.comp (chainColimitι B δ (k + 1)) h

On a stage, the tail comparison is the next stage inclusion.

noncomputable def RS.chainColimitUntail {E : Type u} [CategoryTheory.Category.{v, u} E] (B : ℕ → E) (δ : (n : ℕ) → B n ⟶ B (n + 1)) [CategoryTheory.Limits.HasColimitsOfShape SmallNat E] : chainColimit B δ ⟶ chainColimit (fun (k : ℕ) => B (k + 1)) fun (k : ℕ) => δ (k + 1)

The comparison to the colimit of the shifted chain, whose leg at a stage is the transition followed by the shifted inclusion.

Equations

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

@[simp]

theorem RS.ι_chainColimitUntail {E : Type u} [CategoryTheory.Category.{v, u} E] (B : ℕ → E) (δ : (n : ℕ) → B n ⟶ B (n + 1)) [CategoryTheory.Limits.HasColimitsOfShape SmallNat E] (k : ℕ) : CategoryTheory.CategoryStruct.comp (chainColimitι B δ k) (chainColimitUntail B δ) = CategoryTheory.CategoryStruct.comp (δ k) (chainColimitι (fun (k : ℕ) => B (k + 1)) (fun (k : ℕ) => δ (k + 1)) k)

On a stage, the comparison to the shifted colimit is the transition followed by the shifted inclusion.

@[simp]

theorem RS.ι_chainColimitUntail_assoc {E : Type u} [CategoryTheory.Category.{v, u} E] (B : ℕ → E) (δ : (n : ℕ) → B n ⟶ B (n + 1)) [CategoryTheory.Limits.HasColimitsOfShape SmallNat E] (k : ℕ) {Z : E} (h : (chainColimit (fun (k : ℕ) => B (k + 1)) fun (k : ℕ) => δ (k + 1)) ⟶ Z) : CategoryTheory.CategoryStruct.comp (chainColimitι B δ k) (CategoryTheory.CategoryStruct.comp (chainColimitUntail B δ) h) = CategoryTheory.CategoryStruct.comp (δ k) (CategoryTheory.CategoryStruct.comp (chainColimitι (fun (k : ℕ) => B (k + 1)) (fun (k : ℕ) => δ (k + 1)) k) h)

On a stage, the comparison to the shifted colimit is the transition followed by the shifted inclusion.

noncomputable def RS.chainColimitTailIso {E : Type u} [CategoryTheory.Category.{v, u} E] (B : ℕ → E) (δ : (n : ℕ) → B n ⟶ B (n + 1)) [CategoryTheory.Limits.HasColimitsOfShape SmallNat E] : (chainColimit (fun (k : ℕ) => B (k + 1)) fun (k : ℕ) => δ (k + 1)) ≅ chainColimit B δ

Dropping the bottom stage of a chain does not change the colimit.

Equations

• RS.chainColimitTailIso B δ = { hom := RS.chainColimitTail B δ, inv := RS.chainColimitUntail B δ, hom_inv_id := ⋯, inv_hom_id := ⋯ }

noncomputable def RS.chainColimitMapIso {E : Type u} [CategoryTheory.Category.{v, u} E] (B : ℕ → E) (δ : (n : ℕ) → B n ⟶ B (n + 1)) [CategoryTheory.Limits.HasColimitsOfShape SmallNat E] {C : ℕ → E} (δC : (n : ℕ) → C n ⟶ C (n + 1)) (φ : (n : ℕ) → B n ≅ C n) (hφ : ∀ (n : ℕ), CategoryTheory.CategoryStruct.comp (δ n) (φ (n + 1)).hom = CategoryTheory.CategoryStruct.comp (φ n).hom (δC n)) : chainColimit B δ ≅ chainColimit C δC

The chain colimit is invariant under stagewise isomorphism: compatible stage isomorphisms induce an isomorphism of the chain colimits.

Equations

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

@[simp]

theorem RS.ι_chainColimitMapIso_hom {E : Type u} [CategoryTheory.Category.{v, u} E] (B : ℕ → E) (δ : (n : ℕ) → B n ⟶ B (n + 1)) [CategoryTheory.Limits.HasColimitsOfShape SmallNat E] {C : ℕ → E} (δC : (n : ℕ) → C n ⟶ C (n + 1)) (φ : (n : ℕ) → B n ≅ C n) (hφ : ∀ (n : ℕ), CategoryTheory.CategoryStruct.comp (δ n) (φ (n + 1)).hom = CategoryTheory.CategoryStruct.comp (φ n).hom (δC n)) (n : ℕ) : CategoryTheory.CategoryStruct.comp (chainColimitι B δ n) (chainColimitMapIso B δ δC φ hφ).hom = CategoryTheory.CategoryStruct.comp (φ n).hom (chainColimitι C δC n)

The stage insertions under the stagewise isomorphism.

@[simp]

theorem RS.ι_chainColimitMapIso_hom_assoc {E : Type u} [CategoryTheory.Category.{v, u} E] (B : ℕ → E) (δ : (n : ℕ) → B n ⟶ B (n + 1)) [CategoryTheory.Limits.HasColimitsOfShape SmallNat E] {C : ℕ → E} (δC : (n : ℕ) → C n ⟶ C (n + 1)) (φ : (n : ℕ) → B n ≅ C n) (hφ : ∀ (n : ℕ), CategoryTheory.CategoryStruct.comp (δ n) (φ (n + 1)).hom = CategoryTheory.CategoryStruct.comp (φ n).hom (δC n)) (n : ℕ) {Z : E} (h : chainColimit C δC ⟶ Z) : CategoryTheory.CategoryStruct.comp (chainColimitι B δ n) (CategoryTheory.CategoryStruct.comp (chainColimitMapIso B δ δC φ hφ).hom h) = CategoryTheory.CategoryStruct.comp (φ n).hom (CategoryTheory.CategoryStruct.comp (chainColimitι C δC n) h)

The stage insertions under the stagewise isomorphism.