cospan — Mathlib

English

Reiterates eq_condition for morphisms f,f' on j ⟶ j': the equation eqHom f f' ≫ f equals eqHom f f' ≫ f'.

Русский

Повтор_eq_condition для морфизмов f,f' : j ⟶ j' : eqHom f f' ≫ f = eqHom f f' ≫ f'.

LaTeX

$$$$ \\mathrm{eqHom}(f,f') \\;\\circ\\; f \;=\\; \\mathrm{eqHom}(f,f') \\;\\circ\\; f'. $$$$

Lean4

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

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