English
There exists an initial object for the parallelPair diagram built from f,g with a zigzag property controlled by left/right maps.
Русский
Существует начальный объект для диаграммы parallelPair из f,g с управляемым свойством Zigzag через отображения слева/справа.
LaTeX
$$parallelPair f g.Initial$$
Lean4
theorem parallelPair_initial_mk' {X Y : C} (f g : X ⟶ Y) (h₁ : ∀ Z, Nonempty (X ⟶ Z))
(h₂ :
∀ ⦃Z : C⦄ (i j : X ⟶ Z),
Zigzag (J := CostructuredArrow (parallelPair f g) Z) (mk (Y := zero) i) (mk (Y := zero) j)) :
(parallelPair f g).Initial where
out
Z := by
have : Nonempty (CostructuredArrow (parallelPair f g) Z) := ⟨mk (Y := zero) (h₁ Z).some⟩
have : ∀ (x : CostructuredArrow (parallelPair f g) Z), Zigzag x (mk (Y := zero) (h₁ Z).some) :=
by
rintro ⟨(_ | _), ⟨⟩, φ⟩
· apply h₂
· refine Zigzag.trans ?_ (h₂ (f ≫ φ) _)
exact Zigzag.of_inv (homMk left)
exact zigzag_isConnected (fun x y => (this x).trans (this y).symm)
