English
Given any finite collection of objects O and a finite set H of morphisms between objects of O, there exists an object S with arrows T_X: S → X for each X ∈ O, making all the triangles commute along every morphism in H.
Русский
Для данной конечной коллекции объектов O и конечного набора морфизмов между объектами из O существует объект S с стрелками T_X: S → X для каждого X ∈ O, так что треугольники коммутируют для всех морфизмов из H.
LaTeX
$$$\exists S\in \mathrm{Ob}(C), \; \exists T: \forall X\in O,\; S\to X, \; \forall X,Y\in O, \forall f: X\to Y, (X,Y, mX,mY,f) \in H \Rightarrow T_X \circ f = T_Y$$$
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 : S ⟶ X` from each `X`,
such that the triangles commute: `T X ≫ f = T Y`, for `f : X ⟶ Y` in the `Finset`.
-/
theorem inf_exists :
∃ (S : C) (T : ∀ {X : C}, X ∈ O → (S ⟶ X)),
∀ {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 → T mX ≫ f = T mY :=
by
classical
induction H using Finset.induction with
| empty =>
obtain ⟨S, f⟩ := inf_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 ⟨eq (T' mX ≫ f) (T' mY), fun mZ => eqHom (T' mX ≫ f) (T' mY) ≫ T' mZ, ?_⟩
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 eq_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
