changeInverse — Mathlib

English

The underlying functor of an equivalence C ≌ D is itself an equivalence of categories.

Русский

Основной функтор эквивалентности C ≌ D сам по себе является эквивалентностью категорий.

LaTeX

$$$\text{IsEquivalence}(e.functor)$$$

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 inverse is `G`. -/
@[simps!]
def changeInverse (e : C ≌ D) {G : D ⥤ C} (iso : e.inverse ≅ G) : C ≌ D
    where
  functor := e.functor
  inverse := G
  unitIso := e.unitIso ≪≫ isoWhiskerLeft _ iso
  counitIso := isoWhiskerRight iso.symm _ ≪≫ e.counitIso
  functor_unitIso_comp
    X := by
    dsimp
    rw [← map_comp_assoc, assoc, iso.hom_inv_id_app, comp_id, functor_unit_comp]

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