ι_colimitLimitToLimitColimit_π — Mathlib

English

A compatibility equality for the π components connecting colimit and limit via curry and swap constructions.

Русский

Совместная равенство компонент π между колимитом и пределом через карри и перестановку.

LaTeX

$$Eq( limits... ) (колимит-лимит-π совместимость)$$

Lean4

/-- Since `colimit_limit_to_limit_colimit` is a morphism from a colimit to a limit,
this lemma characterises it.
-/
@[reassoc (attr := simp)]
theorem ι_colimitLimitToLimitColimit_π (j) (k) :
    colimit.ι _ k ≫ colimitLimitToLimitColimit F ≫ limit.π _ j =
      limit.π ((curry.obj (Prod.swap K J ⋙ F)).obj k) j ≫ colimit.ι ((curry.obj F).obj j) k :=
  by
  dsimp [colimitLimitToLimitColimit]
  simp

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