isEquivalence_of_comp_right — Mathlib

English

If G is an equivalence and F ⋙ G is an equivalence, then F is an equivalence.

Русский

Если G — эквивалентность, а F ⋙ G — эквивалентность, то F — эквивалентность.

LaTeX

$$G.IsEquivalence ∧ (F ⋙ G).IsEquivalence ⇒ F.IsEquivalence$$

Lean4

/-- If `G` and `F ⋙ G` are equivalence of categories, then `F` is also an equivalence. -/
theorem isEquivalence_of_comp_right {E : Type*} [Category E] (F : C ⥤ D) (G : D ⥤ E) [IsEquivalence G]
    [IsEquivalence (F ⋙ G)] : IsEquivalence F :=
  by
  rw [isEquivalence_iff_of_iso (F.rightUnitor.symm ≪≫ isoWhiskerLeft F (G.asEquivalence.unitIso))]
  exact ((F ⋙ G).asEquivalence.trans G.asEquivalence.symm).isEquivalence_functor

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