changeFunctor — Mathlib

English

Changing functors along identity isomorphisms leaves the equivalence unchanged.

Русский

Изменение функторов вдоль тождественных изоморфизмов не изменяет эквивалентность.

LaTeX

$$$e.changeFunctor(I \!\mathrm{d}_\mathrm{refl}) = e$$$

Lean4

/-- If `e : C ≌ D` is an equivalence of categories, and `iso : e.functor ≅ G` is
an isomorphism, then there is an equivalence of categories whose functor is `G`. -/
@[simps!]
def changeFunctor (e : C ≌ D) {G : C ⥤ D} (iso : e.functor ≅ G) : C ≌ D
    where
  functor := G
  inverse := e.inverse
  unitIso := e.unitIso ≪≫ isoWhiskerRight iso _
  counitIso := isoWhiskerLeft _ iso.symm ≪≫ e.counitIso

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