Theorems · Definition · category theory

CategoryTheory.IsCofiltered.eqHom

{C : Type u} →
  [inst : CategoryTheory.Category.{v, u} C] →
    [inst_1 : CategoryTheory.IsCofilteredOrEmpty C] →
      {j j' : C} → (f f' : j ⟶ j') → CategoryTheory.IsCofiltered.eq f f' ⟶ j

eqHom f f', for morphisms f f' : j ⟶ j', is an arbitrary choice of morphism eqHom f f' : eq f f' ⟶ j such that eq_condition : eqHom f f' ≫ f = eqHom f f' ≫ f'. Its existence is ensured by IsCofiltered.

Defined in: Mathlib.CategoryTheory.Filtered.Basic
Cited by: 6 results in Mathlib
Foundations: Depth 11 from the axioms · uses Classical.choice
Assumes: CategoryTheory.Category CategoryTheory.IsCofilteredOrEmpty

Mathlib docs Source Loogle LeanSearch

Around this declaration

Dashed lines are statement dependencies; solid lines are citations in proofs.

Cites4

Mathlib declarations this one mentions in its statement or cites explicitly in its proof. Plumbing is filtered out.

CategoryTheory.Categorystatement and proof · cited by 32,673
Quiver.Homstatement and proof · cited by 32,603
CategoryTheory.IsCofilteredOrEmptystatement and proof · cited by 55
CategoryTheory.IsCofiltered.eqstatement · cited by 8

Cited by6

Results whose statement or proof uses this declaration.

CategoryTheory.IsCofiltered.inf_existsproof · cited by 6
CategoryTheory.IsCofiltered.eq_conditionstatement · cited by 4
CategoryTheory.Comma.isCofiltered_of_isCofiltered_costructuredArrowproof · cited by 3
CategoryTheory.IsCofilteredOrEmpty.of_left_adjointproof · cited by 3
CategoryTheory.Comma.initial_fst_of_isCofiltered_costructuredArrowproof · cited by 1
CategoryTheory.IsCofiltered.eq_condition_assocstatement and proof · cited by 0