Theorems · Theorem · category theory

CategoryTheory.IsFiltered.tulip

∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] [CategoryTheory.IsFilteredOrEmpty C] {j₁ j₂ j₃ k₁ k₂ l : C}
  (f₁ : j₁ ⟶ k₁) (f₂ : j₂ ⟶ k₁) (f₃ : j₂ ⟶ k₂) (f₄ : j₃ ⟶ k₂) (g₁ : j₁ ⟶ l) (g₂ : j₃ ⟶ l),
  ∃ s α β γ,
    CategoryTheory.CategoryStruct.comp f₁ α = CategoryTheory.CategoryStruct.comp g₁ β ∧
      CategoryTheory.CategoryStruct.comp f₂ α = CategoryTheory.CategoryStruct.comp f₃ γ ∧
        CategoryTheory.CategoryStruct.comp f₄ γ = CategoryTheory.CategoryStruct.comp g₂ β

Given a "tulip" of morphisms `` j₁ j₂ j₃ |\ / \ / | | \ / \ / | | vv vv | \ k₁ k₂ / \ / \ / \ / \ / v v l ` in a filtered category, we can construct an object s and three morphisms from k₁, k₂ and l to s`, making the resulting squares commute.

Defined in

Mathlib.CategoryTheory.Filtered.Basic

Cited by

4 results in Mathlib

Foundations

Depth 7 from the axioms · uses propext

Assumes

CategoryTheory.CategoryCategoryTheory.IsFilteredOrEmpty