widePushout_exists_rep — Mathlib

English

In a concrete category, every element of a wide pushout is either represented by a head over B or by some index i with ι f i mapping from X i.

Русский

В конкретной категории каждый элемент широкого объединения от B либо представляется головой над B, либо элементом ι f i от некоторого X i.

LaTeX

$$$\\exists y:ToType(B), head\\ f\\ y = x \\quad \\lor\\quad \\exists i:\\alpha, \\exists y:ToType(X_i),\\; ι f i\\, y = x$$$

Lean4

theorem widePushout_exists_rep {B : C} {α : Type _} {X : α → C} (f : ∀ j : α, B ⟶ X j) [HasWidePushout.{v} B X f]
    [PreservesColimit (wideSpan B X f) (forget C)] (x : ToType (widePushout B X f)) :
    (∃ y : ToType B, head f y = x) ∨ ∃ (i : α) (y : ToType (X i)), ι f i y = x :=
  by
  obtain ⟨_ | j, y, rfl⟩ := Concrete.colimit_exists_rep _ x
  · left
    use y
    rfl
  · right
    use j, y
    rfl

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