mapAction_μ_hom — Mathlib

English

The multiplication (μ) constraint for the induced lax monoidal action map agrees with the μ-constraint of the original functor.

Русский

Связь умножения μ для индуцированной карты действия согласуется с μ-ограничением исходной функтории.

LaTeX

$$$\mu (F.mapAction G) X Y)^{\mathrm{hom}} = \mu F X.V Y.V$$$

Lean4

@[simp]
theorem mapAction_μ_hom [F.LaxMonoidal] (X Y : Action V G) : (μ (F.mapAction G) X Y).hom = μ F X.V Y.V :=
  rfl

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