inverseFunctorMapIso_symm_eq_isoInverseOfIsoFunctor

English

Relates the inverse construction on a map of equivalences to the standard isoInverseOfIsoFunctor construction.

Русский

Связано с тем, как обратная конструкция действует на отображение эквивалентностей и соотносится с конструкцией isoInverseOfIsoFunctor.

LaTeX

$$Iso.unop((inverseFunctor C D).mapIso α.symm) = Iso.isoInverseOfIsoFunctor((functorFunctor _ _).mapIso α)$$

Lean4

/-- We can compare the way we obtain a natural isomorphism `e.inverse ≅ f.inverse` from
an isomorphism `e ≌ f` via `inverseFunctor` with the way we get one through
`Iso.isoInverseOfIsoFunctor`. -/
theorem inverseFunctorMapIso_symm_eq_isoInverseOfIsoFunctor {e f : C ≌ D} (α : e ≅ f) :
    Iso.unop ((inverseFunctor C D).mapIso α.symm) = Iso.isoInverseOfIsoFunctor ((functorFunctor _ _).mapIso α) := by
  cat_disch

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