Theorems · Theorem · category theory

CategoryTheory.IsFiltered.coeq_condition_assoc

∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] [inst_1 : CategoryTheory.IsFilteredOrEmpty C] {j j' : C}
  (f f' : j ⟶ j') {Z : C} (h : CategoryTheory.IsFiltered.coeq f f' ⟶ Z),
  CategoryTheory.CategoryStruct.comp f (CategoryTheory.CategoryStruct.comp (CategoryTheory.IsFiltered.coeqHom f f') h) =
    CategoryTheory.CategoryStruct.comp f'
      (CategoryTheory.CategoryStruct.comp (CategoryTheory.IsFiltered.coeqHom f f') h)

coeq_condition f f', for morphisms f f' : j ⟶ j', is the proof that f ≫ coeqHom f f' = f' ≫ coeqHom f f'.

Defined in

Mathlib.CategoryTheory.Filtered.Basic

Cited by

1 results in Mathlib

Foundations

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

Assumes

CategoryTheory.CategoryCategoryTheory.IsFilteredOrEmpty