span — Mathlib

English

For every span i ← f → j, there exists k with maps to i and j making the square commute.

Русский

Для каждого спана i ⟵ f ⟶ j существует объект k и morphisms k → i, k → j так, чтобы квадрат commute.

LaTeX

$$$\\forall {i j : C} (f : i \\to j), \\\\exists k\\, (g : j \\to k) (g' : i \\to k), f \\to g = f' \\to g'.$$$

Lean4

/-- For every span `j ⟵ i ⟶ j'`, there exists a cocone `j ⟶ k ⟵ j'` such that the square
commutes. -/
theorem span {i j j' : C} (f : i ⟶ j) (f' : i ⟶ j') : ∃ (k : C) (g : j ⟶ k) (g' : j' ⟶ k), f ≫ g = f' ≫ g' :=
  let ⟨K, G, G', _⟩ := IsFilteredOrEmpty.cocone_objs j j'
  let ⟨k, e, he⟩ := IsFilteredOrEmpty.cocone_maps (f ≫ G) (f' ≫ G')
  ⟨k, G ≫ e, G' ≫ e, by simpa only [← Category.assoc]⟩

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