instHasTotalIntObjUpShiftFunctor₂

English

The shifted first-index functor preserves totality: applying the shift by x to a K with HasTotal, yields a new object with HasTotal in the up-shifted index.

Русский

Сдвиг по первой оси сохраняет свойство полного комплекса: применяя сдвиг на x к K с HasTotal, получаем новый объект с HasTotal в обновлённом индексе.

LaTeX

$$$((\\text{shiftFunctor}_1 C x).obj K).HasTotal (up\\;\\mathbb{Z})$$$

Lean4

instance : ((shiftFunctor₂ C y).obj K).HasTotal (up ℤ) := fun n =>
  hasCoproduct_of_equiv_of_iso (K.toGradedObject.mapObjFun (π (up ℤ) (up ℤ) (up ℤ)) (n + y)) _
    { toFun := fun ⟨⟨a, b⟩, h⟩ =>
        ⟨⟨a, b + y⟩, by
          simp only [Set.mem_preimage, π_def, Set.mem_singleton_iff] at h ⊢
          cutsat⟩
      invFun := fun ⟨⟨a, b⟩, h⟩ =>
        ⟨(a, b - y), by
          simp only [Set.mem_preimage, π_def, Set.mem_singleton_iff] at h ⊢
          cutsat⟩
      left_inv _ := by simp
      right_inv _ := by simp } (fun _ => Iso.refl _)

Похожие утверждения