inverseImage_map_eq_of_isEquivalence

English

If F is an equivalence, then (P.inverseImage F).map F = P.

Русский

Если F — эквивалентность, то (P.inverseImage F).map F = P.

LaTeX

$$$(P.inverseImage F).map F = P$$$

Lean4

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

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