English
In the Center, whiskering with f.f on the right commutes with the β braiding map and tensor; a compatibility equation expressing naturality in both arguments.
Русский
Справа взятие с f.f совместимо с braiding β и тензором; выражает натурализм по обоим аргументам.
LaTeX
$$$f.f \\;▷\\; Y.1 \\; ∘\\; ((\\operatorname{tensorObj} X Y).2.β U).hom = ((\\operatorname{tensorObj} X Y).2.β U).hom \\; ∘\\; U ◁ f.f \\;▷\\; Y.1$$$
Lean4
@[reassoc]
theorem whiskerRight_comm {X₁ X₂ : Center C} (f : X₁ ⟶ X₂) (Y : Center C) (U : C) :
f.f ▷ Y.1 ▷ U ≫ ((tensorObj X₂ Y).2.β U).hom = ((tensorObj X₁ Y).2.β U).hom ≫ U ◁ f.f ▷ Y.1 :=
by
dsimp only [tensorObj_fst, tensorObj_snd_β, Iso.trans_hom, whiskerLeftIso_hom, Iso.symm_hom, whiskerRightIso_hom]
calc
_ =
𝟙 _ ⊗≫
(f.f ▷ (Y.fst ⊗ U) ≫ X₂.fst ◁ (HalfBraiding.β Y.snd U).hom) ⊗≫ (HalfBraiding.β X₂.snd U).hom ▷ Y.fst ⊗≫ 𝟙 _ :=
by monoidal
_ = 𝟙 _ ⊗≫ X₁.fst ◁ (HalfBraiding.β Y.snd U).hom ⊗≫ (f.f ▷ U ≫ (HalfBraiding.β X₂.snd U).hom) ▷ Y.fst ⊗≫ 𝟙 _ := by
rw [← whisker_exchange]; monoidal
_ = _ := by rw [f.comm]; monoidal
