ι_colimitLimitToLimitColimit_π_apply

English

Another specialization in the same vein; clarifies a variant of the π-compatibility under smallness assumptions.

Русский

Еще одна вариация в той же теме; поясняет вариант совместимости π при малости.

LaTeX

$$$[Small.{v} J][Small.{v} K] ...$$$

Lean4

@[simp]
theorem ι_colimitLimitToLimitColimit_π_apply [Small.{v} J] [Small.{v} K] (F : J × K ⥤ Type v) (j : J) (k : K) (f) :
    limit.π (curry.obj F ⋙ colim) j
        (colimitLimitToLimitColimit F (colimit.ι (curry.obj (Prod.swap K J ⋙ F) ⋙ lim) k f)) =
      colimit.ι ((curry.obj F).obj j) k (limit.π ((curry.obj (Prod.swap K J ⋙ F)).obj k) j f) :=
  by
  dsimp [colimitLimitToLimitColimit]
  rw [Types.Limit.lift_π_apply]
  dsimp only
  rw [Types.Colimit.ι_desc_apply]
  dsimp

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