zigzag_prefunctor_obj_of_zigzag — Mathlib

English

If there is a Zigzag between j1 and j2, then there is a Zigzag between F.obj j1 and F.obj j2 for any prefunctor F.

Русский

Если существует Zigzag между j1 и j2, то для любого предфункторa F существует Zigzag между F(j1) и F(j2).

LaTeX

$$$\forall F : J \dashv K,\forall j_1 j_2 : J,\ Zigzag\ j_1 j_2 \Rightarrow Zigzag\ (F.obj\ j_1)\ (F.obj\ j_2)$$$

Lean4

/-- If there is a zigzag from `j₁` to `j₂`, then there is a zigzag from `F j₁` to
`F j₂` as long as `F` is a prefunctor.
-/
theorem zigzag_prefunctor_obj_of_zigzag (F : J ⥤q K) {j₁ j₂ : J} (h : Zigzag j₁ j₂) : Zigzag (F.obj j₁) (F.obj j₂) :=
  h.lift _ fun _ _ => Or.imp (Nonempty.map fun f => F.map f) (Nonempty.map fun f => F.map f)

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