Lean4
/-- Auxiliary definition for the `MonoidalCategory` instance on `Center C`. -/
@[simps]
def tensorObj (X Y : Center C) : Center C :=
⟨X.1 ⊗ Y.1,
{ β := fun U =>
α_ _ _ _ ≪≫ (whiskerLeftIso X.1 (Y.2.β U)) ≪≫ (α_ _ _ _).symm ≪≫ (whiskerRightIso (X.2.β U) Y.1) ≪≫ α_ _ _ _
monoidal := fun U U' =>
by
dsimp only [Iso.trans_hom, whiskerLeftIso_hom, Iso.symm_hom, whiskerRightIso_hom]
simp only [HalfBraiding.monoidal]
-- We'd like to commute `X.1 ◁ U ◁ (HalfBraiding.β Y.2 U').hom`
-- and `((HalfBraiding.β X.2 U).hom ▷ U' ▷ Y.1)` past each other.
-- We do this with the help of the monoidal composition `⊗≫` and the `coherence` tactic.
calc
_ =
𝟙 _ ⊗≫
X.1 ◁ (HalfBraiding.β Y.2 U).hom ▷ U' ⊗≫
(_ ◁ (HalfBraiding.β Y.2 U').hom ≫ (HalfBraiding.β X.2 U).hom ▷ _) ⊗≫
U ◁ (HalfBraiding.β X.2 U').hom ▷ Y.1 ⊗≫ 𝟙 _ :=
by monoidal
_ = _ := by rw [whisker_exchange]; monoidal
naturality := fun {U U'} f =>
by
dsimp only [Iso.trans_hom, whiskerLeftIso_hom, Iso.symm_hom, whiskerRightIso_hom]
calc
_ = 𝟙 _ ⊗≫ (X.1 ◁ (Y.1 ◁ f ≫ (HalfBraiding.β Y.2 U').hom)) ⊗≫ (HalfBraiding.β X.2 U').hom ▷ Y.1 ⊗≫ 𝟙 _ := by
monoidal
_ = 𝟙 _ ⊗≫ X.1 ◁ (HalfBraiding.β Y.2 U).hom ⊗≫ (X.1 ◁ f ≫ (HalfBraiding.β X.2 U').hom) ▷ Y.1 ⊗≫ 𝟙 _ := by
rw [HalfBraiding.naturality]; monoidal
_ = _ := by rw [HalfBraiding.naturality]; monoidal }⟩
