Theorems · Theorem · category theory

CategoryTheory.IsFiltered.span

∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] [CategoryTheory.IsFilteredOrEmpty C] {i j j' : C} (f : i ⟶ j)
  (f' : i ⟶ j'), ∃ k g g', CategoryTheory.CategoryStruct.comp f g = CategoryTheory.CategoryStruct.comp f' g'

For every span j ⟵ i ⟶ j', there exists a cocone j ⟶ k ⟵ j' such that the square commutes.

Defined in

Mathlib.CategoryTheory.Filtered.Basic

Cited by

5 results in Mathlib

Foundations

Depth 5 from the axioms · uses no axioms

Assumes

CategoryTheory.CategoryCategoryTheory.IsFilteredOrEmpty