whiskeringRight_comp_evaluation — Mathlib

English

Whiskering by F on the right and then evaluating at a is the same as evaluating at a and then applying F: (whiskeringRight A B C).obj F ⋙ (evaluation _ _).obj a = (evaluation _ _).obj a ⋅ F.

Русский

Склейка по правой части через F и затем оценка в a совпадает с оценкой в a и последующим применением F.

LaTeX

$$$(\\mathrm{whiskeringRight}\\ A\\ B\\ C).\\mathrm{obj} F \\; ⋅ (\\mathrm{evaluation}\\ _\\ _).\\mathrm{obj} a = (\\mathrm{evaluation}\\ _\\ _).\\mathrm{obj} a \\; ⋅ F$$$

Lean4

/-- Whiskering by `F` and then evaluating at `a` is the same as evaluating at `F` and then
applying `F`. -/
@[simp]
theorem whiskeringRight_comp_evaluation (F : B ⥤ C) (a : A) :
    (whiskeringRight A B C).obj F ⋙ (evaluation _ _).obj a = (evaluation _ _).obj a ⋙ F :=
  rfl

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