instEssSurjSumFromSum — Mathlib

English

The fromSum functor is essentially surjective onto Join, i.e., every object of Join is isomorphic to the image of fromSum of some object of C ⊕ D.

Русский

Функтор fromSum сюръективен по существу на Join: каждый объект Join изоморфен образу fromSum некоторого объекта из C ⊕ D.

LaTeX

$$$\text{EssSurj}(\mathrm{fromSum} C D)$$$

Lean4

instance : (fromSum C D).EssSurj where
  mem_essImage
    | left c => Functor.obj_mem_essImage _ (Sum.inl c)
    | right d => Functor.obj_mem_essImage _ (Sum.inr d)

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