Theorems · Theorem · category theory

CategoryTheory.IsFiltered.bowtie

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

Given a "bowtie" of morphisms `` j₁ j₂ |\ /| | \/ | | /\ | |/ \∣ vv vv 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

5 results in Mathlib

Foundations

Depth 6 from the axioms · uses propext

Assumes

CategoryTheory.CategoryCategoryTheory.IsFilteredOrEmpty