Theorems · Definition · category theory

GrpCat.FilteredColimits.G.mk

{J : Type v} →
  [inst : CategoryTheory.SmallCategory J] →
    [inst_1 : CategoryTheory.IsFiltered J] →
      (F : CategoryTheory.Functor J GrpCat) → (j : J) × ↑(F.obj j) → ↑(GrpCat.FilteredColimits.G F)

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

Defined in

Mathlib.Algebra.Category.Grp.FilteredColimits

Cited by

5 results in Mathlib

Foundations

Depth 35 from the axioms · uses propext, Classical.choice, Quot.sound

Assumes

CategoryTheory.SmallCategoryCategoryTheory.IsFiltered