jointly_surjective — Mathlib

English

In a finite setup, a cocone is jointly surjective onto its colimit.

Русский

В конечной постановке коли-диаграмма сходится к колимиту образуя сюръективность по всем индексам.

LaTeX

$$$\\text{jointly_surjective}(F,t,h,x)$$$

Lean4

theorem jointly_surjective {J : Type*} [Category J] [FinCategory J] (F : J ⥤ FintypeCat.{u}) (t : Cocone F)
    (h : IsColimit t) (x : t.pt) : ∃ j y, t.ι.app j y = x :=
  let hs := isColimitOfPreserves FintypeCat.incl.{u} h
  Types.jointly_surjective (F ⋙ FintypeCat.incl) hs x

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