comp_whiskerRight — Mathlib

English

Whiskering on the right distributes over composition of natural transformations.

Русский

Правый whisker-операция распределяется по композиций натуральных трансформаций.

LaTeX

$$$\\mathrm{whiskerRight}(f \\circ g, I) = \\mathrm{whiskerRight}(f,I) \\circ \\mathrm{whiskerRight}(g,I)$$$

Lean4

theorem comp_whiskerRight {F G H : EnrichedFunctor V C D} (α : F ⟶ G) (β : G ⟶ H) (I : EnrichedFunctor V D E) :
    whiskerRight ⟨α.out ≫ β.out⟩ I = whiskerRight α I ≫ whiskerRight β I :=
  by
  ext X
  simp only [whiskerRight_out_app, NatTrans.comp_app, EnrichedFunctor.category_comp_out, EnrichedFunctor.forget,
    EnrichedFunctor.comp_obj, EnrichedFunctor.comp_map]
  simp [← ForgetEnrichment.homOf_comp]

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