toPseudoFunctor' — Mathlib

English

If η is an isomorphism, then F.map₂ η.inv is an isomorphism with inverse F.map₂ η.hom.

Русский

Если η — изоморфизм, то F.map₂ η.inv является изоморфизмом с обратным F.map₂ η.hom.

LaTeX

$$IsIso (F.map₂ η.inv)$$

Lean4

/-- If `B` is a strict bicategory and `I` is a (1-)category, any functor (of 1-categories) `I ⥤ B` can
be promoted to a pseudofunctor from `LocallyDiscrete I` to `B`.
-/
@[simps! obj map mapId mapComp]
def toPseudoFunctor' : Pseudofunctor (LocallyDiscrete I) B :=
  pseudofunctorOfIsLocallyDiscrete (fun ⟨X⟩ ↦ F.obj X) (fun ⟨f⟩ ↦ F.map f) (fun ⟨X⟩ ↦ eqToIso (by simp))
    (fun f g ↦ eqToIso (by simp))

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