inverse — Mathlib

Lean4
/-- The functor going from the opposite of the underlying category of the enriched category `C`
to the underlying category of the enriched category `Cᵒᵖ`. -/
def inverse : (ForgetEnrichment V C)ᵒᵖ ⥤ ForgetEnrichment V Cᵒᵖ
    where
  obj x := x
  map {x y} f := f.unop
  map_comp {x y z} f
    g := by
    have : g.unop ≫ f.unop = homTo V (g.unop ≫ f.unop) := rfl
    dsimp
    rw [this, ForgetEnrichment.homTo_comp, Category.assoc, unitors_inv_equal, ← leftUnitor_inv_braiding_assoc]
    have :
      (β_ _ _).hom ≫ (homTo V g.unop ⊗ₘ homTo V f.unop) ≫ eComp V («to» V z.unop) («to» V y.unop) («to» V x.unop) =
        ((homTo V f.unop) ⊗ₘ (homTo V g.unop)) ≫ eComp V x y z :=
      (tensorHom_eComp_op_eq V _ _).symm
    rw [this, ← Category.assoc]
    congr 1
Похожие утверждения