inverseImage_equivalence_inverse_eq_map_functor

English

If E is an equivalence C ≌ D, then P.inverseImage E.functor = P.map E.inverse.

Русский

Если E — эквивалентность C ≌ D, то P.inverseImage E.functor = P.map E.inverse.

LaTeX

$$$P^{-1}E.\\mathrm{functor} = P.map E^{-1}$$$

Lean4

theorem inverseImage_equivalence_inverse_eq_map_functor (P : MorphismProperty D) [RespectsIso P] (E : C ≌ D) :
    P.inverseImage E.functor = P.map E.inverse := by
  apply le_antisymm
  · intro X Y f hf
    refine ⟨_, _, _, hf, ⟨?_⟩⟩
    exact ((Functor.mapArrowFunctor _ _).mapIso E.unitIso.symm).app (Arrow.mk f)
  · rw [map_le_iff]
    intro X Y f hf
    exact (P.arrow_mk_iso_iff (((Functor.mapArrowFunctor _ _).mapIso E.counitIso).app (Arrow.mk f))).2 hf

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