map_inverseImage_eq_of_isEquivalence

English

If P is a morphism property on D and E is an equivalence C ≌ D, then (P.inverseImage F).map F = P for F = E.functor.

Русский

Если P — свойство морфизмов на D и E — эквивалентность C ≌ D, то (P.inverseImage F).map F = P для F = E.functor.

LaTeX

$$$(P.map F)^{-1}F = P$ (understanding via equivalence)$$

Lean4

theorem map_inverseImage_eq_of_isEquivalence (P : MorphismProperty D) [P.RespectsIso] (F : C ⥤ D) [F.IsEquivalence] :
    (P.inverseImage F).map F = P := by
  erw [P.inverseImage_equivalence_inverse_eq_map_functor F.asEquivalence, map_map,
    P.map_eq_of_iso F.asEquivalence.counitIso, map_id]

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