jointly_surjective — Mathlib

English

Let J and K be categories, F : J ⥤ K ⥤ Type be a functor, and t a colimit cocone of F. Then every element of t.pt at every k ∈ K can be represented by a component from the colimit cocone, i.e., the family {ι_j} jointly surjects onto t.pt at each k.

Русский

Пусть J и K — категории, F : J ⥤ K ⥤ Type, и t — сошеление колимита F. Тогда каждый элемент t.pt в точке k ∈ K представим как компоненту кубка колимита, т.е. семейство ι_j совместно покрывает t.pt на каждом k.

LaTeX

$$$\\forall k,\\; \\exists j, \\exists y, x = (t.ι.app j).app k y$$$

Lean4

theorem jointly_surjective (k : K) {t : Cocone F} (h : IsColimit t) (x : t.pt.obj k) [∀ k, HasColimit (F.flip.obj k)] :
    ∃ j y, x = (t.ι.app j).app k y :=
  by
  let hev := isColimitOfPreserves ((evaluation _ _).obj k) h
  obtain ⟨j, y, rfl⟩ := Types.jointly_surjective _ hev x
  exact ⟨j, y, by simp⟩

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