map_rightUnitor — Mathlib

English

For a fixed functor F, the map from Monoidal structures to LaxMonoidal structures on F is injective.

Русский

Для фиксированного функторы F отображение из монодийных структур в ленсовые структуры на F инъективно.

LaTeX

$$$$ \\operatorname{Injective}\\Big( \\operatorname{toLaxMonoidal}_{F} \\Big) $$$$

Lean4

@[reassoc]
theorem map_rightUnitor (X : C) : F.map (ρ_ X).hom = δ F X (𝟙_ C) ≫ F.obj X ◁ η F ≫ (ρ_ (F.obj X)).hom := by simp

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