jointly_surjective' — Mathlib

English

In the setting of FunctorToTypes, the jointly surjective property for colimits can be extended to the flipped functor, ensuring that every element in the colimit corresponds to a pair (j,y) in the flipped diagram.

Русский

Для случая FunctorToTypes, свойство совместной полноты колимита сохраняется для перевернутого функторa, обеспечивая, что любой элемент в колимите соответствует паре (j,y) в перевернутой диаграмме.

LaTeX

$$$\\exists j,\\exists y, x = (\\text{colimit.ι } F j).app k y$$$

Lean4

theorem jointly_surjective' [∀ k, HasColimit (F.flip.obj k)] (k : K) (x : (colimit F).obj k) :
    ∃ j y, x = (colimit.ι F j).app k y :=
  jointly_surjective _ _ (colimit.isColimit _) x

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