Theorems · Theorem · category theory

CategoryTheory.IsFiltered.coeq_condition

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

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

14 results in Mathlib

Foundations

Depth 12 from the axioms · uses Classical.choice

Assumes

CategoryTheory.CategoryCategoryTheory.IsFilteredOrEmpty