preservesTerminalIso_comp — Mathlib

English

For F:C→D and G:D→E, the terminal object iso for F∘G equals the whisker composition of terminalIsos: preservesTerminalIso (F∘G) = G.mapIso (preservesTerminalIso F) ≪≫ preservesTerminalIso G.

Русский

Для F:C→D и G:D→E изоморфизм терминального объекта для F∘G равен композиции по хвостовым стрелкам: preservesTerminalIso (F∘G) = G.mapIso (preservesTerminalIso F) ≪≫ preservesTerminalIso G.

LaTeX

$$preservesTerminalIso (F ⋙ G) = G.mapIso (preservesTerminalIso F) ≪≫ preservesTerminalIso G$$

Lean4

@[simp]
theorem preservesTerminalIso_comp [PreservesLimit (Functor.empty.{0} C) F] [PreservesLimit (Functor.empty.{0} D) G]
    [PreservesLimit (Functor.empty.{0} C) (F ⋙ G)] :
    preservesTerminalIso (F ⋙ G) = G.mapIso (preservesTerminalIso F) ≪≫ preservesTerminalIso G := by cat_disch

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