Theorems · Definition · category theory
CategoryTheory.IsFiltered.rightToMax
{C : Type u} →
[inst : CategoryTheory.Category.{v, u} C] →
[inst_1 : CategoryTheory.IsFilteredOrEmpty C] → (j j' : C) → j' ⟶ CategoryTheory.IsFiltered.max j j'rightToMax j j' is an arbitrary choice of morphism from j' to max j j',
whose existence is ensured by IsFiltered.
- Defined in
- Mathlib.CategoryTheory.Filtered.Basic
- Cited by
- 26 results in Mathlib
- Foundations
- Depth 11 from the axioms · uses Classical.choice
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 · cited by 32,603
- CategoryTheory.IsFilteredOrEmptystatement and proof · cited by 55
- CategoryTheory.IsFiltered.maxstatement · cited by 26
Cited by34
Results whose statement or proof uses this declaration.
- CategoryTheory.Functor.IsEventuallyConstantFrom.coconeιAppproof · cited by 4
- AddMonCat.FilteredColimits.colimit_add_mk_eqproof · cited by 3
- CategoryTheory.IsFilteredOrEmpty.of_right_adjointproof · cited by 3
- CategoryTheory.isFiltered_structuredArrow_of_isFiltered_of_existsproof · cited by 3
- CategoryTheory.IsFiltered.coeq₃proof · cited by 3
- CategoryTheory.IsFiltered.coeq₃Homproof · cited by 3
- AddMonCat.FilteredColimits.colimit_zero_eqproof · cited by 2
- CategoryTheory.IsFiltered.crownproof · cited by 2
- MonCat.FilteredColimits.colimitMulAuxproof · cited by 2
- MonCat.FilteredColimits.colimit_mul_mk_eqproof · cited by 2