English
Given a bowtie of morphisms f1, g1, f2, g2 in a filtered category, there exists an object s and morphisms to s from k1 and k2 making two squares commute.
Русский
Дано «галочку» из морфизмов f1, g1, f2, g2 в фильтрованной категории, существует объект s и такие морфизмы k1 ⟶ s, k2 ⟶ s, чтобы два квадрата commute.
LaTeX
$$$\\forall {j_1 j_2 k_1 k_2 : C}\\ (f_1 : j_1 \\to k_1) (g_1 : j_1 \\to k_2) (f_2 : j_2 \\to k_1) (g_2 : j_2 \\to k_2), \\\\exists s\\, (\\alpha : k_1 \\to s) (\\beta : k_2 \\to s), f_1 \\circ \\alpha = g_1 \\circ \\beta \\land f_2 \\circ \\alpha = g_2 \\circ \\beta.$$$
Lean4
/-- Given a "bowtie" of morphisms
```
j₁ j₂
|\ /|
| \/ |
| /\ |
|/ \∣
vv vv
k₁ k₂
```
in a filtered category, we can construct an object `s` and two morphisms from `k₁` and `k₂` to `s`,
making the resulting squares commute.
-/
theorem bowtie {j₁ j₂ k₁ k₂ : C} (f₁ : j₁ ⟶ k₁) (g₁ : j₁ ⟶ k₂) (f₂ : j₂ ⟶ k₁) (g₂ : j₂ ⟶ k₂) :
∃ (s : C) (α : k₁ ⟶ s) (β : k₂ ⟶ s), f₁ ≫ α = g₁ ≫ β ∧ f₂ ≫ α = g₂ ≫ β :=
by
obtain ⟨t, k₁t, k₂t, ht⟩ := span f₁ g₁
obtain ⟨s, ts, hs⟩ := IsFilteredOrEmpty.cocone_maps (f₂ ≫ k₁t) (g₂ ≫ k₂t)
simp_rw [Category.assoc] at hs
exact ⟨s, k₁t ≫ ts, k₂t ≫ ts, by simp only [← Category.assoc, ht], hs⟩
