Lean4
/-- If `m ⊗ n ≅ 𝟙_M` and `n ⊗ m ≅ 𝟙_M` (subject to some commuting constraints),
then `F.obj m` and `F.obj n` forms a self-equivalence of `C`. -/
@[simps]
noncomputable def equivOfTensorIsoUnit (m n : M) (h₁ : m ⊗ n ≅ 𝟙_ M) (h₂ : n ⊗ m ≅ 𝟙_ M)
(H : h₁.hom ▷ m ≫ (λ_ m).hom = (α_ m n m).hom ≫ m ◁ h₂.hom ≫ (ρ_ m).hom) [F.Monoidal] : C ≌ C
where
functor := F.obj m
inverse := F.obj n
unitIso := (unitOfTensorIsoUnit F m n h₁).symm
counitIso := unitOfTensorIsoUnit F n m h₂
functor_unitIso_comp
X := by
dsimp
simp only [μ_naturalityᵣ_assoc, μ_naturalityₗ_assoc, η_app_obj, Category.assoc, obj_μ_inv_app, Functor.map_comp,
δ_μ_app_assoc, obj_ε_app, unitOfTensorIsoUnit_inv_app]
simp only [← NatTrans.comp_app, ← F.map_comp, ← H, inv_hom_whiskerRight_assoc, Iso.inv_hom_id, Functor.map_id,
NatTrans.id_app]
