isEquivalence_of_comp_left — Mathlib

English

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

Русский

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

LaTeX

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

Lean4

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

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