Theorems · Definition · category theory

DirectLimit.lift

{ι : Type u_1} →
  [inst : Preorder ι] →
    {F : ι → Type u_4} →
      {T : ⦃i j : ι⦄ → i ≤ j → Sort u_8} →
        (f : (i j : ι) → (h : i ≤ j) → T h) →
          [inst_1 : ⦃i j : ι⦄ → (h : i ≤ j) → FunLike (T h) (F i) (F j)] →
            [inst_2 : DirectedSystem F fun x1 x2 x3 => ⇑(f x1 x2 x3)] →
              [inst_3 : IsDirectedOrder ι] →
                {C : Sort u_9} →
                  (ih : (i : ι) → F i → C) →
                    (∀ (i j : ι) (h : i ≤ j) (x : F i), ih i x = ih j ((f i j h) x)) → DirectLimit F f → C

To define a function from the direct limit, it suffices to provide one function from each component subject to a compatibility condition.

Defined in

Mathlib.Order.DirectedInverseSystem

Cited by

29 results in Mathlib

Foundations

Depth 13 from the axioms · uses propext, Quot.sound

Assumes

PreorderFunLikeDirectedSystemIsDirectedOrder