inverseImage_equivalence_functor_eq_map_inverse

English

If Q is a morphism property on C and E is an equivalence C ≌ D, then Q.inverseImage E.inverse = Q.map E.functor.

Русский

Если Q — свойство морфизмов на C и E — эквивалентность C ≌ D, то Q inverseImage E.inverse = Q.map E.functor.

LaTeX

$$$Q.inverseImage E.inverse = Q.map E.functor$$$

Lean4

theorem inverseImage_equivalence_functor_eq_map_inverse (Q : MorphismProperty C) [RespectsIso Q] (E : C ≌ D) :
    Q.inverseImage E.inverse = Q.map E.functor :=
  inverseImage_equivalence_inverse_eq_map_functor Q E.symm

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