Theorems · Theorem · category theory

CategoryTheory.IsFiltered.crown

∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] [CategoryTheory.IsFilteredOrEmpty C] {ι : Type u_1} [Finite ι]
  (j : ι → C) {k₁ k₂ : C} (f : (i : ι) → j i ⟶ k₁) (g : (i : ι) → j i ⟶ k₂),
  ∃ s α β, ∀ (i : ι), CategoryTheory.CategoryStruct.comp (f i) α = CategoryTheory.CategoryStruct.comp (g i) β

Given a "crown" of morphisms `` j₁ j₂ j₃ ... jₙ / \ /\ / \ | \/ \/ | | /\ /\ | | | \/ | | \ | /\ | / \ | / \ | / vvv vvv k₁ k₂ ` in a filtered category, we can construct an object s and two morphisms from k₁ and k₂ to s`, making the resulting squares commute.

Defined in

Mathlib.CategoryTheory.Filtered.Basic

Cited by

2 results in Mathlib

Foundations

Depth 71 from the axioms · uses propext, Classical.choice, Quot.sound

Assumes

CategoryTheory.CategoryCategoryTheory.IsFilteredOrEmptyFinite