Theorems · Theorem · category theory

CategoryTheory.Limits.SequentialProduct.functorMap_commSq_succ

∀ {C : Type u_1} {M N : ℕ → C} [inst : CategoryTheory.Category.{v_1, u_1} C] (f : (n : ℕ) → M n ⟶ N n)
  [inst_1 : CategoryTheory.Limits.HasCountableProducts C] (n : ℕ),
  CategoryTheory.CategoryStruct.comp
      ((CategoryTheory.Functor.ofOpSequence (CategoryTheory.Limits.SequentialProduct.functorMap f)).map
        (CategoryTheory.homOfLE ⋯).op)
      (CategoryTheory.CategoryStruct.comp
        (CategoryTheory.Limits.Pi.π (fun m => if x : m < Opposite.unop (Opposite.op n) then M m else N m) n)
        (CategoryTheory.eqToHom ⋯)) =
    CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.Pi.π (fun i => if x : i < n + 1 then M i else N i) n)
      (CategoryTheory.CategoryStruct.comp (CategoryTheory.eqToHom ⋯) (f n))

Defined in

Mathlib.CategoryTheory.Limits.Shapes.SequentialProduct

Cited by

1 results in Mathlib

Foundations

Depth 61 from the axioms · uses propext, Classical.choice, Quot.sound

Assumes

CategoryTheory.CategoryCategoryTheory.Limits.HasCountableProducts