instBraidedTransportedFunctorEquivalenceTransported

Lean4
instance (e : C ≌ D) [MonoidalCategory C] [BraidedCategory C] : (e' e).functor.Braided where
  braided X
    Y := by
    apply (e' e).inverse.map_injective
    have :
      Functor.LaxMonoidal.μ (((e' e).functor ⋙ (e' e).inverse)) X Y ≫
          ((e' e).functor ⋙ (e' e).inverse).map (β_ X Y).hom ≫
            Functor.OplaxMonoidal.δ ((e' e).functor ⋙ (e' e).inverse) Y X =
        (β_ (((e' e).functor ⋙ (e' e).inverse).obj X) (((e' e).functor ⋙ (e' e).inverse).obj Y)).hom :=
      by
      simp only [((e' e).functor ⋙ (e' e).inverse).map_braiding X Y, Functor.CoreMonoidal.toMonoidal_toOplaxMonoidal,
        assoc, Functor.Monoidal.μ_δ, comp_id, Functor.Monoidal.μ_δ_assoc]
    simp? [-Adjunction.rightAdjointLaxMonoidal_μ]  at this says
      simp only [Functor.comp_obj, Functor.CoreMonoidal.toMonoidal_toLaxMonoidal, Equivalence.symm_inverse,
        Equivalence.symm_functor, Functor.CoreMonoidal.toMonoidal_toOplaxMonoidal, comp_μ, Functor.comp_map,
        Equivalence.inv_fun_map, Functor.id_obj, comp_δ, assoc] at this
    simp [-Adjunction.rightAdjointLaxMonoidal_μ, ← this]
Похожие утверждения