comp_reflectsFiniteCoproducts — Mathlib

English

If F and G reflect finite coproducts, then F ∘ G reflects finite coproducts.

Русский

Если F и G отражают конечные копроизведения, тогда F ∘ G отражает конечные копроизведения.

LaTeX

$$$\mathrm{ReflectsFiniteCoproducts}(F) \land \mathrm{ReflectsFiniteCoproducts}(G) \Rightarrow \mathrm{ReflectsFiniteCoproducts}(F \circ G)$$$

Lean4

instance comp_reflectsFiniteCoproducts (F : C ⥤ D) (G : D ⥤ E) [ReflectsFiniteCoproducts F]
    [ReflectsFiniteCoproducts G] : ReflectsFiniteCoproducts (F ⋙ G) where reflects _ := inferInstance

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