faithful_whiskeringLeft_functor — Mathlib

English

The whiskering-left functor is faithful; equality of whiskered natural transformations implies equality of the original natural transformations.

Русский

Функтор ослабления слева по-прежнему верен (faithful): равенство ослабленных трансформаций означает равенство исходных трансформаций.

LaTeX

$$$\text{Faithful}\; (\mathrm{whiskeringLeft})\; (\mathrm{functor}\ r).\mathrm{obj} \;\Rightarrow\; \text{equality of original transformations}$$$

Lean4

instance faithful_whiskeringLeft_functor : ((whiskeringLeft C _ D).obj (functor r)).Faithful :=
  ⟨by apply natTrans_ext⟩

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