toPseudoFunctor — Mathlib

English

For η : f ≅ g, the composition F.map₂ η.hom ≫ F.map₂ η.inv equals the identity on F.map g.

Русский

Для η : f ≅ g, композиция F.map₂ η.hom ≫ F.map₂ η.inv равна единице на F.map g.

LaTeX

$$$F.map₂ η.hom ≫ F.map₂ η.inv = 𝟙 (F.map g)$$$

Lean4

/-- A functor between two categories `C` and `D` can be lifted to a pseudofunctor between the
corresponding locally discrete bicategories.
-/
@[simps! obj map mapId mapComp]
def toPseudoFunctor : Pseudofunctor (LocallyDiscrete C) (LocallyDiscrete D) :=
  pseudofunctorOfIsLocallyDiscrete (fun ⟨X⟩ ↦ .mk <| F.obj X) (fun ⟨f⟩ ↦ (F.map f).toLoc) (fun ⟨X⟩ ↦ eqToIso (by simp))
    (fun f g ↦ eqToIso (by simp))

Похожие утверждения