isEquivalence_pre — Mathlib

English

Variant asserting faithfulness of pre when F is faithful under the appropriate universal construction.

Русский

Вариант, утверждающий вернообразность pre при Faithful F в соответствующей универсальной постановке.

LaTeX

$$$\text{(pre S F G).Faithful holds when } F\text{ is faithful}$$$

Lean4

/-- If `F` is an equivalence, then so is the functor `(S, F ⋙ G) ⥤ (S, G)`. -/
instance isEquivalence_pre (S : D) (F : B ⥤ C) (G : C ⥤ D) [F.IsEquivalence] : (pre S F G).IsEquivalence :=
  Comma.isEquivalence_preRight _ _ _

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