initial_of_comp_full_faithful — Mathlib

English

If G is full and faithful and F ⋙ G is initial, then F is initial.

Русский

Если G полон и верен и F ⋙ G начальный, тогда F начальный.

LaTeX

$$$[\\text{Full}(G)] \\wedge [\\text{Faithful}(G)] \\wedge [\\text{Initial}(F \\circ G)] \\Rightarrow [\\text{Initial}(F)].$$$

Lean4

/-- The hypotheses also imply that `G` is initial, see `initial_of_comp_full_faithful'`. -/
theorem initial_of_comp_full_faithful [Full G] [Faithful G] [Initial (F ⋙ G)] : Initial F where
  out d := isConnected_of_equivalent (CostructuredArrow.post F G d).asEquivalence.symm

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