of_comp_faithful_iso — Mathlib

English

If F ⋙ G is full and G is faithful, then F is full (via iso-arguments).

Русский

Если F ⋙ G полно и G верен, то F полно (через изоморфности).

LaTeX

$$$[ Full (F \circ G) ] \land [ G.Faithful] \Rightarrow Full F$$$

Lean4

/-- If `F ⋙ G` is full and `G` is faithful, then `F` is full. -/
theorem of_comp_faithful_iso {F : C ⥤ D} {G : D ⥤ E} {H : C ⥤ E} [Full H] [G.Faithful] (h : F ⋙ G ≅ H) : Full F :=
  by
  have := Full.of_iso h.symm
  exact Full.of_comp_faithful F G

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