English
Given a finite set of objects and a finite family of morphisms among them, there exists a universal right object S and maps from each X to S making all specified equalities hold.
Русский
Дано конечное множество объектов и семейство морфизмов между ними, существует общий правый объект S и стрелки X ⟶ S, делающие все указанные равенства выполняемыми.
LaTeX
$$$\exists S, \exists T, \text{triangles commute as specified}$$$
Lean4
/-- Given any `Finset` of objects `{X, ...}` and
indexed collection of `Finset`s of morphisms `{f, ...}` in `C`,
there exists an object `S`, with a morphism `T X : X ⟶ S` from each `X`,
such that the triangles commute: `f ≫ T Y = T X`, for `f : X ⟶ Y` in the `Finset`.
-/
theorem sup_exists :
∃ (S : C) (T : ∀ {X : C}, X ∈ O → (X ⟶ S)),
∀ {X Y : C} (mX : X ∈ O) (mY : Y ∈ O) {f : X ⟶ Y},
(⟨X, Y, mX, mY, f⟩ : Σ' (X Y : C) (_ : X ∈ O) (_ : Y ∈ O), X ⟶ Y) ∈ H → f ≫ T mY = T mX :=
by
classical
induction H using Finset.induction with
| empty =>
obtain ⟨S, f⟩ := sup_objs_exists O
exact ⟨S, fun mX => (f mX).some, by rintro - - - - - ⟨⟩⟩
| insert h' H' nmf h'' =>
obtain ⟨X, Y, mX, mY, f⟩ := h'
obtain ⟨S', T', w'⟩ := h''
refine ⟨coeq (f ≫ T' mY) (T' mX), fun mZ => T' mZ ≫ coeqHom (f ≫ T' mY) (T' mX), ?_⟩
intro X' Y' mX' mY' f' mf'
rw [← Category.assoc]
by_cases h : X = X' ∧ Y = Y'
· rcases h with ⟨rfl, rfl⟩
by_cases hf : f = f'
· subst hf
apply coeq_condition
· rw [@w' _ _ mX mY f']
simp only [Finset.mem_insert, PSigma.mk.injEq, heq_eq_eq, true_and] at mf'
grind
· rw [@w' _ _ mX' mY' f' _]
apply Finset.mem_of_mem_insert_of_ne mf'
contrapose! h
obtain ⟨rfl, h⟩ := h
trivial
