Theorems · Theorem · category theory

CategoryTheory.IsFiltered.sup_exists

∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] [CategoryTheory.IsFiltered C] (O : Finset C)
  (H : Finset ((X : C) ×' (Y : C) ×' (_ : X ∈ O) ×' (_ : Y ∈ O) ×' (X ⟶ Y))),
  ∃ S T,
    ∀ {X Y : C} (mX : X ∈ O) (mY : Y ∈ O) {f : X ⟶ Y},
      ⟨X, ⟨Y, ⟨mX, ⟨mY, f⟩⟩⟩⟩ ∈ H → CategoryTheory.CategoryStruct.comp f (T mY) = T mX

Given any Finset of objects {X, ...} and indexed collection of Finsets of morphisms {f, ...} in C, there exists an object S, with a morphism T X : X ⟶ S from each X, such that the triangles commute: f ≫ T Y = T X, for f : X ⟶ Y in the Finset.

Defined in

Mathlib.CategoryTheory.Filtered.Basic

Cited by

5 results in Mathlib

Foundations

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

Assumes

CategoryTheory.CategoryCategoryTheory.IsFiltered