map_eq_of_iso — Mathlib

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 map_eq_of_iso (P : MorphismProperty C) {F G : C ⥤ D} (e : F ≅ G) : P.map F = P.map G :=
  by
  revert F G e
  suffices ∀ {F G : C ⥤ D} (_ : F ≅ G), P.map F ≤ P.map G from fun F G e => le_antisymm (this e) (this e.symm)
  intro F G e X Y f ⟨X', Y', f', hf', ⟨e'⟩⟩
  exact ⟨X', Y', f', hf', ⟨((Functor.mapArrowFunctor _ _).mapIso e.symm).app (Arrow.mk f') ≪≫ e'⟩⟩

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