Theorems · Definition · category theory

MonCat.FilteredColimits.M.mk

{J : Type v} →
  [inst : CategoryTheory.SmallCategory J] →
    (F : CategoryTheory.Functor J MonCat) → (j : J) × ↑(F.obj j) → MonCat.FilteredColimits.M F

The canonical projection into the colimit, as a quotient type.

Defined in: Mathlib.Algebra.Category.MonCat.FilteredColimits
Cited by: 6 results in Mathlib
Foundations: Depth 21 from the axioms · uses propext, Classical.choice, Quot.sound
Assumes: CategoryTheory.SmallCategory

Mathlib docs Source Loogle LeanSearch

Around this declaration

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

Cites9

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

CategoryTheory.Functor.objstatement and proof · cited by 19,642
CategoryTheory.Functorstatement and proof · cited by 16,252
CategoryTheory.Functor.compproof · cited by 6,529
CategoryTheory.SmallCategorystatement and proof · cited by 480
CategoryTheory.forgetproof · cited by 418
MonCatstatement and proof · cited by 127
MonCat.carrierstatement and proof · cited by 107
CategoryTheory.Functor.ιColimitTypeproof · cited by 23
MonCat.FilteredColimits.Mstatement · cited by 8

Cited by7

Results whose statement or proof uses this declaration.

MonCat.FilteredColimits.M.mk_eqstatement · cited by 5
MonCat.FilteredColimits.colimit_mul_mk_eqstatement · cited by 2
MonCat.FilteredColimits.colimitMulAuxproof · cited by 2
MonCat.FilteredColimits.colimit_one_eqstatement · cited by 1
MonCat.FilteredColimits.colimit_mul_mk_eq'statement and proof · cited by 0
MonCat.FilteredColimits.M.map_mkstatement · cited by 0
MonCat.FilteredColimits.M.mk_surjectivestatement · cited by 0