μ_natural_left — Mathlib

English

The left unit constraint μ is natural in its left argument: the naturality square commutes with left whiskering by a morphism f on X.

Русский

Левый критерий единицы μ естествен по левому аргументу: натурализованность квадрата совместима с левым оборачивающим отображением от f.

LaTeX

$$$\\text{μ\tnatural\_left }(f,X,Y): (L').map f ▷ (L').obj Y ≫ μ(X_2,Y).hom = μ(X_1,Y).hom ≫ (L').map (f ▷ Y)$$$

Lean4

@[reassoc (attr := simp)]
theorem μ_natural_left {X₁ X₂ : C} (f : X₁ ⟶ X₂) (Y : C) :
    (L').map f ▷ (L').obj Y ≫ (μ L W ε X₂ Y).hom = (μ L W ε X₁ Y).hom ≫ (L').map (f ▷ Y) :=
  NatTrans.naturality_app (tensorBifunctorIso L W ε).hom Y f

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