initial_comp_equivalence — Mathlib

English

If F and G are equivalences, then F ⋙ G is final.

Русский

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

LaTeX

$$$[\\text{IsEquivalence}(F)] \\wedge [\\text{IsEquivalence}(G)] \\Rightarrow [\\text{Final}(F \\circ G)].$$$

Lean4

/-- See also the strictly more general `initial_comp` below. -/
theorem initial_comp_equivalence [Initial F] [IsEquivalence G] : Initial (F ⋙ G) :=
  let i : F ≅ (F ⋙ G) ⋙ G.inv := isoWhiskerLeft F G.asEquivalence.unitIso
  have : Initial ((F ⋙ G) ⋙ G.inv) := initial_of_natIso i
  initial_of_comp_full_faithful (F ⋙ G) G.inv

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