parallelPair_initial_mk — Mathlib

English

Given f,g with a universal property (every Z has a morphism from X, etc.), one constructs an initial object using zigzags via homMk.

Русский

Данные f,g с универсальным свойством строят начальный объект через зигзакг через homMk.

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), ∃ (a : Y ⟶ Z), i = f ≫ a ∧ j = g ≫ a) : (parallelPair f g).Initial :=
  parallelPair_initial_mk' f g h₁
    (fun Z i j => by
      obtain ⟨a, rfl, rfl⟩ := h₂ i j
      let f₁ : (mk (Y := zero) (f ≫ a) : CostructuredArrow (parallelPair f g) Z) ⟶ mk (Y := one) a := homMk left
      let f₂ : (mk (Y := zero) (g ≫ a) : CostructuredArrow (parallelPair f g) Z) ⟶ mk (Y := one) a := homMk right
      exact Zigzag.of_hom_inv f₁ f₂)

Похожие утверждения