English
Given a tulip configuration (three arrows from j1, j2, j3 to k1, k2) and two arrows to l, there exists s and four maps α,β,γ connecting k1, k2, l to s, giving a system of commuting squares.
Русский
Дано конфигурацию Tulip (три стрелки из j1, j2, j3 в k1, k2) и две стрелки к l; существует s и четыре отображения α,β,γ, соединяющих k1, k2, l с s так, чтобы квадраты сходились.
LaTeX
$$$\\forall {j_1 j_2 j_3 k_1 k_2 l : C} (f_1 : j_1 \\to k_1) (f_2 : j_2 \\to k_1) (f_3 : j_2 \\to k_2) (f_4 : j_3 \\to k_2) (g_1 : j_1 \\to l) (g_2 : j_3 \\to l), \\\\exists s\\, (\\alpha : k_1 \\to s) (\\beta : l \\to s) (\\gamma : k_2 \\to s), \\\\; f_1 \\to \\alpha = g_1 \\to \\beta \land f_2 \\to \\alpha = f_3 \\to \\gamma \land f_4 \\to \\gamma = g_2 \\to \\beta.$$$
Lean4
/-- Given a "tulip" of morphisms
```
j₁ j₂ j₃
|\ / \ / |
| \ / \ / |
| vv vv |
\ k₁ k₂ /
\ /
\ /
\ /
\ /
v v
l
```
in a filtered category, we can construct an object `s` and three morphisms from `k₁`, `k₂` and `l`
to `s`, making the resulting squares commute.
-/
theorem tulip {j₁ j₂ j₃ k₁ k₂ l : C} (f₁ : j₁ ⟶ k₁) (f₂ : j₂ ⟶ k₁) (f₃ : j₂ ⟶ k₂) (f₄ : j₃ ⟶ k₂) (g₁ : j₁ ⟶ l)
(g₂ : j₃ ⟶ l) :
∃ (s : C) (α : k₁ ⟶ s) (β : l ⟶ s) (γ : k₂ ⟶ s), f₁ ≫ α = g₁ ≫ β ∧ f₂ ≫ α = f₃ ≫ γ ∧ f₄ ≫ γ = g₂ ≫ β :=
by
obtain ⟨l', k₁l, k₂l, hl⟩ := span f₂ f₃
obtain ⟨s, ls, l's, hs₁, hs₂⟩ := bowtie g₁ (f₁ ≫ k₁l) g₂ (f₄ ≫ k₂l)
refine ⟨s, k₁l ≫ l's, ls, k₂l ≫ l's, ?_, by simp only [← Category.assoc, hl], ?_⟩ <;>
simp only [hs₁, hs₂, Category.assoc]
