fromSum — Mathlib

English

The canonical functor fromSum C D : C ⊕ D ⥤ C ⋆ D is essentially surjective; every object of the join is in the image of fromSum.

Русский

Канонический функтор fromSum C D: C ⊕ D ⥤ C ⋆ D сюръективен на эквивалентном уровне; каждый объект соединения принадлежит образу fromSum.

LaTeX

$$$\operatorname{EssSurj}(\mathrm{fromSum} \; C \; D)$$$

Lean4

/-- The canonical functor from the sum to the join.
It sends `inl c` to `left c` and `inr d` to `right d`. -/
@[simps! obj] -- Maps get characterized w.r.t. the inclusions below

def fromSum : C ⊕ D ⥤ C ⋆ D :=
  (inclLeft C D).sum' <| inclRight C D

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