Theorems · Definition · category theory
CategoryTheory.Limits.CompleteLattice.finiteColimitCocone
{α : Type u} →
{J : Type w} →
[inst : CategoryTheory.SmallCategory J] →
[CategoryTheory.FinCategory J] →
[inst_2 : SemilatticeSup α] →
[OrderBot α] → (F : CategoryTheory.Functor J α) → CategoryTheory.Limits.ColimitCocone FThe colimit cocone over any functor from a finite diagram into a SemilatticeSup with OrderBot.
- Defined in
- Mathlib.CategoryTheory.Limits.Lattice
- Cited by
- 5 results in Mathlib
- Foundations
- Depth 58 from the axioms · uses propext, Classical.choice, Quot.sound
Around this declaration
Dashed lines are statement dependencies; solid lines are citations in proofs.
Cites11
Mathlib declarations this one mentions in its statement or cites explicitly in its proof. Plumbing is filtered out.
- CategoryTheory.Functor.objproof · cited by 19,642
- CategoryTheory.Functorstatement and proof · cited by 16,252
- Finset.univproof · cited by 3,473
- OrderBotstatement and proof · cited by 1,055
- SemilatticeSupstatement and proof · cited by 785
- CategoryTheory.Limits.Coconeproof · cited by 746
- CategoryTheory.homOfLEproof · cited by 554
- Finset.supproof · cited by 530
- CategoryTheory.SmallCategorystatement and proof · cited by 480
- CategoryTheory.FinCategorystatement and proof · cited by 107
- CategoryTheory.Limits.ColimitCoconestatement · cited by 20
Cited by5
Results whose statement or proof uses this declaration.
- CategoryTheory.Limits.CompleteLattice.finite_colimit_eq_finset_univ_supproof · cited by 2
- CategoryTheory.Limits.CompleteLattice.finiteColimitCocone_cocone_ptstatement and proof · cited by 0
- CategoryTheory.Limits.CompleteLattice.finiteColimitCocone_cocone_ι_appstatement and proof · cited by 0
- CategoryTheory.Limits.CompleteLattice.finiteColimitCocone_isColimit_descstatement and proof · cited by 0
- CategoryTheory.Limits.CompleteLattice.finite_coproduct_eq_finset_supproof · cited by 0