Theorems · Theorem · category theory

CategoryTheory.Limits.SequentialProduct.functorMap_commSq

∀ {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 m : ℕ} (h : ¬m < 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) m)
        (CategoryTheory.eqToHom ⋯)) =
    CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.Pi.π (fun i => if x : i < m + 1 then M i else N i) m)
      (CategoryTheory.CategoryStruct.comp (CategoryTheory.eqToHom ⋯) (f m))

Defined in

Mathlib.CategoryTheory.Limits.Shapes.SequentialProduct

Cited by

0 results in Mathlib

Foundations

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

Assumes

CategoryTheory.CategoryCategoryTheory.Limits.HasCountableProducts