isZero_single_comp_eval — Mathlib

English

For any j,i with i ≠ j, the composite functor single V c j followed by eval V c i is zero.

Русский

Для любых j и i с i ≠ j композиция single V c j ⋙ eval V c i равна нулю.

LaTeX

$$$$ \operatorname{IsZero}\big((\text{single } V\ c\ j) \circ \operatorname{eval } V\ c\ i\big) $$$$

Lean4

theorem isZero_single_comp_eval (j i : ι) (hi : i ≠ j) : IsZero (single V c j ⋙ eval V c i) :=
  Functor.isZero _ (fun _ ↦ isZero_single_obj_X c _ _ _ hi)

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