Theorems · Definition · category theory

CategoryTheory.Limits.Multiequalizer.lift

{C : Type u} →
  [inst : CategoryTheory.Category.{v, u} C] →
    {J : CategoryTheory.Limits.MulticospanShape} →
      (I : CategoryTheory.Limits.MulticospanIndex J C) →
        [inst_1 : CategoryTheory.Limits.HasMultiequalizer I] →
          (W : C) →
            (k : (a : J.L) → W ⟶ I.left a) →
              (∀ (b : J.R),
                  CategoryTheory.CategoryStruct.comp (k (J.fst b)) (I.fst b) =
                    CategoryTheory.CategoryStruct.comp (k (J.snd b)) (I.snd b)) →
                (W ⟶ CategoryTheory.Limits.multiequalizer I)

Construct a morphism to the multiequalizer from its universal property.

Defined in

Mathlib.CategoryTheory.Limits.Shapes.Multiequalizer

Cited by

18 results in Mathlib

Foundations

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

Assumes

CategoryTheory.CategoryCategoryTheory.Limits.HasMultiequalizer