English
In the center, whiskering left with f.f distributes with β and composition; a coherence relation that aligns left whiskering with the tensor interactions.
Русский
В центре левое взятие с f.f распределяется через β и композицию; когерентное соотношение, согласующее левое взятие с тензорной структурой.
LaTeX
$$$(X.1) \\;◁\\; f.f \\;▷\\; U \\; ≈\\; ((X.tensorObj Y).snd.β U).hom \\;∘\\; U ◁ X.1 ◁ f.f$$$
Lean4
@[reassoc]
theorem whiskerLeft_comm (X : Center C) {Y₁ Y₂ : Center C} (f : Y₁ ⟶ Y₂) (U : C) :
(X.1 ◁ f.f) ▷ U ≫ ((tensorObj X Y₂).2.β U).hom = ((tensorObj X Y₁).2.β U).hom ≫ U ◁ X.1 ◁ f.f :=
by
dsimp only [tensorObj_fst, tensorObj_snd_β, Iso.trans_hom, whiskerLeftIso_hom, Iso.symm_hom, whiskerRightIso_hom]
calc
_ = 𝟙 _ ⊗≫ X.fst ◁ (f.f ▷ U ≫ (HalfBraiding.β Y₂.snd U).hom) ⊗≫ (HalfBraiding.β X.snd U).hom ▷ Y₂.fst ⊗≫ 𝟙 _ := by
monoidal
_ =
𝟙 _ ⊗≫
X.fst ◁ (HalfBraiding.β Y₁.snd U).hom ⊗≫ ((X.fst ⊗ U) ◁ f.f ≫ (HalfBraiding.β X.snd U).hom ▷ Y₂.fst) ⊗≫ 𝟙 _ :=
by rw [f.comm]; monoidal
_ = _ := by rw [whisker_exchange]; monoidal
