eComp_eHomWhiskerLeft — Mathlib

English

The enriched composition commutes with right whiskering: composing first then whiskering equals whiskering then composition.

Русский

Обогащённая композиция коммутирует с правым whiskerRight: композицию сначала затем whiskerRight равносильно whiskerRight затем композиция.

LaTeX

$$$eComp\,V\,X'\,Y\,Z \;\;\; ≔ \; eHomWhiskerRight\,V\,fZ \circ eHomWhiskerRight\,V\,fY \Rightarrow$$$

Lean4

/-- Whiskering commutes with the enriched composition. -/
@[reassoc]
theorem eComp_eHomWhiskerLeft (X Y : C) {Z Z' : C} (g : Z ⟶ Z') :
    eComp V X Y Z ≫ eHomWhiskerLeft V X g = _ ◁ eHomWhiskerLeft V Y g ≫ eComp V X Y Z' :=
  by
  dsimp [eHomWhiskerLeft]
  rw [rightUnitor_inv_naturality_assoc, ← whisker_exchange_assoc]
  simp

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