Theorems · Definition · category theory

AddMonCat.FilteredColimits.colimitAddAux

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

The "unlifted" version of addition in the colimit. To add two dependent pairs ⟨j₁, x⟩ and ⟨j₂, y⟩, we pass to a common successor of j₁ and j₂ (given by IsFiltered.max) and add them there.

Defined in

Mathlib.Algebra.Category.MonCat.FilteredColimits

Cited by

2 results in Mathlib

Foundations

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

Assumes

CategoryTheory.SmallCategoryCategoryTheory.IsFiltered